| 1 | % Heinrich Heine Universitaet Duesseldorf | |
| 2 | % (c) 2025-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | ||
| 6 | :- module(simplification_rules,[simplification_rule/6, is_true/1]). | |
| 7 | ||
| 8 | ||
| 9 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 10 | :- module_info(group,sequent_prover). | |
| 11 | :- module_info(description,'This module provides the simplification rules'). | |
| 12 | ||
| 13 | :- use_module(seqproversrc(prover_utils)). | |
| 14 | :- use_module(library(lists)). | |
| 15 | :- use_module(probsrc(tools),[list_intersection/3, list_difference/3]). | |
| 16 | ||
| 17 | simplification_rule(Goal,NewGoal,_,Rule,Descr,Info) :- | |
| 18 | simp_rule(Goal,NewGoal,Rule,level0,Descr,Info), | |
| 19 | Goal \= NewGoal. | |
| 20 | simplification_rule(Goal,NewGoal,Hyps,Rule,Descr,_Info) :- | |
| 21 | simp_rule_with_hyps(Goal,NewGoal,Rule,Hyps), | |
| 22 | create_descr(Rule,Goal,Descr), | |
| 23 | Goal \= NewGoal. | |
| 24 | ||
| 25 | ||
| 26 | ||
| 27 | is_true(equal(X,Y)) :- equal_terms(X,Y). % SIMP_MULTI_EQUAL | |
| 28 | is_true(less_equal(X,Y)) :- equal_terms(X,Y). % SIMP_MULTI_LT + SIMP_MULTI_GT | |
| 29 | is_true(greater_equal(X,Y)) :- equal_terms(X,Y). % SIMP_MULTI_LE + SIMP_MULTI_GE | |
| 30 | is_true(negation(falsity)). % SIMP_SPECIAL_NOT_BFALSE | |
| 31 | is_true(subset(empty_set,_)). % SIMP_SPECIAL_SUBSETEQ | |
| 32 | is_true(subset(S,T)) :- equal_terms(S,T). % SIMP_MULTI_SUBSETEQ | |
| 33 | is_true(implication(_P,truth)). % SIMP_SPECIAL_IMP_BTRUE_R | |
| 34 | is_true(implication(falsity,_P)). % SIMP_SPECIAL_IMP_BFALSE_L | |
| 35 | is_true(implication(P,Q)) :- equal_terms(P,Q). % SIMP_MULTI_IMP | |
| 36 | is_true(equivalence(P,Q)) :- equal_terms(P,Q). % SIMP_MULTI_EQV | |
| 37 | is_true(member(card(_S),Nat)) :- is_natural_set(Nat). % SIMP_CARD_NATURAL | |
| 38 | is_true(P) :- is_less_eq(P,0,card(_S)). % SIMP_LIT_LE_CARD_0 + SIMP_LIT_GE_CARD_0 | |
| 39 | is_true(member(min(S),T)) :- equal_terms(S,T). % SIMP_MIN_IN | |
| 40 | is_true(member(max(S),T)) :- equal_terms(S,T). % SIMP_MAX_IN | |
| 41 | is_true(member(couple(E,F),event_b_identity)) :- equal_terms(E,F). % SIMP_SPECIAL_IN_ID | |
| 42 | is_true(finite(bool_set)). % SIMP_FINITE_BOOL | |
| 43 | is_true(finite(set_extension(_))). % SIMP_FINITE_SETENUM | |
| 44 | is_true(finite(interval(_,_))). % SIMP_FINITE_UPTO | |
| 45 | is_true(finite(empty_set)). % SIMP_SPECIAL_FINITE | |
| 46 | is_true(member(I,Nat)) :- is_natural_set(Nat), number(I), I >= 0. % SIMP_LIT_IN_NATURAL | |
| 47 | is_true(member(I,Nat)) :- is_natural1_set(Nat), number(I), I >= 1. % SIMP_LIT_IN_NATURAL1 | |
| 48 | ||
| 49 | ||
| 50 | ||
| 51 | % simp_rule/6 | |
| 52 | simp_rule(X,NewX,Rule,Op,Descr,Info) :- | |
| 53 | (simp_rule(X,NewX,Rule) | |
| 54 | ; simp_rule(X,NewX,Rule,Op) | |
| 55 | ; simp_rule(X,NewX,Rule,Op,Info) | |
| 56 | ; simp_rule_with_info(X,NewX,Rule,Info)), | |
| 57 | create_descr(Rule,X,Descr). | |
| 58 | simp_rule(X,NewX,Rule,_,Descr,_) :- simp_rule_with_descr(X,NewX,Rule,Descr). | |
| 59 | simp_rule(Expr,Res,Expr,_,Descr,_) :- compute(Expr,Res), create_descr('Compute',Expr,Descr). | |
| 60 | % allow simplifications deeper inside the term: | |
| 61 | simp_rule(Term,NewTerm,Rule,_OuterOp,Descr,Info) :- sub_terms_as_list(Term,Op,List), !, | |
| 62 | append(Prefix,[P|Suffix],List), | |
| 63 | simp_rule(P,Q,Rule,Op,Descr,Info), | |
| 64 | append(Prefix,[Q|Suffix],NewList), sub_terms_as_list(NewTerm,Op,NewList). | |
| 65 | simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,P], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,Q]. | |
| 66 | simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,P,R], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,Q,R]. | |
| 67 | simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,R,P], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,R,Q]. | |
| 68 | ||
| 69 | % TODO: complete the list below: | |
| 70 | sub_terms_as_list(partition(S,L),partition,[S|L]). | |
| 71 | sub_terms_as_list(set_extension(L),set_extension,L). | |
| 72 | sub_terms_as_list(sequence_extension(L),sequence_extension,L). | |
| 73 | ||
| 74 | ||
| 75 | compute(Expr,Res) :- evaluate(Expr,Res). | |
| 76 | ||
| 77 | evaluate(I,I) :- number(I). | |
| 78 | evaluate(add(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI + NewJ. | |
| 79 | evaluate(minus(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI - NewJ. | |
| 80 | evaluate(multiplication(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI * NewJ. | |
| 81 | evaluate(div(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), J =\= 0, Res is NewI // NewJ. | |
| 82 | evaluate(modulo(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), J =\= 0, Res is NewI mod NewJ. | |
| 83 | evaluate(power_of(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI ^ NewJ. | |
| 84 | ||
| 85 | ||
| 86 | % simp_rule/5 | |
| 87 | simp_rule(U,Ty,'SIMP_TYPE_BUNION',OuterOp,Info) :- OuterOp \= union, | |
| 88 | % S \/ ... Ty \/ ... T == Ty | |
| 89 | member_of_bin_op(union,Ty,U), type_expression(Ty,Info). | |
| 90 | simp_rule(overwrite(P,Q),Res,'SIMP_TYPE_OVERL_CPROD',OuterOp,Info) :- | |
| 91 | OuterOp \= overwrite, | |
| 92 | op_to_list(overwrite(P,Q),List,overwrite), | |
| 93 | overwrite_type(List,[],ResList,Info), | |
| 94 | list_to_op(ResList,Res,overwrite). | |
| 95 | ||
| 96 | % rules that do not require hyps: | |
| 97 | simp_rule(not_equal(L,L),falsity,'SIMP_MULTI_NOTEQUAL'). | |
| 98 | simp_rule(less_equal(I,J),Res,'SIMP_LIT_LE') :- number(I), number(J), (I =< J -> Res=truth ; Res=falsity). % where I and J are literals | |
| 99 | simp_rule(less(I,J),Res,'SIMP_LIT_LT') :- number(I), number(J), (I < J -> Res=truth ; Res=falsity). | |
| 100 | simp_rule(greater_equal(I,J),Res,'SIMP_LIT_GE') :- number(I), number(J), (I >= J -> Res=truth ; Res=falsity). | |
| 101 | simp_rule(greater(I,J),Res,'SIMP_LIT_GT') :- number(I), number(J), (I > J -> Res=truth ; Res=falsity). | |
| 102 | simp_rule(equal(I,J),Res,'SIMP_LIT_EQUAL') :- number(I), number(J), (I = J -> Res=truth ; Res=falsity). | |
| 103 | simp_rule(not_equal(L,R),negation(equal(L,R)),'SIMP_NOTEQUAL'). | |
| 104 | simp_rule(domain(event_b_comprehension_set(Ids,couple(E,_),P)),event_b_comprehension_set(Ids,E,P),'SIMP_DOM_LAMBDA'). | |
| 105 | simp_rule(range(event_b_comprehension_set(Ids,couple(_,F),P)),event_b_comprehension_set(Ids,F,P),'SIMP_RAN_LAMBDA'). | |
| 106 | simp_rule(NotEmpty,exists([X],member(X,Set)),'DEF_SPECIAL_NOT_EQUAL') :- | |
| 107 | (is_inequality(NotEmpty,Set,empty_set) ; NotEmpty = negation(subset(Set,empty_set))), | |
| 108 | new_identifier(Set,X). | |
| 109 | simp_rule(convert_bool(Eq),P,'SIMP_KBOOL_LIT_EQUAL_TRUE') :- is_equality(Eq,P,boolean_true). | |
| 110 | simp_rule(implication(truth,P),P,'SIMP_SPECIAL_IMP_BTRUE_L'). | |
| 111 | simp_rule(implication(P,falsity),negation(P),'SIMP_SPECIAL_IMP_BFALSE_R'). | |
| 112 | simp_rule(not_member(L,R),negation(member(L,R)),'SIMP_NOTIN'). | |
| 113 | simp_rule(not_subset_strict(L,R),negation(subset_strict(L,R)),'SIMP_NOTSUBSET'). | |
| 114 | simp_rule(not_subset(L,R),negation(subset(L,R)),'SIMP_NOTSUBSETEQ'). | |
| 115 | simp_rule(I,equal(E,boolean_true),'SIMP_SPECIAL_NOT_EQUAL_FALSE') :- is_inequality(I,E,boolean_false). % SIMP_SPECIAL_NOT_EQUAL_FALSE_L, SIMP_SPECIAL_NOT_EQUAL_FALSE_R | |
| 116 | simp_rule(I,equal(E,boolean_false),'SIMP_SPECIAL_NOT_EQUAL_TRUE') :- is_inequality(I,E,boolean_true). % SIMP_SPECIAL_NOT_EQUAL_TRUE_L, SIMP_SPECIAL_NOT_EQUAL_TRUE_R | |
| 117 | simp_rule(forall(X,P1,P2),Res,'SIMP_FORALL_AND') :- P2 = conjunct(_,_), distribute_forall(X,P1,P2,Res). | |
| 118 | simp_rule(exists(X,D),Res,'SIMP_EXISTS_OR') :- D = disjunct(_,_), distribute_exists(X,D,Res). | |
| 119 | simp_rule(exists(X,implication(P,Q)),implication(forall(X,truth,P),exists(X,Q)),'SIMP_EXISTS_IMP'). | |
| 120 | simp_rule(forall(L,P1,P2),forall(Used,P1,P2),'SIMP_FORALL') :- remove_unused_identifier(L,P1,Used). | |
| 121 | simp_rule(exists(L,P),exists(Used,P),'SIMP_EXISTS') :- remove_unused_identifier(L,P,Used). | |
| 122 | simp_rule(negation(forall(X,P1,P2)),exists(X,negation(implication(P1,P2))),'DERIV_NOT_FORALL'). | |
| 123 | simp_rule(negation(exists(X,P)),forall(X,truth,negation(P)),'DERIV_NOT_EXISTS'). | |
| 124 | simp_rule(event_b_comprehension_set(Ids,E,P),event_b_comprehension_set(Used,E,P),'SIMP_COMPSET') :- % own rule | |
| 125 | remove_unused_identifier(Ids,P,Used). | |
| 126 | simp_rule(equal(boolean_true,boolean_false),falsity,'SIMP_SPECIAL_EQUAL_TRUE'). | |
| 127 | simp_rule(equal(couple(E,F),couple(G,H)),conjunct(equal(E,G),equal(F,H)),'SIMP_EQUAL_MAPSTO'). | |
| 128 | simp_rule(equal(SetE,SetF),equal(E,F),'SIMP_EQUAL_SING') :- singleton_set(SetE,E),singleton_set(SetF,F). | |
| 129 | simp_rule(set_subtraction(S,S),empty_set,'SIMP_MULTI_SETMINUS'). | |
| 130 | simp_rule(set_subtraction(S,empty_set),S,'SIMP_SPECIAL_SETMINUS_R'). | |
| 131 | simp_rule(set_subtraction(empty_set,_),empty_set,'SIMP_SPECIAL_SETMINUS_L'). | |
| 132 | simp_rule(member(E,set_subtraction(_,set_extension(L))),falsity,'DERIV_MULTI_IN_SETMINUS') :- member(F,L), equal_terms(E,F). | |
| 133 | simp_rule(member(E,U),truth,'DERIV_MULTI_IN_BUNION') :- | |
| 134 | % E\in A\/...\/ {..., E,...} \/...\/ B == \btrue | |
| 135 | % U = union(_,_), this requirement is not necessary for soundness of the rule | |
| 136 | member_of(union,set_extension(L),U), | |
| 137 | member(F,L), | |
| 138 | equal_terms(E,F). | |
| 139 | simp_rule(convert_bool(truth),boolean_true,'SIMP_SPECIAL_KBOOL_BTRUE'). | |
| 140 | simp_rule(convert_bool(falsity),boolean_false,'SIMP_SPECIAL_KBOOL_BFALSE'). | |
| 141 | simp_rule(unary_minus(C),NewC,'DISTRI_MINUS') :- % own rule | |
| 142 | distribute_unary_minus(C,NewC). | |
| 143 | simp_rule(C,Res,'DISTRI_MINUS') :- | |
| 144 | distribute_binary_minus(C,NewC), | |
| 145 | left_associate_additions(NewC,Res). | |
| 146 | simp_rule(subset(Union,T),Res,'DISTRI_SUBSETEQ_BUNION_SING') :- | |
| 147 | member_of(union,SetF,Union), | |
| 148 | singleton_set(SetF,_), | |
| 149 | union_subset_member(T,Union,Res). | |
| 150 | simp_rule(finite(S),exists([N,F],member(F,total_bijection(interval(1,N),S))),'DEF_FINITE') :- | |
| 151 | new_identifier(S,N), | |
| 152 | new_function(S,F). | |
| 153 | simp_rule(finite(U),Conj,'SIMP_FINITE_BUNION') :- U = union(_,_), finite_union(U,Conj). % covers fin_bunion_r | |
| 154 | simp_rule(finite(pow_subset(S)),finite(S),'SIMP_FINITE_POW'). | |
| 155 | simp_rule(finite(cartesian_product(S,T)),disjunct(disjunct(equal(S,empty_set),equal(T,empty_set)),conjunct(finite(S),finite(T))),'DERIV_FINITE_CPROD'). | |
| 156 | simp_rule(finite(reverse(R)),finite(R),'SIMP_FINITE_CONVERSE'). | |
| 157 | simp_rule(finite(domain_restriction(E,event_b_identity)),finite(E),'SIMP_FINITE_ID_DOMRES'). | |
| 158 | simp_rule(finite(domain_restriction(E,event_b_first_projection_v2)),finite(E),'SIMP_FINITE_PRJ1_DOMRES'). | |
| 159 | simp_rule(finite(domain_restriction(E,event_b_second_projection_v2)),finite(E),'SIMP_FINITE_PRJ2_DOMRES'). | |
| 160 | simp_rule(finite(Nat),falsity,'SIMP_FINITE_NATURAL') :- is_natural_set(Nat). | |
| 161 | simp_rule(finite(Nat),falsity,'SIMP_FINITE_NATURAL1') :- is_natural1_set(Nat). | |
| 162 | simp_rule(finite(Z),falsity,'SIMP_FINITE_INTEGER') :- is_integer_set(Z). | |
| 163 | simp_rule(equivalence(A,B),P,'SIMP_SPECIAL_EQV_BTRUE') :- sym_unify(A,B,P,truth). | |
| 164 | simp_rule(equivalence(A,B),negation(P),'SIMP_SPECIAL_EQV_BFALSE') :- sym_unify(A,B,P,falsity). | |
| 165 | simp_rule(subset_strict(A,B),conjunct(subset(A,B),negation(equal(A,B))),'DEF_SUBSET'). | |
| 166 | simp_rule(subset_strict(_,empty_set),falsity,'SIMP_SPECIAL_SUBSET_R'). | |
| 167 | simp_rule(subset_strict(empty_set,S),negation(equal(S,empty_set)),'SIMP_SPECIAL_SUBSET_L'). | |
| 168 | simp_rule(subset_strict(S,T),falsity,'SIMP_MULTI_SUBSET') :- equal_terms(S,T). | |
| 169 | simp_rule(C,Res,'DISTRI_PROD_PLUS') :- distri(C,Res,multiplication,add). | |
| 170 | simp_rule(C,Res,'DISTRI_PROD_MINUS') :- distri(C,Res,multiplication,minus). | |
| 171 | simp_rule(C,Res,'DISTRI_AND_OR') :- distri(C,Res,conjunct,disjunct). | |
| 172 | simp_rule(C,Res,'DISTRI_OR_AND') :- distri(C,Res,disjunct,conjunct). | |
| 173 | simp_rule(implication(P,Q),implication(negation(Q),negation(P)),'DERIV_IMP'). | |
| 174 | simp_rule(implication(P,implication(Q,R)),implication(conjunct(P,Q),R),'DERIV_IMP_IMP'). | |
| 175 | simp_rule(implication(P,C),Res,'DISTRI_IMP_AND') :- C = conjunct(_,_), and_imp(C,P,Res,conjunct). | |
| 176 | simp_rule(implication(D,R),Res,'DISTRI_IMP_OR') :- D = disjunct(_,_), and_imp(D,R,Res,disjunct). | |
| 177 | simp_rule(equivalence(P,Q),conjunct(implication(P,Q),implication(Q,P)),'DEF_EQV'). | |
| 178 | simp_rule(conjunct(A,B),P,'SIMP_SPECIAL_AND_BTRUE') :- sym_unify(A,B,P,truth). | |
| 179 | simp_rule(disjunct(A,B),P,'SIMP_SPECIAL_OR_BFALSE') :- sym_unify(A,B,P,falsity). | |
| 180 | simp_rule(implication(NotP,P),P,'SIMP_MULTI_IMP_NOT_L') :- is_negation(P,NotP). | |
| 181 | simp_rule(implication(P,NotP),NotP,'SIMP_MULTI_IMP_NOT_R') :- is_negation(P,NotP). | |
| 182 | simp_rule(equivalence(A,B),falsity,'SIMP_MULTI_EQV_NOT') :- sym_unify(A,B,P,NotP), is_negation(P,NotP). | |
| 183 | simp_rule(implication(C,Q),truth,'SIMP_MULTI_IMP_AND') :- | |
| 184 | % P & ... & Q & ... & R => Q == \btrue | |
| 185 | member_of(conjunct,Q,C). % TODO: will not select a conjunction for Q | |
| 186 | simp_rule(negation(truth),falsity,'SIMP_SPECIAL_NOT_BTRUE'). | |
| 187 | simp_rule(member(X,SetA),equal(X,A),'SIMP_IN_SING') :- | |
| 188 | singleton_set(SetA,A). | |
| 189 | simp_rule(subset(SetA,S),member(A,S),'SIMP_SUBSETEQ_SING') :- singleton_set(SetA,A). | |
| 190 | simp_rule(subset(Union,S),Conj,'DERIV_SUBSETEQ_BUNION') :- Union = union(_,_), union_subset(S,Union,Conj). | |
| 191 | simp_rule(subset(S,Inter),Conj,'DERIV_SUBSETEQ_BINTER') :- Inter = intersection(_,_), subset_inter(S,Inter,Conj). | |
| 192 | simp_rule(member(_,empty_set),falsity,'SIMP_SPECIAL_IN') . | |
| 193 | simp_rule(member(B,S),truth,'SIMP_MULTI_IN') :- S = set_extension(L), member(B,L). | |
| 194 | simp_rule(set_extension(L),set_extension(Res),'SIMP_MULTI_SETENUM') :- without_duplicates(L,Res). | |
| 195 | simp_rule(subset(S,U),truth,'SIMP_SUBSETEQ_BUNION') :- member_of(union,S,U). | |
| 196 | simp_rule(subset(I,S),truth,'SIMP_SUBSETEQ_BINTER') :- member_of(intersection,S,I). | |
| 197 | simp_rule(implication(C,negation(Q)),negation(C),'SIMP_MULTI_IMP_AND_NOT_R') :- member_of(conjunct,Q,C). | |
| 198 | simp_rule(implication(C,Q),negation(C),'SIMP_MULTI_IMP_AND_NOT_L') :- member_of(conjunct,negation(Q),C). | |
| 199 | simp_rule(union(A,B),S,'SIMP_SPECIAL_BUNION') :- sym_unify(A,B,S,empty_set). | |
| 200 | simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_EQUAL_RELDOMRAN') :- R=..[Op,empty_set,empty_set], | |
| 201 | member(Op,[total_surjection,total_bijection,total_surjection_relation]). | |
| 202 | simp_rule(domain(cartesian_product(E,F)),E,'SIMP_MULTI_DOM_CPROD') :- equal_terms(E,F). | |
| 203 | simp_rule(range(cartesian_product(E,F)),E,'SIMP_MULTI_RAN_CPROD') :- equal_terms(E,F). | |
| 204 | simp_rule(image(cartesian_product(SetE,S),SetF),S,'SIMP_MULTI_RELIMAGE_CPROD_SING') :- | |
| 205 | singleton_set(SetE,E), | |
| 206 | singleton_set(SetF,F), | |
| 207 | equal_terms(E,F). | |
| 208 | simp_rule(image(set_extension([couple(E,G)]),SetF),set_extension([G]),'SIMP_MULTI_RELIMAGE_SING_MAPSTO') :- | |
| 209 | singleton_set(SetF,F), | |
| 210 | equal_terms(E,F). | |
| 211 | simp_rule(domain(domain_restriction(A,F)),intersection(domain(F),A),'SIMP_MULTI_DOM_DOMRES'). | |
| 212 | simp_rule(domain(domain_subtraction(A,F)),set_subtraction(domain(F),A),'SIMP_MULTI_DOM_DOMSUB'). | |
| 213 | simp_rule(range(range_restriction(F,A)),intersection(range(F),A),'SIMP_MULTI_RAN_RANRES'). | |
| 214 | simp_rule(range(range_subtraction(F,A)),set_subtraction(range(F),A),'SIMP_MULTI_RAN_RANSUB'). | |
| 215 | simp_rule(M,exists([Y],member(couple(R,Y),F)),'DEF_IN_DOM') :- | |
| 216 | M = member(R,domain(F)), | |
| 217 | new_identifier(M,Y). | |
| 218 | simp_rule(M,exists([X],member(couple(X,R),F)),'DEF_IN_RAN') :- | |
| 219 | M = member(R,range(F)), | |
| 220 | new_identifier(M,X). | |
| 221 | simp_rule(member(couple(E,F),reverse(R)),member(couple(F,E),R),'DEF_IN_CONVERSE'). | |
| 222 | simp_rule(member(couple(E,F),domain_restriction(S,R)),conjunct(member(E,S),member(couple(E,F),R)),'DEF_IN_DOMRES'). | |
| 223 | simp_rule(member(couple(E,F),range_restriction(R,T)),conjunct(member(couple(E,F),R),member(F,T)),'DEF_IN_RANRES'). | |
| 224 | simp_rule(member(couple(E,F),domain_subtraction(S,R)),conjunct(not_member(E,S),member(couple(E,F),R)),'DEF_IN_DOMSUB'). | |
| 225 | simp_rule(member(couple(E,F),range_subtraction(R,T)),conjunct(member(couple(E,F),R),not_member(F,T)),'DEF_IN_RANSUB'). | |
| 226 | simp_rule(member(F,image(R,W)),exists([X],conjunct(member(X,W),member(couple(X,F),R))),'DEF_IN_RELIMAGE') :- | |
| 227 | new_identifier(image(R,W),X). | |
| 228 | simp_rule(M,exists(Ids,Res),'DEF_IN_FCOMP') :- | |
| 229 | M = member(couple(E,F),Comp), | |
| 230 | Comp = composition(_,_), | |
| 231 | op_to_list(Comp,List,composition), | |
| 232 | length(List,Length), | |
| 233 | L1 is Length - 1, | |
| 234 | new_identifiers(M,L1,Ids), | |
| 235 | member_couples(E,F,List,Ids,ConjList), | |
| 236 | list_to_op(ConjList,Res,conjunct). | |
| 237 | simp_rule(image(Comp,S),image(Q,image(P,S)),'DERIV_RELIMAGE_FCOMP') :- split_composition(Comp,P,Q). | |
| 238 | ||
| 239 | simp_rule(composition(SetEF,SetGH),set_extension([couple(E,H)]),'DERIV_FCOMP_SING') :- | |
| 240 | singleton_set(SetEF,couple(E,F)), | |
| 241 | singleton_set(SetGH,couple(G,H)), | |
| 242 | equal_terms(F,G). | |
| 243 | simp_rule(overwrite(P,Q),union(domain_subtraction(domain(Q),P),Q),'DEF_OVERL'). | |
| 244 | simp_rule(member(couple(E,F),event_b_identity),equal(E,F),'DEF_IN_ID'). | |
| 245 | simp_rule(member(couple(E,couple(F,G)),direct_product(P,Q)),conjunct(member(couple(E,F),P),member(couple(E,G),Q)),'DEF_IN_DPROD'). | |
| 246 | simp_rule(member(couple(couple(E,G),couple(F,H)),parallel_product(P,Q)),conjunct(member(couple(E,F),P),member(couple(G,H),Q)),'DEF_IN_PPROD'). | |
| 247 | simp_rule(member(R,relations(S,T)),subset(R,cartesian_product(S,T)),'DEF_IN_REL'). | |
| 248 | simp_rule(member(R,total_relation(S,T)),conjunct(member(R,relations(S,T)),equal(domain(R),S)),'DEF_IN_RELDOM'). | |
| 249 | simp_rule(member(R,surjection_relation(S,T)),conjunct(member(R,relations(S,T)),equal(range(R),T)),'DEF_IN_RELRAN'). | |
| 250 | simp_rule(member(R,total_surjection_relation(S,T)),conjunct(conjunct(member(R,relations(S,T)),equal(domain(R),S)),equal(range(R),T)),'DEF_IN_RELDOMRAN'). | |
| 251 | simp_rule(M,conjunct(Conj1,Conj2),'DEF_IN_FCT') :- | |
| 252 | M = member(F,partial_function(S,T)), | |
| 253 | Conj1 = member(F,relations(S,T)), | |
| 254 | new_identifiers(M,3,Ids), | |
| 255 | Ids = [X,Y,Z], | |
| 256 | Conj2 = forall(Ids,conjunct(member(couple(X,Y),F),member(couple(X,Z),F)),equal(Y,Z)). | |
| 257 | simp_rule(member(X,total_function(Dom,Ran)),conjunct(Conj1,Conj2),'DEF_IN_TFCT') :- | |
| 258 | Conj1 = member(X,partial_function(Dom,Ran)), | |
| 259 | Conj2 = equal(domain(X),Dom). | |
| 260 | simp_rule(member(F,partial_injection(S,T)),conjunct(member(F,partial_function(S,T)),member(reverse(F),partial_function(T,S))),'DEF_IN_INJ'). | |
| 261 | simp_rule(member(F,total_injection(S,T)),conjunct(member(F,partial_injection(S,T)),equal(domain(F),S)),'DEF_IN_TINJ'). | |
| 262 | simp_rule(member(F,partial_surjection(S,T)),conjunct(member(F,partial_function(S,T)),equal(range(F),T)),'DEF_IN_SURJ'). | |
| 263 | simp_rule(member(F,total_surjection(S,T)),conjunct(member(F,partial_surjection(S,T)),equal(domain(F),S)),'DEF_IN_TSURJ'). | |
| 264 | simp_rule(member(F,total_bijection(S,T)),conjunct(member(F,total_injection(S,T)),equal(range(F),T)),'DEF_IN_BIJ'). | |
| 265 | simp_rule(C,Res,'DISTRI_DOMSUB_BUNION_L') :- distri_l3(C,Res,domain_subtraction,union,intersection). | |
| 266 | simp_rule(C,Res,'DISTRI_DOMSUB_BINTER_L') :- distri_l3(C,Res,domain_subtraction,intersection,union). | |
| 267 | ||
| 268 | simp_rule(C,Res,Rule) :- distri_r2(C,Res,Rule). | |
| 269 | simp_rule(C,Res,Rule) :- distri_r3(C,Res,Rule). | |
| 270 | simp_rule(C,Res,Rule) :- distri_l2(C,Res,Rule). | |
| 271 | simp_rule(reverse(U),Res,'DISTRI_CONVERSE_BUNION') :- U = union(_,_), distri_reverse(U,Res,union). | |
| 272 | simp_rule(reverse(I),Res,'DISTRI_CONVERSE_BINTER') :- I = intersection(_,_), distri_reverse(I,Res,intersection). | |
| 273 | simp_rule(reverse(S),Res,'DISTRI_CONVERSE_SETMINUS') :- S = set_subtraction(_,_), distri_reverse(S,Res,set_subtraction). | |
| 274 | simp_rule(reverse(R),Res,'DISTRI_CONVERSE_BCOMP') :- R = ring(_,_), distri_reverse_reverse(R,Res,ring). | |
| 275 | simp_rule(reverse(R),Res,'DISTRI_CONVERSE_FCOMP') :- R = composition(_,_), distri_reverse_reverse(R,Res,composition). | |
| 276 | simp_rule(reverse(parallel_product(S,R)),parallel_product(reverse(S),reverse(R)),'DISTRI_CONVERSE_PPROD'). | |
| 277 | simp_rule(reverse(domain_restriction(S,R)),range_restriction(reverse(R),S),'DISTRI_CONVERSE_DOMRES'). | |
| 278 | simp_rule(reverse(domain_subtraction(S,R)),range_subtraction(reverse(R),S),'DISTRI_CONVERSE_DOMSUB'). | |
| 279 | simp_rule(reverse(range_restriction(R,S)),domain_restriction(S,reverse(R)),'DISTRI_CONVERSE_RANRES'). | |
| 280 | simp_rule(reverse(range_subtraction(R,S)),domain_subtraction(S,reverse(R)),'DISTRI_CONVERSE_RANSUB'). | |
| 281 | simp_rule(domain(U),Res,'DISTRI_DOM_BUNION') :- U = union(_,_), distri_union(U,Res,domain). | |
| 282 | simp_rule(range(U),Res,'DISTRI_RAN_BUNION') :- U = union(_,_), distri_union(U,Res,range). | |
| 283 | simp_rule(image(R,U),Res,'DISTRI_RELIMAGE_BUNION_R') :- U = union(_,_), image_union(R,U,Res). | |
| 284 | simp_rule(image(U,S),Res,'DISTRI_RELIMAGE_BUNION_L') :- U = union(_,_), union_image(U,S,Res). | |
| 285 | simp_rule(member(LB,interval(LB,UB)),truth,'lower_bound_in_interval') :- number(LB), number(UB), LB =< UB. % own rule: lower bound in interval | |
| 286 | simp_rule(member(Nr,interval(LB,UB)),truth,'SIMP_IN_UPTO') :- number(LB), number(UB), number(Nr), LB =< Nr, Nr =< UB. % own rule | |
| 287 | simp_rule(member(Nr,interval(LB,UB)),falsity,'SIMP_IN_UPTO') :- number(LB), number(UB), number(Nr), (Nr =< LB ; UB =< Nr). % own rule | |
| 288 | simp_rule(member(E,U),Res,'DEF_IN_BUNION') :- U = union(_,_), member_union(E,U,Res). | |
| 289 | simp_rule(member(E,I),Res,'DEF_IN_BINTER') :- I = intersection(_,_), member_intersection(E,I,Res). | |
| 290 | simp_rule(member(couple(E,F),cartesian_product(S,T)),conjunct(member(E,S),member(F,T)),'DEF_IN_MAPSTO'). | |
| 291 | simp_rule(member(E,pow_subset(S)),subset(E,S),'DEF_IN_POW'). | |
| 292 | simp_rule(member(E,pow1_subset(S)),conjunct(member(E,pow_subset(S)),not_equal(S,empty_set)),'DEF_IN_POW1'). | |
| 293 | simp_rule(S,forall([X],member(X,A),member(X,B)),'DEF_SUBSETEQ') :- S = subset(A,B), new_identifier(S,X). | |
| 294 | simp_rule(member(E,set_subtraction(S,T)),conjunct(member(E,S),negation(member(E,T))),'DEF_IN_SETMINUS'). | |
| 295 | simp_rule(member(E,set_extension(L)),D,'DEF_IN_SETENUM') :- L = [A,B|T], | |
| 296 | or_equal(T,E,disjunct(equal(E,A),equal(E,B)),D). | |
| 297 | simp_rule(M,exists([X],conjunct(member(X,S),member(E,X))),'DEF_IN_KUNION') :- | |
| 298 | M = member(E,general_union(S)), | |
| 299 | new_identifier(M,X). | |
| 300 | simp_rule(member(E,general_intersection(S)),forall([X],member(X,S),member(E,X)),'DEF_IN_KINTER') :- new_identifier(S,X). | |
| 301 | simp_rule(member(E,quantified_union(Ids,P,T)),exists(NewIds,conjunct(P1,member(E,T1))),'DEF_IN_QUNION') :- | |
| 302 | length(Ids,L), | |
| 303 | new_identifiers(E,L,NewIds), | |
| 304 | rewrite_pairwise(Ids,NewIds,conjunct(P,T),conjunct(P1,T1)). | |
| 305 | simp_rule(member(E,quantified_intersection(Ids,P,T)),forall(NewIds,P1,member(E,T1)),'DEF_IN_QINTER') :- | |
| 306 | length(Ids,L), | |
| 307 | new_identifiers(E,L,NewIds), | |
| 308 | rewrite_pairwise(Ids,NewIds,conjunct(P,T),conjunct(P1,T1)). | |
| 309 | simp_rule(member(E,interval(L,R)),conjunct(less_equal(L,E),less_equal(E,R)),'DEF_IN_UPTO'). | |
| 310 | simp_rule(C,Res,'DISTRI_BUNION_BINTER') :- distri(C,Res,union,intersection). | |
| 311 | simp_rule(C,Res,'DISTRI_BINTER_BUNION') :- distri(C,Res,intersection,union). | |
| 312 | simp_rule(C,Res,'DISTRI_BINTER_SETMINUS') :- distri(C,Res,intersection,set_subtraction). | |
| 313 | simp_rule(set_subtraction(X,Y),Res,'DISTRI_SETMINUS_BUNION') :- distri_setminus(X,Y,Res). | |
| 314 | simp_rule(C,Res,'DISTRI_CPROD_BINTER') :- distri(C,Res,cartesian_product,intersection). | |
| 315 | simp_rule(C,Res,'DISTRI_CPROD_BUNION') :- distri(C,Res,cartesian_product,union). | |
| 316 | simp_rule(C,Res,'DISTRI_CPROD_SETMINUS') :- distri(C,Res,cartesian_product,set_subtraction). | |
| 317 | simp_rule(subset(set_subtraction(A,B),S),subset(A,union(B,S)),'DERIV_SUBSETEQ_SETMINUS_L'). | |
| 318 | simp_rule(subset(S,set_subtraction(A,B)),conjunct(subset(S,A),equal(intersection(S,B),empty_set)),'DERIV_SUBSETEQ_SETMINUS_R'). | |
| 319 | simp_rule(partition(S,L),Res,'DEF_PARTITION') :- | |
| 320 | length(L,LL), LL > 1, | |
| 321 | list_to_op(L,U,union), | |
| 322 | Eq = equal(S,U), | |
| 323 | findall(equal(intersection(X,Y),empty_set),(all_pairs(L,Pairs), member([X,Y],Pairs)), Disjoint), | |
| 324 | list_to_op([Eq|Disjoint],Res,conjunct). | |
| 325 | simp_rule(partition(S,[]),equal(S,empty_set),'SIMP_EMPTY_PARTITION'). | |
| 326 | simp_rule(partition(S,[T]),equal(S,T),'SIMP_SINGLE_PARTITION'). | |
| 327 | simp_rule(domain(set_extension(L)),set_extension(Res),'SIMP_DOM_SETENUM') :- | |
| 328 | map_dom(L,Dom), | |
| 329 | without_duplicates(Dom,Res). | |
| 330 | simp_rule(range(set_extension(L)),set_extension(Res),'SIMP_RAN_SETENUM') :- | |
| 331 | map_ran(L,Ran), | |
| 332 | without_duplicates(Ran,Res). | |
| 333 | simp_rule(general_union(pow_subset(S)),S,'SIMP_KUNION_POW'). | |
| 334 | simp_rule(general_union(pow1_subset(S)),S,'SIMP_KUNION_POW1'). | |
| 335 | simp_rule(general_union(set_extension([empty_set])),empty_set,'SIMP_SPECIAL_KUNION'). | |
| 336 | simp_rule(quantified_union([_],falsity,_),empty_set,'SIMP_SPECIAL_QUNION'). | |
| 337 | simp_rule(general_intersection(set_extension([empty_set])),empty_set,'SIMP_SPECIAL_KINTER'). | |
| 338 | simp_rule(general_intersection(pow_subset(S)),S,'SIMP_KINTER_POW'). | |
| 339 | simp_rule(pow_subset(empty_set),set_extension([empty_set]),'SIMP_SPECIAL_POW'). | |
| 340 | simp_rule(pow1_subset(empty_set),empty_set,'SIMP_SPECIAL_POW1'). | |
| 341 | simp_rule(event_b_comprehension_set(Ids,X,member(X,S)),S,'SIMP_COMPSET_IN') :- | |
| 342 | used_identifiers(X,Ids), | |
| 343 | free_identifiers(S,Free), | |
| 344 | list_intersection(Ids,Free,[]). | |
| 345 | simp_rule(event_b_comprehension_set(Ids,X,subset(X,S)),pow_subset(S),'SIMP_COMPSET_SUBSETEQ') :- | |
| 346 | used_identifiers(X,Ids), | |
| 347 | free_identifiers(S,Free), | |
| 348 | list_intersection(Ids,Free,[]). | |
| 349 | simp_rule(event_b_comprehension_set(_,_,falsity),empty_set,'SIMP_SPECIAL_COMPSET_BFALSE'). | |
| 350 | simp_rule(event_b_comprehension_set(Ids,F,Conj),event_b_comprehension_set(Ids0,F1,Conj0),'SIMP_COMPSET_EQUAL') :- | |
| 351 | op_to_list(Conj,ConjList,conjunct), | |
| 352 | select(Eq,ConjList,ConjList0), | |
| 353 | is_equality(Eq,X,E), | |
| 354 | list_to_op(ConjList0,Conj0,conjunct), | |
| 355 | free_identifiers(conjunct(E,Conj0),Free), | |
| 356 | op_to_list(X,CIds,couple), | |
| 357 | list_intersection(CIds,Free,[]), | |
| 358 | list_subset(CIds,Ids), | |
| 359 | list_difference(Ids,CIds,Ids0), | |
| 360 | Ids0 \= [], | |
| 361 | rewrite(X,E,F,F1). | |
| 362 | simp_rule(member(E,event_b_comprehension_set(BIds,X,P)),Q,'SIMP_IN_COMPSET_ONEPOINT') :- | |
| 363 | op_to_list(X,IdsX,couple), | |
| 364 | IdsX = BIds, | |
| 365 | op_to_list(E,IdsE,couple), | |
| 366 | length(IdsX,LengthX), | |
| 367 | length(IdsE,LengthE), | |
| 368 | LengthE =:= LengthX, | |
| 369 | rewrite_pairwise(IdsX,IdsE,P,Q). | |
| 370 | simp_rule(member(F,event_b_comprehension_set(Ids,E,P)),exists(Ids,conjunct(P,equal(E,F))),'SIMP_IN_COMPSET') :- | |
| 371 | free_identifiers(F,FreeInF), | |
| 372 | list_intersection(Ids,FreeInF,[]). | |
| 373 | simp_rule(Exp,forall(NewIds,member(Couple,S),Q),'SIMP_SUBSETEQ_COMPSET_R') :- | |
| 374 | Exp = subset(S,event_b_comprehension_set(BIds,X,P)), | |
| 375 | op_to_list(X,IdsX,couple), | |
| 376 | IdsX = BIds, | |
| 377 | length(BIds,NrOfIds), | |
| 378 | new_identifiers(Exp,NrOfIds,NewIds), | |
| 379 | list_to_op(NewIds,Couple,couple), | |
| 380 | rewrite_pairwise(BIds,NewIds,P,Q). | |
| 381 | simp_rule(function(event_b_comprehension_set([X],couple(X,E),_),Y),F,'SIMP_FUNIMAGE_LAMBDA') :- rewrite(X,Y,E,F). | |
| 382 | simp_rule(Hyp,New,Rule) :- | |
| 383 | CompSet = event_b_comprehension_set(Ids,couple(E,F),P), | |
| 384 | NewComp = event_b_comprehension_set(Ids,E,P), | |
| 385 | (Hyp = finite(CompSet), New = finite(NewComp), Rule = 'SIMP_FINITE_LAMBDA' ; | |
| 386 | Hyp = card(CompSet), New = card(NewComp), Rule = 'SIMP_CARD_LAMBDA' ), | |
| 387 | used_identifiers(E,IdsE), | |
| 388 | list_subset(Ids,IdsE), | |
| 389 | used_identifiers(F,IdsF), | |
| 390 | list_intersection(IdsF,Ids,BoundF), | |
| 391 | list_subset(BoundF,IdsE). | |
| 392 | simp_rule(overwrite(A,B),S,'SIMP_SPECIAL_OVERL') :- sym_unify(A,B,S,empty_set). | |
| 393 | simp_rule(domain(reverse(R)),range(R),'SIMP_DOM_CONVERSE'). | |
| 394 | simp_rule(range(reverse(R)),domain(R),'SIMP_RAN_CONVERSE'). | |
| 395 | simp_rule(domain_restriction(empty_set,_),empty_set,'SIMP_SPECIAL_DOMRES_L'). | |
| 396 | simp_rule(domain_restriction(_,empty_set),empty_set,'SIMP_SPECIAL_DOMRES_R'). | |
| 397 | simp_rule(domain_restriction(domain(R),R),R,'SIMP_MULTI_DOMRES_DOM'). | |
| 398 | simp_rule(domain_restriction(range(R),reverse(R)),reverse(R),'SIMP_MULTI_DOMRES_RAN'). | |
| 399 | simp_rule(domain_restriction(S,domain_restriction(T,event_b_identity)),domain_restriction(intersection(S,T),event_b_identity),'SIMP_DOMRES_DOMRES_ID'). | |
| 400 | simp_rule(domain_restriction(S,domain_subtraction(T,event_b_identity)),domain_restriction(set_subtraction(S,T),event_b_identity),'SIMP_DOMRES_DOMSUB_ID'). | |
| 401 | simp_rule(range_restriction(_,empty_set),empty_set,'SIMP_SPECIAL_RANRES_R'). | |
| 402 | simp_rule(range_restriction(empty_set,_),empty_set,'SIMP_SPECIAL_RANRES_L'). | |
| 403 | simp_rule(range_restriction(domain_restriction(S,event_b_identity),T),domain_restriction(intersection(S,T),event_b_identity),'SIMP_RANRES_DOMRES_ID'). | |
| 404 | simp_rule(range_restriction(domain_subtraction(S,event_b_identity),T),domain_restriction(set_subtraction(T,S),event_b_identity),'SIMP_RANRES_DOMSUB_ID'). | |
| 405 | simp_rule(range_restriction(R,range(R)),R,'SIMP_MULTI_RANRES_RAN'). | |
| 406 | simp_rule(range_restriction(reverse(R),domain(R)),reverse(R),'SIMP_MULTI_RANRES_DOM'). | |
| 407 | simp_rule(range_restriction(event_b_identity,S),domain_restriction(S,event_b_identity),'SIMP_RANRES_ID'). | |
| 408 | simp_rule(range_subtraction(event_b_identity,S),domain_subtraction(S,event_b_identity),'SIMP_RANSUB_ID'). | |
| 409 | simp_rule(domain_subtraction(empty_set,R),R,'SIMP_SPECIAL_DOMSUB_L'). | |
| 410 | simp_rule(domain_subtraction(_,empty_set),empty_set,'SIMP_SPECIAL_DOMSUB_R'). | |
| 411 | simp_rule(domain_subtraction(domain(R),R),empty_set,'SIMP_MULTI_DOMSUB_DOM'). | |
| 412 | simp_rule(domain_subtraction(range(R),reverse(R)),empty_set,'SIMP_MULTI_DOMSUB_RAN'). | |
| 413 | simp_rule(domain_subtraction(S,domain_restriction(T,event_b_identity)),domain_restriction(set_subtraction(T,S),event_b_identity),'SIMP_DOMSUB_DOMRES_ID'). | |
| 414 | simp_rule(domain_subtraction(S,domain_subtraction(T,event_b_identity)),domain_subtraction(union(S,T),event_b_identity),'SIMP_DOMSUB_DOMSUB_ID'). | |
| 415 | simp_rule(range_subtraction(R,empty_set),R,'SIMP_SPECIAL_RANSUB_R'). | |
| 416 | simp_rule(range_subtraction(empty_set,_),empty_set,'SIMP_SPECIAL_RANSUB_L'). | |
| 417 | simp_rule(range_subtraction(reverse(R),domain(R)),empty_set,'SIMP_MULTI_RANSUB_DOM'). | |
| 418 | simp_rule(range_subtraction(R,range(R)),empty_set,'SIMP_MULTI_RANSUB_RAN'). | |
| 419 | simp_rule(range_subtraction(domain_restriction(S,event_b_identity),T),domain_restriction(set_subtraction(S,T),event_b_identity),'SIMP_RANSUB_DOMRES_ID'). | |
| 420 | simp_rule(range_subtraction(domain_subtraction(S,event_b_identity),T),domain_subtraction(union(S,T),event_b_identity),'SIMP_RANSUB_DOMSUB_ID'). | |
| 421 | simp_rule(composition(A,B),R,'SIMP_TYPE_FCOMP_ID') :- sym_unify(A,B,R,event_b_identity). | |
| 422 | simp_rule(ring(A,B),R,'SIMP_TYPE_BCOMP_ID') :- sym_unify(A,B,R,event_b_identity). | |
| 423 | simp_rule(direct_product(_,empty_set),empty_set,'SIMP_SPECIAL_DPROD_R'). | |
| 424 | simp_rule(direct_product(empty_set,_),empty_set,'SIMP_SPECIAL_DPROD_L'). | |
| 425 | simp_rule(direct_product(cartesian_product(S,T),cartesian_product(U,V)), | |
| 426 | cartesian_product(intersection(S,U),cartesian_product(T,V)),'SIMP_DPROD_CPROD'). | |
| 427 | simp_rule(parallel_product(A,B),empty_set,'SIMP_SPECIAL_PPROD') :- sym_unify(A,B,empty_set,_). % SIMP_SPECIAL_PPROD_L / SIMP_SPECIAL_PPROD_R | |
| 428 | simp_rule(parallel_product(cartesian_product(S,T),cartesian_product(U,V)), | |
| 429 | cartesian_product(cartesian_product(S,U),cartesian_product(T,V)),'SIMP_PPROD_CPROD'). | |
| 430 | simp_rule(image(_,empty_set),empty_set,'SIMP_SPECIAL_RELIMAGE_R'). | |
| 431 | simp_rule(image(empty_set,_),empty_set,'SIMP_SPECIAL_RELIMAGE_L'). | |
| 432 | simp_rule(image(R,domain(R)),range(R),'SIMP_MULTI_RELIMAGE_DOM'). | |
| 433 | simp_rule(image(event_b_identity,T),T,'SIMP_RELIMAGE_ID'). | |
| 434 | simp_rule(image(domain_restriction(S,event_b_identity),T),intersection(S,T),'SIMP_RELIMAGE_DOMRES_ID'). | |
| 435 | simp_rule(image(domain_subtraction(S,event_b_identity),T),set_subtraction(T,S),'SIMP_RELIMAGE_DOMSUB_ID'). | |
| 436 | simp_rule(image(reverse(range_subtraction(_,S)),S),empty_set,'SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB'). | |
| 437 | simp_rule(image(reverse(range_restriction(R,S)),S),image(reverse(R),S),'SIMP_MULTI_RELIMAGE_CONVERSE_RANRES'). | |
| 438 | simp_rule(image(reverse(domain_subtraction(S,R)),T), | |
| 439 | set_subtraction(image(reverse(R),T),S),'SIMP_RELIMAGE_CONVERSE_DOMSUB'). | |
| 440 | simp_rule(image(range_subtraction(R,S),T),set_subtraction(image(R,T),S),'DERIV_RELIMAGE_RANSUB'). | |
| 441 | simp_rule(image(range_restriction(R,S),T),intersection(image(R,T),S),'DERIV_RELIMAGE_RANRES'). | |
| 442 | simp_rule(image(domain_subtraction(S,_),S),empty_set,'SIMP_MULTI_RELIMAGE_DOMSUB'). | |
| 443 | simp_rule(image(domain_subtraction(S,R),T),image(R,set_subtraction(T,S)),'DERIV_RELIMAGE_DOMSUB'). | |
| 444 | simp_rule(image(domain_restriction(S,R),T),image(R,intersection(S,T)),'DERIV_RELIMAGE_DOMRES'). | |
| 445 | simp_rule(reverse(empty_set),empty_set,'SIMP_SPECIAL_CONVERSE'). | |
| 446 | simp_rule(reverse(event_b_identity),event_b_identity,'SIMP_CONVERSE_ID'). | |
| 447 | simp_rule(member(couple(E,F),set_subtraction(_,event_b_identity)),falsity,'SIMP_SPECIAL_IN_SETMINUS_ID') :- equal_terms(E,F). | |
| 448 | simp_rule(member(couple(E,F),domain_restriction(S,event_b_identity)),member(E,S),'SIMP_SPECIAL_IN_DOMRES_ID') :- | |
| 449 | equal_terms(E,F). | |
| 450 | simp_rule(member(couple(E,F),set_subtraction(R,domain_restriction(S,event_b_identity))), | |
| 451 | member(couple(E,F),domain_subtraction(S,R)),'SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID') :- equal_terms(E,F). | |
| 452 | simp_rule(reverse(cartesian_product(S,T)),cartesian_product(T,S),'SIMP_CONVERSE_CPROD'). | |
| 453 | simp_rule(reverse(set_extension(L)),set_extension(NewL),'SIMP_CONVERSE_SETENUM') :- convert_map_to(L,NewL). | |
| 454 | simp_rule(reverse(event_b_comprehension_set(Ids,couple(X,Y),P)), | |
| 455 | event_b_comprehension_set(Ids,couple(Y,X),P),'SIMP_CONVERSE_COMPSET'). | |
| 456 | simp_rule(composition(domain_restriction(S,event_b_identity),R),domain_restriction(S,R),'SIMP_FCOMP_ID_L'). | |
| 457 | simp_rule(composition(R,domain_restriction(S,event_b_identity)),range_restriction(R,S),'SIMP_FCOMP_ID_R'). | |
| 458 | simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_REL_R') :- simp_relation_empty_range(R). | |
| 459 | simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_REL_L') :- simp_relation_empty_domain(R). | |
| 460 | simp_rule(function(event_b_first_projection_v2,couple(E,_)),E,'SIMP_FUNIMAGE_PRJ1'). | |
| 461 | simp_rule(function(event_b_second_projection_v2,couple(_,F)),F,'SIMP_FUNIMAGE_PRJ2'). | |
| 462 | simp_rule(member(couple(E,function(F,E)),F),truth,'SIMP_IN_FUNIMAGE'). | |
| 463 | simp_rule(member(couple(function(reverse(F),E),E),F),truth,'SIMP_IN_FUNIMAGE_CONVERSE_L'). | |
| 464 | simp_rule(member(couple(function(F,E),E),reverse(F)),truth,'SIMP_IN_FUNIMAGE_CONVERSE_R'). | |
| 465 | simp_rule(function(set_extension(L),_),E,'SIMP_MULTI_FUNIMAGE_SETENUM_LL') :- all_map_to(L,E). | |
| 466 | simp_rule(function(set_extension(L),X),Y,'SIMP_MULTI_FUNIMAGE_SETENUM_LR') :- member(couple(Z,Y),L), equal_terms(X,Z). | |
| 467 | simp_rule(function(Over,X),Y,'SIMP_MULTI_FUNIMAGE_OVERL_SETENUM') :- | |
| 468 | Over = overwrite(_,_), | |
| 469 | last_overwrite(Over,set_extension(L)), | |
| 470 | member(couple(Z,Y),L), | |
| 471 | equal_terms(X,Z). | |
| 472 | simp_rule(function(U,X),Y,'SIMP_MULTI_FUNIMAGE_BUNION_SETENUM') :- | |
| 473 | member_of(union,set_extension(L),U), | |
| 474 | member(couple(Z,Y),L), | |
| 475 | equal_terms(X,Z). | |
| 476 | simp_rule(function(cartesian_product(_,set_extension([F])),_),F,'SIMP_FUNIMAGE_CPROD'). | |
| 477 | simp_rule(function(F,function(reverse(F),E)),E,'SIMP_FUNIMAGE_FUNIMAGE_CONVERSE'). | |
| 478 | simp_rule(function(reverse(F),function(F,E)),E,'SIMP_FUNIMAGE_CONVERSE_FUNIMAGE'). | |
| 479 | simp_rule(function(set_extension(L),function(set_extension(L2),E)),E,'SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM') :- | |
| 480 | convert_map_to(L,LConverted), | |
| 481 | equal_terms(LConverted,L2). | |
| 482 | simp_rule(domain_restriction(SetE,event_b_identity),set_extension([couple(E,E)]),'DERIV_ID_SING') :- singleton_set(SetE,E). | |
| 483 | simp_rule(domain(empty_set),empty_set,'SIMP_SPECIAL_DOM'). | |
| 484 | simp_rule(range(empty_set),empty_set,'SIMP_SPECIAL_RAN'). | |
| 485 | simp_rule(reverse(reverse(R)),R,'SIMP_CONVERSE_CONVERSE'). | |
| 486 | simp_rule(function(event_b_identity,X),X,'SIMP_FUNIMAGE_ID'). | |
| 487 | simp_rule(member(E,Nat),less_equal(0,E),'DEF_IN_NATURAL') :- is_natural_set(Nat). | |
| 488 | simp_rule(member(E,Nat),less_equal(1,E),'DEF_IN_NATURAL1') :- is_natural1_set(Nat). | |
| 489 | simp_rule(div(E,1),E,'SIMP_SPECIAL_DIV_1'). | |
| 490 | simp_rule(div(0,_),0,'SIMP_SPECIAL_DIV_0'). | |
| 491 | simp_rule(power_of(E,1),E,'SIMP_SPECIAL_EXPN_1_R'). | |
| 492 | simp_rule(power_of(1,_),1,'SIMP_SPECIAL_EXPN_1_L'). | |
| 493 | simp_rule(power_of(_,0),1,'SIMP_SPECIAL_EXPN_0'). | |
| 494 | simp_rule(add(A,B),S,'SIMP_SPECIAL_PLUS') :- sym_unify(A,B,S,0). | |
| 495 | simp_rule(multiplication(A,B),Res,Rule) :- | |
| 496 | op_to_list(multiplication(A,B),L,multiplication), | |
| 497 | change_sign(L,NL,Nr), | |
| 498 | list_to_op(NL,New,multiplication), | |
| 499 | (Nr mod 2 =:= 0 -> Rule = 'SIMP_SPECIAL_PROD_MINUS_EVEN', Res = New | |
| 500 | ; Rule = 'SIMP_SPECIAL_PROD_MINUS_ODD', Res = unary_minus(New)). | |
| 501 | simp_rule(unary_minus(I),J,'SIMP_LIT_MINUS') :- number(I), J is I * (-1). | |
| 502 | simp_rule(minus(E,0),E,'SIMP_SPECIAL_MINUS_R'). | |
| 503 | simp_rule(minus(0,E),unary_minus(E),'SIMP_SPECIAL_MINUS_L'). | |
| 504 | simp_rule(unary_minus(F),E,'SIMP_MINUS_MINUS') :- is_minus(F,E). | |
| 505 | simp_rule(minus(E,F),add(E,F2),'SIMP_MINUS_UNMINUS') :- is_minus(F,F2). | |
| 506 | simp_rule(minus(E,F),0,'SIMP_MULTI_MINUS') :- equal_terms(E,F). | |
| 507 | simp_rule(minus(S,C),S0,'SIMP_MULTI_MINUS_PLUS_L') :- select_op(C,S,S0,add). | |
| 508 | simp_rule(minus(C,S),unary_minus(S0),'SIMP_MULTI_MINUS_PLUS_R') :- select_op(C,S,S0,add). | |
| 509 | simp_rule(minus(S1,S2),minus(S01,S02),'SIMP_MULTI_MINUS_PLUS_PLUS') :- | |
| 510 | member_of(add,El,S1), | |
| 511 | select_op(El,S1,S01,add), | |
| 512 | select_op(El,S2,S02,add), | |
| 513 | S01 = add(_,_), | |
| 514 | S02 = add(_,_). | |
| 515 | simp_rule(S,S1,'SIMP_MULTI_PLUS_MINUS') :- | |
| 516 | member_of(add,minus(C,D),S), | |
| 517 | select_op(D,S,S0,add), | |
| 518 | select_op(minus(C,D),S0,C,S1,add). | |
| 519 | simp_rule(Ex,Res,Rule) :- simp_multi_arithrel(Ex,Res,Rule). | |
| 520 | simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL') :- % own rule for cases not covered by SIMP_MULTI_ARITHREL_[...] | |
| 521 | \+ simp_multi_arithrel(Ex,Res,_), | |
| 522 | Ex=..[Rel,L,R], | |
| 523 | comparison(Rel), | |
| 524 | (select_summand(L,Term,L0), | |
| 525 | select_summand(R,Term,R0) | |
| 526 | ; select_subtrahend(L,Term,L0), | |
| 527 | select_subtrahend(R,Term,R0) ), | |
| 528 | NewEx=..[Rel,L0,R0], | |
| 529 | normalize_minus(NewEx,Res). | |
| 530 | simp_rule(multiplication(A,B),E,'SIMP_SPECIAL_PROD_1') :- sym_unify(A,B,E,1). | |
| 531 | simp_rule(min(set_extension(L)),min(set_extension(Res)),'SIMP_LIT_MIN') :- | |
| 532 | min_list(L,I), | |
| 533 | remove_greater(L,I,Res). | |
| 534 | simp_rule(max(set_extension(L)),max(set_extension(Res)),'SIMP_LIT_MAX') :- | |
| 535 | max_list(L,I), | |
| 536 | remove_smaller(L,I,Res). | |
| 537 | simp_rule(card(empty_set),0,'SIMP_SPECIAL_CARD'). | |
| 538 | simp_rule(card(set_extension([_])),1,'SIMP_CARD_SING'). | |
| 539 | simp_rule(card(pow_subset(S)),power_of(2,card(S)),'SIMP_CARD_POW'). | |
| 540 | simp_rule(card(union(S,T)),minus(add(card(S),card(T)),card(intersection(S,T))),'SIMP_CARD_BUNION'). | |
| 541 | simp_rule(card(reverse(R)),card(R),'SIMP_CARD_CONVERSE'). | |
| 542 | simp_rule(card(domain_restriction(S,event_b_identity)),S,'SIMP_CARD_ID_DOMRES'). | |
| 543 | simp_rule(card(domain_restriction(E,event_b_first_projection_v2)),E,'SIMP_CARD_PRJ1_DOMRES'). | |
| 544 | simp_rule(card(domain_restriction(E,event_b_second_projection_v2)),E,'SIMP_CARD_PRJ2_DOMRES'). | |
| 545 | simp_rule(P,falsity,'SIMP_MULTI_LT') :- is_less(P,E,F), equal_terms(E,F). % covers SIMP_MULTI_GT too | |
| 546 | simp_rule(div(NE,NF),div(E,F),'SIMP_DIV_MINUS') :- is_minus(NE,E), is_minus(NF,F). | |
| 547 | simp_rule(div(E,F),1,'SIMP_MULTI_DIV') :- equal_terms(E,F). | |
| 548 | simp_rule(modulo(0,_),0,'SIMP_SPECIAL_MOD_0'). | |
| 549 | simp_rule(modulo(_,1),0,'SIMP_SPECIAL_MOD_1'). | |
| 550 | simp_rule(modulo(E,F),1,'SIMP_MULTI_MOD') :- equal_terms(E,F). | |
| 551 | simp_rule(min(SetE),E,'SIMP_MIN_SING') :- singleton_set(SetE,E). | |
| 552 | simp_rule(max(SetE),E,'SIMP_MAX_SING') :- singleton_set(SetE,E). | |
| 553 | simp_rule(div(P1,E2),P0,'SIMP_MULTI_DIV_PROD') :- | |
| 554 | member_of(multiplication,E1,P1), | |
| 555 | equal_terms(E1,E2), | |
| 556 | select_op(E1,P1,P0,multiplication). | |
| 557 | simp_rule(card(set_extension(L)),LL,'SIMP_TYPE_CARD') :- length(L,LL). | |
| 558 | simp_rule(card(interval(I,J)),Res,'SIMP_LIT_CARD_UPTO') :- number(I), number(J), I =< J, Res is J - I + 1. | |
| 559 | simp_rule(card(interval(I,J)),0,'SIMP_LIT_CARD_UPTO') :- number(I), number(J), I > J. % from "Proposal for an extensible rule-based prover for Event-B", pg. 7 | |
| 560 | simp_rule(P,negation(equal(S,empty_set)),'SIMP_LIT_LE_CARD_1') :- is_less_eq(P,1,card(S)). | |
| 561 | simp_rule(P,negation(equal(S,empty_set)),'SIMP_LIT_LT_CARD_0') :- is_less(P,0,card(S)). | |
| 562 | simp_rule(member(card(S),Nat),negation(equal(S,empty_set)),'SIMP_CARD_NATURAL1') :- is_natural1_set(Nat). | |
| 563 | simp_rule(equal(card(S),card(T)),exists([F],member(F,total_bijection(S,T))),'SIMP_EQUAL_CARD') :- | |
| 564 | new_function(conjunct(S,T),F). | |
| 565 | simp_rule(member(0,Nat),falsity,'SIMP_SPECIAL_IN_NATURAL1') :- is_natural1_set(Nat). | |
| 566 | simp_rule(interval(I,J),empty_set,'SIMP_LIT_UPTO') :- number(I), number(J), I > J. | |
| 567 | simp_rule(member(NI,Nat),falsity,'SIMP_LIT_IN_MINUS_NATURAL') :- | |
| 568 | is_natural_set(Nat), | |
| 569 | (NI = unary_minus(I), number(I), I > 0 | |
| 570 | ; number(NI), NI < 0). | |
| 571 | simp_rule(member(NI,Nat),falsity,'SIMP_LIT_IN_MINUS_NATURAL1') :- | |
| 572 | is_natural1_set(Nat), | |
| 573 | (NI = unary_minus(I), number(I), I >= 0 | |
| 574 | ; number(NI), NI < 0). | |
| 575 | simp_rule(min(Nat),0,'SIMP_MIN_NATURAL') :- is_natural_set(Nat). | |
| 576 | simp_rule(min(Nat),1,'SIMP_MIN_NATURAL1') :- is_natural1_set(Nat). | |
| 577 | simp_rule(max(interval(_,F)),F,'SIMP_MAX_UPTO'). | |
| 578 | simp_rule(min(interval(E,_)),E,'SIMP_MIN_UPTO'). | |
| 579 | simp_rule(min(U),min(New),'SIMP_MIN_BUNION_SING') :- U = union(_,_), select_op(set_extension([min(T)]),U,T,New,union). | |
| 580 | simp_rule(max(U),max(New),'SIMP_MAX_BUNION_SING') :- U = union(_,_), select_op(set_extension([max(T)]),U,T,New,union). | |
| 581 | simp_rule(negation(P),Q,Rule) :- seperate_negate_rule(Rule,P), negate(P,Q). | |
| 582 | simp_rule(negation(P),Q,'Propagate negation') :- | |
| 583 | \+ seperate_negate_rule(_,P), | |
| 584 | negate(P,Q), | |
| 585 | Q \= negation(_). % De-Morgan and similar rules to propagate negation | |
| 586 | simp_rule(P,truth,'Evaluate tautology') :- is_true(P). | |
| 587 | simp_rule(E,NewE,Rule) :- is_empty(E,EmptyTerm), simp_empty_rule(EmptyTerm,NewE,Rule). | |
| 588 | simp_rule(E,NewE,Rule) :- is_equality(E,LHS,RHS), simp_equality(LHS,RHS,NewE,Rule). | |
| 589 | ||
| 590 | new_function(Expr,F) :- used_identifiers(Expr,L), possible_function(X), F = '$'(X), \+ member(F,L), !. | |
| 591 | ||
| 592 | func_id(f). | |
| 593 | func_id(g). | |
| 594 | func_id(h). | |
| 595 | ||
| 596 | possible_function(Z) :- func_id(Z). | |
| 597 | possible_function(Z) :- func_id(X), func_id(Y), atom_concat(X,Y,Z). | |
| 598 | ||
| 599 | seperate_negate_rule('SIMP_NOT_NOT',negation(_)). | |
| 600 | seperate_negate_rule('DISTRI_NOT_AND',conjunct(_,_)). | |
| 601 | seperate_negate_rule('DISTRI_NOT_OR',disjunct(_,_)). | |
| 602 | seperate_negate_rule('DERIV_NOT_IMP',implication(_,_)). | |
| 603 | ||
| 604 | ||
| 605 | overwrite_type([Ty|R],_,ListOut,Info) :- type_expression(Ty,Info), !, overwrite_type(R,[Ty],ListOut,Info). | |
| 606 | overwrite_type([S|R],Prev,ListOut,Info) :- append(Prev,[S],ListIn), overwrite_type(R,ListIn,ListOut,Info). | |
| 607 | overwrite_type([],L,L,_). | |
| 608 | ||
| 609 | change_sign(L,NL,Nr) :- remove_minus(L,NL,Nr), Nr > 0. | |
| 610 | ||
| 611 | remove_minus([NE|R],[E|T],NrN) :- is_minus(NE,E), remove_minus(R,T,Nr), NrN is Nr + 1, !. | |
| 612 | remove_minus([E|R],[E|T],Nr) :- remove_minus(R,T,Nr). | |
| 613 | remove_minus([],[],0). | |
| 614 | ||
| 615 | remove_unused_identifier(L,P,Used) :- | |
| 616 | member(Z,L), | |
| 617 | used_identifiers(P,Ids), | |
| 618 | member(Z,Ids), | |
| 619 | list_intersection(L,Ids,Used). | |
| 620 | ||
| 621 | ||
| 622 | min_list([H|T], Min) :- number(H) -> min_list(T,H,Min) ; min_list(T,Min). | |
| 623 | ||
| 624 | min_list([],Min,Min). | |
| 625 | min_list([H|T],Min0,Min) :- | |
| 626 | number(H),!, | |
| 627 | Min1 is min(H,Min0), | |
| 628 | min_list(T,Min1,Min). | |
| 629 | min_list([_|T],Min0,Min) :- | |
| 630 | min_list(T,Min0,Min). | |
| 631 | ||
| 632 | remove_greater(L,I,Res) :- only_min(L,I,[],Res). | |
| 633 | ||
| 634 | only_min([],_,List,List). | |
| 635 | only_min([E|R],I,Filtered, Res) :- | |
| 636 | \+ number(E),!, | |
| 637 | append(Filtered,[E],New), | |
| 638 | only_min(R,I,New,Res). | |
| 639 | only_min([E|R],I,Filtered,Res) :- | |
| 640 | E > I, | |
| 641 | only_min(R,I,Filtered,Res). | |
| 642 | only_min([E|R],I,Filtered,Res) :- | |
| 643 | E =:= I, | |
| 644 | member(E,Filtered), | |
| 645 | only_min(R,I,Filtered,Res). | |
| 646 | only_min([E|R],I,Filtered,Res) :- | |
| 647 | E =:= I, | |
| 648 | \+ member(E,Filtered), | |
| 649 | append(Filtered,[E],New), | |
| 650 | only_min(R,I,New,Res). | |
| 651 | ||
| 652 | max_list([H|T],Max) :- number(H) -> max_list(T,H,Max) ; max_list(T,Max). | |
| 653 | ||
| 654 | max_list([],Max,Max). | |
| 655 | max_list([H|T],Max0,Max) :- | |
| 656 | number(H),!, | |
| 657 | Max1 is max(H,Max0), | |
| 658 | max_list(T,Max1,Max). | |
| 659 | max_list([_|T],Max0,Max) :- | |
| 660 | max_list(T,Max0,Max). | |
| 661 | ||
| 662 | remove_smaller(L,I,Res) :- only_max(L,I,[],Res). | |
| 663 | ||
| 664 | only_max([],_,List,List). | |
| 665 | only_max([E|R],I,Filtered, Res) :- | |
| 666 | \+ number(E),!, | |
| 667 | append(Filtered,[E],New), | |
| 668 | only_max(R,I,New,Res). | |
| 669 | only_max([E|R],I,Filtered,Res) :- | |
| 670 | E < I, | |
| 671 | only_max(R,I,Filtered,Res). | |
| 672 | only_max([E|R],I,Filtered,Res) :- | |
| 673 | E =:= I, | |
| 674 | member(E,Filtered), | |
| 675 | only_max(R,I,Filtered,Res). | |
| 676 | only_max([E|R],I,Filtered,Res) :- | |
| 677 | E =:= I, | |
| 678 | \+ member(E,Filtered), | |
| 679 | append(Filtered,[E],New), | |
| 680 | only_max(R,I,New,Res). | |
| 681 | ||
| 682 | % ----------------- | |
| 683 | ||
| 684 | ||
| 685 | % simplification rules for equality | |
| 686 | % simp_equality(LHS,RHS,NewPred,'RuleName'). | |
| 687 | simp_equality(interval(_,_),Z,falsity,Rule) :- | |
| 688 | ( is_integer_set(Z) -> Rule = 'SIMP_UPTO_EQUAL_INTEGER' | |
| 689 | ; is_natural_set(Z) -> Rule = 'SIMP_UPTO_EQUAL_NATURAL' | |
| 690 | ; is_natural1_set(Z) -> Rule = 'SIMP_UPTO_EQUAL_NATURAL1'). | |
| 691 | simp_equality(convert_bool(P),boolean_true,P,'SIMP_LIT_EQUAL_KBOOL_TRUE'). | |
| 692 | simp_equality(convert_bool(P),boolean_false,negation(P),'SIMP_LIT_EQUAL_KBOOL_FALSE'). | |
| 693 | simp_equality(T,U,subset(NewU,T),'SIMP_MULTI_EQUAL_BUNION') :- | |
| 694 | member_of(union,T,U), | |
| 695 | remove_from_op(T,U,NewU,union). | |
| 696 | simp_equality(I,T,subset(T,NewI),'SIMP_MULTI_EQUAL_BINTER') :- | |
| 697 | member_of(intersection,T,I), | |
| 698 | remove_from_op(T,I,NewI,intersection). | |
| 699 | simp_equality(function(F,X),Y,member(couple(X,Y),F),'DEF_EQUAL_FUNIMAGE'). | |
| 700 | simp_equality(card(S),0,equal(S,empty_set),'SIMP_SPECIAL_EQUAL_CARD'). | |
| 701 | simp_equality(card(S),1,exists([X],equal(S,set_extension([X]))),'SIMP_LIT_EQUAL_CARD_1') :- | |
| 702 | new_identifier(S,X). | |
| 703 | simp_equality(card(S),K,member(F,total_bijection(interval(1,K),S)),'DEF_EQUAL_CARD') :- | |
| 704 | new_function(conjunct(S,K),F). | |
| 705 | simp_equality(E,min(S),conjunct(member(E,S),forall([X],member(X,S),less_equal(E,X))),'DEF_EQUAL_MIN') :- | |
| 706 | new_identifier(member(E,S),X). | |
| 707 | simp_equality(E,max(S),conjunct(member(E,S),forall([X],member(X,S),greater_equal(E,X))),'DEF_EQUAL_MAX') :- | |
| 708 | new_identifier(member(E,S),X). | |
| 709 | ||
| 710 | ||
| 711 | % candidates for SIMP_SPECIAL_REL_R rule rewriting to {{}} | |
| 712 | simp_relation_empty_range(relations(_,empty_set)). | |
| 713 | simp_relation_empty_range(surjection_relation(_,empty_set)). | |
| 714 | simp_relation_empty_range(partial_function(_,empty_set)). | |
| 715 | simp_relation_empty_range(partial_injection(_,empty_set)). | |
| 716 | simp_relation_empty_range(partial_surjection(_,empty_set)). | |
| 717 | ||
| 718 | % candidates for SIMP_SPECIAL_REL_L rule rewriting to {{}} | |
| 719 | simp_relation_empty_domain(relations(empty_set,_)). | |
| 720 | simp_relation_empty_domain(total_relation(empty_set,_)). | |
| 721 | simp_relation_empty_domain(partial_function(empty_set,_)). | |
| 722 | simp_relation_empty_domain(total_function(empty_set,_)). | |
| 723 | simp_relation_empty_domain(partial_injection(empty_set,_)). | |
| 724 | simp_relation_empty_domain(total_injection(empty_set,_)). | |
| 725 | ||
| 726 | % simplification rules for empty set equalities | |
| 727 | % simp_empty_rule(TermThatIsEmpty,NewPredicate,RuleName) | |
| 728 | simp_empty_rule(set_extension(L),Res,'SIMP_SETENUM_EQUAL_EMPTY') :- length(L,LL), | |
| 729 | (LL > 0 -> Res = falsity ; Res = truth). | |
| 730 | simp_empty_rule(interval(I,J),greater(I,J),'SIMP_UPTO_EQUAL_EMPTY'). | |
| 731 | simp_empty_rule(relations(_,_),falsity,'SIMP_SPECIAL_EQUAL_REL'). | |
| 732 | simp_empty_rule(total_relation(A,B),conjunct(negation(equal(A,empty_set)),equal(B,empty_set)),'SIMP_SPECIAL_EQUAL_RELDOM'). | |
| 733 | simp_empty_rule(total_function(A,B),conjunct(negation(equal(A,empty_set)),equal(B,empty_set)),'SIMP_SPECIAL_EQUAL_RELDOM'). | |
| 734 | simp_empty_rule(surjection_relation(A,B),conjunct(equal(A,empty_set),negation(equal(B,empty_set))), | |
| 735 | 'SIMP_SREL_EQUAL_EMPTY'). | |
| 736 | simp_empty_rule(total_surjection_relation(A,B),equivalence(equal(A,empty_set),negation(equal(B,empty_set))), | |
| 737 | 'SIMP_STREL_EQUAL_EMPTY'). | |
| 738 | simp_empty_rule(domain(R),equal(R,empty_set),'SIMP_DOM_EQUAL_EMPTY'). | |
| 739 | simp_empty_rule(range(R),equal(R,empty_set),'SIMP_RAN_EQUAL_EMPTY'). | |
| 740 | simp_empty_rule(composition(P,Q),equal(intersection(range(P),domain(Q)),empty_set),'SIMP_FCOMP_EQUAL_EMPTY'). | |
| 741 | simp_empty_rule(ring(P,Q),equal(intersection(range(Q),domain(P)),empty_set),'SIMP_BCOMP_EQUAL_EMPTY'). | |
| 742 | simp_empty_rule(domain_restriction(S,R),equal(intersection(domain(R),S),empty_set),'SIMP_DOMRES_EQUAL_EMPTY'). | |
| 743 | simp_empty_rule(domain_subtraction(S,R),subset(domain(R),S),'SIMP_DOMSUB_EQUAL_EMPTY'). | |
| 744 | simp_empty_rule(range_restriction(R,S),equal(intersection(range(R),S),empty_set),'SIMP_RANRES_EQUAL_EMPTY'). | |
| 745 | simp_empty_rule(range_subtraction(R,S),subset(range(R),S),'SIMP_RANSUB_EQUAL_EMPTY'). | |
| 746 | simp_empty_rule(reverse(R),equal(R,empty_set),'SIMP_CONVERSE_EQUAL_EMPTY'). | |
| 747 | simp_empty_rule(image(R,S),equal(domain_restriction(S,R),empty_set),'SIMP_RELIMAGE_EQUAL_EMPTY'). | |
| 748 | simp_empty_rule(overwrite(P,Q),Res,'SIMP_OVERL_EQUAL_EMPTY') :- | |
| 749 | and_empty(overwrite(P,Q),Res,overwrite). | |
| 750 | simp_empty_rule(direct_product(P,Q),equal(intersection(domain(P),domain(Q)),empty_set),'SIMP_DPROD_EQUAL_EMPTY'). | |
| 751 | simp_empty_rule(parallel_product(P,Q),disjunct(equal(P,empty_set),equal(Q,empty_set)),'SIMP_PPROD_EQUAL_EMPTY'). | |
| 752 | simp_empty_rule(event_b_identity,falsity,'SIMP_ID_EQUAL_EMPTY'). | |
| 753 | simp_empty_rule(event_b_first_projection_v2,falsity,'SIMP_PRJ1_EQUAL_EMPTY'). | |
| 754 | simp_empty_rule(event_b_second_projection_v2,falsity,'SIMP_PRJ2_EQUAL_EMPTY'). | |
| 755 | simp_empty_rule(cartesian_product(S,T),disjunct(equal(S,empty_set),equal(T,empty_set)),'SIMP_CPROD_EQUAL_EMPTY'). | |
| 756 | simp_empty_rule(quantified_union([X],P,E),forall([X],P,equal(E,empty_set)),'SIMP_QUNION_EQUAL_EMPTY'). | |
| 757 | simp_empty_rule(union(A,B),Res,'SIMP_BUNION_EQUAL_EMPTY') :- and_empty(union(A,B),Res,union). | |
| 758 | simp_empty_rule(set_subtraction(A,B),subset(A,B),'SIMP_SETMINUS_EQUAL_EMPTY'). | |
| 759 | simp_empty_rule(event_b_comprehension_set(Ids,_,P),forall(Ids,truth,negation(P)),'SIMP_SPECIAL_EQUAL_COMPSET'). | |
| 760 | simp_empty_rule(pow_subset(_),falsity,'SIMP_POW_EQUAL_EMPTY'). | |
| 761 | simp_empty_rule(pow1_subset(S),equal(S,empty_set),'SIMP_POW1_EQUAL_EMPTY'). % TODO: similar rules for FIN/FIN1 ? | |
| 762 | simp_empty_rule(general_union(S),subset(S,set_extension([empty_set])),'SIMP_KUNION_EQUAL_EMPTY'). | |
| 763 | simp_empty_rule(I,equal(set_subtraction(I0,C),empty_set),'SIMP_BINTER_SETMINUS_EQUAL_EMPTY') :- | |
| 764 | member_of(intersection,set_subtraction(B,C),I), | |
| 765 | select_op(minus(B,C),I,B,I0,intersection). | |
| 766 | simp_empty_rule(Nat,falsity,'SIMP_NATURAL_EQUAL_EMPTY') :- is_natural_set(Nat). | |
| 767 | simp_empty_rule(Nat,falsity,'SIMP_NATURAL1_EQUAL_EMPTY') :- is_natural1_set(Nat). | |
| 768 | %simp_empty_rule(TermThatIsEmpty,NewPred,RuleName). | |
| 769 | ||
| 770 | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_PLUS') :- | |
| 771 | Ex=..[Rel,L,R], | |
| 772 | comparison(Rel), | |
| 773 | R = add(_,_), | |
| 774 | member_of(add,El,L), | |
| 775 | select_op(El,L,L0,add), | |
| 776 | select_op(El,R,R0,add), | |
| 777 | Res=..[Rel,L0,R0]. | |
| 778 | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_R') :- | |
| 779 | Ex=..[Rel,C,R], | |
| 780 | comparison(Rel), | |
| 781 | R = add(_,_), | |
| 782 | select_op(C,R,R0,add), | |
| 783 | Res=..[Rel,0,R0]. | |
| 784 | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_L') :- | |
| 785 | Ex=..[Rel,L,C], | |
| 786 | comparison(Rel), | |
| 787 | L = add(_,_), | |
| 788 | select_op(C,L,L0,add), | |
| 789 | Res=..[Rel,L0,0]. | |
| 790 | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_R') :- | |
| 791 | Ex=..[Rel,L,R], | |
| 792 | comparison(Rel), | |
| 793 | L = minus(A,C1), | |
| 794 | R = minus(B,C2), | |
| 795 | equal_terms(C1,C2), | |
| 796 | Res=..[Rel,A,B]. | |
| 797 | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_L') :- | |
| 798 | Ex=..[Rel,L,R], | |
| 799 | comparison(Rel), | |
| 800 | L = minus(C1,A), | |
| 801 | R = minus(C2,B), | |
| 802 | equal_terms(C1,C2), | |
| 803 | Res=..[Rel,B,A]. | |
| 804 | ||
| 805 | select_summand(X,Y,0) :- equal_terms(X,Y). | |
| 806 | select_summand(add(L,R),X,ResTerm) :- select_summand(L,X,NewL), if_zero(NewL,R,add(NewL,R),ResTerm). | |
| 807 | select_summand(add(L,R),X,ResTerm) :- select_summand(R,X,NewR), if_zero(NewR,L,add(L,NewR),ResTerm). | |
| 808 | select_summand(minus(L,R),X,ResTerm) :- select_summand(L,X,NewL), if_zero(NewL,unary_minus(R),minus(NewL,R),ResTerm). | |
| 809 | ||
| 810 | select_subtrahend(MinusY,X,0) :- is_minus(MinusY,Y), equal_terms(X,Y). | |
| 811 | select_subtrahend(minus(Y,X),X,Y). | |
| 812 | select_subtrahend(add(MinusX,Y),X,Res) :- select_subtrahend(MinusX,X,NewR), if_zero(NewR,Y,add(NewR,Y),Res). | |
| 813 | select_subtrahend(add(Y,MinusX),X,Res) :- select_subtrahend(MinusX,X,NewR), if_zero(NewR,Y,add(Y,NewR),Res). | |
| 814 | select_subtrahend(minus(L,Y),X,Res) :- select_subtrahend(L,X,NewL), if_zero(NewL,unary_minus(Y),minus(NewL,Y),Res). | |
| 815 | ||
| 816 | if_zero(Term,Then,Else,Res) :- | |
| 817 | (Term = 0 | |
| 818 | -> Res = Then | |
| 819 | ; Res = Else). | |
| 820 | ||
| 821 | ||
| 822 | all_pairs(L,Pairs) :- findall([X,Y], (combination(L,[X,Y])), Pairs). | |
| 823 | ||
| 824 | combination(_,[]). | |
| 825 | combination([X|T],[X|C]) :- combination(T,C). | |
| 826 | combination([_|T],[X|C]) :- combination(T,[X|C]). | |
| 827 | ||
| 828 | ||
| 829 | all_in_set([E],S,Hyps) :- member_hyps(member(E,S),Hyps). | |
| 830 | all_in_set([E|R],S,Hyps) :- member_hyps(member(E,S),Hyps), all_in_set(R,S,Hyps). | |
| 831 | ||
| 832 | map_dom([couple(X,_)],[X]) :- !. | |
| 833 | map_dom([couple(X,_)|T],[X|R]) :- map_dom(T,R). | |
| 834 | ||
| 835 | map_ran([couple(_,A)],[A]) :- !. | |
| 836 | map_ran([couple(_,B)|T],[B|R]) :- map_ran(T,R). | |
| 837 | ||
| 838 | all_map_to([couple(_,F)],E) :- equal_terms(E,F), !. | |
| 839 | all_map_to([couple(_,F)|T],E) :- equal_terms(E,F), all_map_to(T,E). | |
| 840 | ||
| 841 | convert_map_to([couple(X,Y)],[couple(Y,X)]) :- !. | |
| 842 | convert_map_to([couple(X,Y)|T],[couple(Y,X)|R]) :- convert_map_to(T,R). | |
| 843 | ||
| 844 | list_subset([],_). | |
| 845 | list_subset([E|T],L) :- memberchk(E,L), list_subset(T,L). | |
| 846 | ||
| 847 | ||
| 848 | ||
| 849 | % ----------------- | |
| 850 | ||
| 851 | ||
| 852 | distri(C,Res,Op1,Op2) :- | |
| 853 | C=..[Op1,A,B], | |
| 854 | (X = A ; X = B), | |
| 855 | functor(X,Op2,2), | |
| 856 | distribute_op(C,X,Op1,Op2,Res). | |
| 857 | ||
| 858 | distri_r2(C,Res,Rule) :- | |
| 859 | C=..[Op1,_,X], | |
| 860 | functor(X,Op2,2), | |
| 861 | distri_r2_name(Op1,Op2,Rule), | |
| 862 | distribute_op(C,X,Op1,Op2,Res). | |
| 863 | distri_r2_name(ring,union,'DISTRI_BCOMP_BUNION'). | |
| 864 | distri_r2_name(direct_product,union,'DISTRI_DPROD_BUNION'). | |
| 865 | distri_r2_name(direct_product,set_subtraction,'DISTRI_DPROD_SETMINUS'). | |
| 866 | distri_r2_name(direct_product,intersection,'DISTRI_DPROD_BINTER'). | |
| 867 | distri_r2_name(direct_product,overwrite,'DISTRI_DPROD_OVERL'). | |
| 868 | distri_r2_name(parallel_product,union,'DISTRI_PPROD_BUNION'). | |
| 869 | distri_r2_name(parallel_product,intersection,'DISTRI_PPROD_BINTER'). | |
| 870 | distri_r2_name(parallel_product,set_subtraction,'DISTRI_PPROD_SETMINUS'). | |
| 871 | distri_r2_name(parallel_product,overwrite,'DISTRI_PPROD_OVERL'). | |
| 872 | distri_r2_name(domain_restriction,union,'DISTRI_DOMRES_BUNION_R'). | |
| 873 | distri_r2_name(domain_restriction,intersection,'DISTRI_DOMRES_BINTER_R'). | |
| 874 | distri_r2_name(domain_restriction,set_subtraction,'DISTRI_DOMRES_SETMINUS_R'). | |
| 875 | distri_r2_name(domain_restriction,direct_product,'DISTRI_DOMRES_DPROD'). | |
| 876 | distri_r2_name(domain_restriction,overwrite,'DISTRI_DOMRES_OVERL'). | |
| 877 | distri_r2_name(domain_subtraction,union,'DISTRI_DOMSUB_BUNION_R'). | |
| 878 | distri_r2_name(domain_subtraction,intersection,'DISTRI_DOMSUB_BINTER_R'). | |
| 879 | distri_r2_name(domain_subtraction,direct_product,'DISTRI_DOMSUB_DPROD'). | |
| 880 | distri_r2_name(domain_subtraction,overwrite,'DISTRI_DOMSUB_OVERL'). | |
| 881 | distri_r2_name(composition,union,'DISTRI_FCOMP_BUNION_R'). | |
| 882 | distri_r2_name(range_restriction,union,'DISTRI_RANRES_BUNION_R'). | |
| 883 | distri_r2_name(range_restriction,intersection,'DISTRI_RANRES_BINTER_R'). | |
| 884 | distri_r2_name(range_restriction,set_subtraction,'DISTRI_RANRES_SETMINUS_R'). | |
| 885 | ||
| 886 | distri_l2(C,Res,RuleName) :- | |
| 887 | distri_l2_arg1(C,Op1,X), | |
| 888 | functor(X,Op2,2), | |
| 889 | distri_l2_name(Op1,Op2,RuleName), | |
| 890 | distribute_op(C,X,Op1,Op2,Res). | |
| 891 | distri_l2_arg1(overwrite(X,_),overwrite,X). | |
| 892 | distri_l2_arg1(composition(X,_),composition,X). | |
| 893 | distri_l2_arg1(domain_restriction(X,_),domain_restriction,X). | |
| 894 | distri_l2_arg1(range_restriction(X,_),range_restriction,X). | |
| 895 | distri_l2_arg1(range_subtraction(X,_),range_subtraction,X). | |
| 896 | distri_l2_name(overwrite,union,'DISTRI_OVERL_BUNION_L'). | |
| 897 | distri_l2_name(overwrite,intersection,'DISTRI_OVERL_BINTER_L'). | |
| 898 | distri_l2_name(composition,union,'DISTRI_FCOMP_BUNION_L'). | |
| 899 | distri_l2_name(domain_restriction,union,'DISTRI_DOMRES_BUNION_L'). | |
| 900 | distri_l2_name(domain_restriction,intersection,'DISTRI_DOMRES_BINTER_L'). | |
| 901 | distri_l2_name(domain_restriction,set_subtraction,'DISTRI_DOMRES_SETMINUS_L'). | |
| 902 | distri_l2_name(range_restriction,union,'DISTRI_RANRES_BUNION_L'). | |
| 903 | distri_l2_name(range_restriction,intersection,'DISTRI_RANRES_BINTER_L'). | |
| 904 | distri_l2_name(range_restriction,set_subtraction,'DISTRI_RANRES_SETMINUS_L'). | |
| 905 | distri_l2_name(range_subtraction,union,'DISTRI_RANSUB_BUNION_L'). | |
| 906 | distri_l2_name(range_subtraction,intersection,'DISTRI_RANSUB_BINTER_L'). | |
| 907 | ||
| 908 | distribute_op(C,X,Op1,Op2,Res) :- | |
| 909 | op_to_list(X,L,Op2), | |
| 910 | distribute(C,X,L,CN,Op1), | |
| 911 | list_to_op(CN,Res,Op2). | |
| 912 | ||
| 913 | distribute(_,_,[],[],_). | |
| 914 | distribute(C,X,[D|T],[N|R],Op) :- select_op(X,C,D,N,Op), distribute(C,X,T,R,Op). | |
| 915 | ||
| 916 | distri_r3(C,Res,Rule) :- | |
| 917 | C = range_subtraction(_,X), Op1=range_subtraction, %C=..[Op1,_,X], | |
| 918 | distri_r3_name_ransub(Op2,Op3,Rule), | |
| 919 | distri_and_change(C,X,Op1,Op2,Op3,Res). | |
| 920 | distri_r3_name_ransub(union,intersection,'DISTRI_RANSUB_BUNION_R'). | |
| 921 | distri_r3_name_ransub(intersection,union,'DISTRI_RANSUB_BINTER_R'). | |
| 922 | ||
| 923 | distri_r3_info(C,Res,Rule,Info) :- | |
| 924 | C = set_subtraction(Ty,X), Op1=set_subtraction, | |
| 925 | type_expression(Ty,Info), | |
| 926 | distri_r3_name_setsub(Op2,Op3,Rule), | |
| 927 | distri_and_change(C,X,Op1,Op2,Op3,Res). | |
| 928 | distri_r3_name_setsub(intersection,union,'DERIV_TYPE_SETMINUS_BINTER'). % Ty \ (S /\ T) == (Ty \ S) \/ (Ty \ T) | |
| 929 | distri_r3_name_setsub(union,intersection,'DERIV_TYPE_SETMINUS_BUNION'). | |
| 930 | ||
| 931 | distri_l3(C,Res,Op1,Op2,Op3) :- | |
| 932 | C=..[Op1,X,_], | |
| 933 | distri_and_change(C,X,Op1,Op2,Op3,Res). | |
| 934 | ||
| 935 | % Op2 changes to Op3 | |
| 936 | distri_and_change(C,X,Op1,Op2,Op3,Res) :- | |
| 937 | functor(X,Op2,2), | |
| 938 | op_to_list(X,L,Op2), | |
| 939 | distribute(C,X,L,CN,Op1), | |
| 940 | list_to_op(CN,Res,Op3). | |
| 941 | ||
| 942 | distri_setminus(U,X,Res) :- | |
| 943 | C = set_subtraction(U,X), X = union(_,_), | |
| 944 | select_op(X,C,NewC,set_subtraction), | |
| 945 | op_to_list(NewC,CL,set_subtraction), | |
| 946 | op_to_list(X,L,union), | |
| 947 | append(CL,L,L2), | |
| 948 | list_to_op(L2,Res,set_subtraction). | |
| 949 | ||
| 950 | ||
| 951 | % ----------------- | |
| 952 | ||
| 953 | %simp_rule(X,X,'EQ'(F,N,X)) :- functor(X,F,N). | |
| 954 | ||
| 955 | % simp_rule/4 | |
| 956 | simp_rule(D,implication(negation(P),D0),'DEF_OR',OuterOp) :- OuterOp \= disjunct, D = disjunct(_,_), select_op(P,D,D0,disjunct). | |
| 957 | simp_rule(C,falsity,'SIMP_SPECIAL_AND_BFALSE',OuterOp) :- OuterOp \= conjunct, | |
| 958 | member_of_bin_op(conjunct,falsity,C). | |
| 959 | simp_rule(D,truth,'SIMP_SPECIAL_OR_BTRUE',OuterOp) :- OuterOp \= disjunct, | |
| 960 | member_of_bin_op(disjunct,truth,D). | |
| 961 | simp_rule(C,Res,'SIMP_MULTI_AND',OuterOp) :- OuterOp \= conjunct, remove_duplicates_for_op(C,Res,conjunct). | |
| 962 | simp_rule(D,Res,'SIMP_MULTI_OR',OuterOp) :- OuterOp \= disjunct, remove_duplicates_for_op(D,Res,disjunct). | |
| 963 | simp_rule(C,falsity,'SIMP_MULTI_AND_NOT',OuterOp) :- | |
| 964 | OuterOp \= conjunct, | |
| 965 | member_of(conjunct,Q,C), | |
| 966 | member_of(conjunct,NotQ,C), | |
| 967 | is_negation(Q,NotQ). | |
| 968 | simp_rule(D,truth,'SIMP_MULTI_OR_NOT',OuterOp) :- | |
| 969 | OuterOp \= disjunct, | |
| 970 | member_of(disjunct,Q,D), | |
| 971 | member_of(disjunct,NotQ,D), | |
| 972 | is_negation(Q,NotQ). | |
| 973 | simp_rule(I,empty_set,'SIMP_SPECIAL_BINTER',OuterOp) :- OuterOp \= intersection, | |
| 974 | member_of_bin_op(intersection,empty_set,I). | |
| 975 | simp_rule(I,Res,'SIMP_MULTI_BINTER',OuterOp) :- OuterOp \= intersection, remove_duplicates_for_op(I,Res,intersection). | |
| 976 | simp_rule(U,Res,'SIMP_MULTI_BUNION',OuterOp) :- OuterOp \= union, remove_duplicates_for_op(U,Res,union). | |
| 977 | simp_rule(C,empty_set,'SIMP_SPECIAL_CPROD',OuterOp) :- OuterOp \= cartesian_product, % SIMP_SPECIAL_CPROD_L / SIMP_SPECIAL_CPROD_R | |
| 978 | member_of_bin_op(cartesian_product,empty_set,C). | |
| 979 | simp_rule(C,empty_set,'SIMP_SPECIAL_FCOMP',OuterOp) :- OuterOp \= composition, | |
| 980 | member_of_bin_op(composition,empty_set,C). | |
| 981 | simp_rule(Comp,empty_set,'SIMP_SPECIAL_BCOMP',OuterOp) :- OuterOp \= ring, | |
| 982 | member_of_bin_op(ring,empty_set,Comp). | |
| 983 | simp_rule(C,Res,'DEF_BCOMP',OuterOp) :- OuterOp \= ring, C = ring(_,_), | |
| 984 | bwd_to_fwd_comp(C,Comp), reorder(Comp,Res,composition). | |
| 985 | simp_rule(P,0,'SIMP_SPECIAL_PROD_0',OuterOp) :- OuterOp \= multiplication, member_of(multiplication,0,P). | |
| 986 | simp_rule(ring(P,Q),Res,'SIMP_BCOMP_ID',OuterOp) :- OuterOp \= ring, | |
| 987 | op_to_list(ring(P,Q),List,ring), | |
| 988 | rewrite_comp_id(List,List2), | |
| 989 | list_to_op(List2,Res,ring). | |
| 990 | simp_rule(composition(P,Q),Res,'SIMP_FCOMP_ID',OuterOp) :- OuterOp \= composition, | |
| 991 | op_to_list(composition(P,Q),List,composition), | |
| 992 | rewrite_comp_id(List,List2), | |
| 993 | list_to_op(List2,Res,composition). | |
| 994 | simp_rule(Comp,Res,'DERIV_FCOMP_DOMRES',OuterOp) :- OuterOp \= composition, deriv_fcomp_dom(Comp,domain_restriction,Res). | |
| 995 | simp_rule(Comp,Res,'DERIV_FCOMP_DOMSUB',OuterOp) :- OuterOp \= composition, deriv_fcomp_dom(Comp,domain_subtraction,Res). | |
| 996 | simp_rule(Comp,Res,'DERIV_FCOMP_RANRES',OuterOp) :- OuterOp \= composition, deriv_fcomp_ran(Comp,range_restriction,Res). | |
| 997 | simp_rule(Comp,Res,'DERIV_FCOMP_RANSUB',OuterOp) :- OuterOp \= composition, deriv_fcomp_ran(Comp,range_subtraction,Res). | |
| 998 | ||
| 999 | ||
| 1000 | deriv_fcomp_dom(Comp,Functor,Res) :- | |
| 1001 | Comp = composition(_,_), | |
| 1002 | op_to_list(Comp,List,composition), | |
| 1003 | append(L,[At|R],List), | |
| 1004 | At=..[Functor,P,Q], | |
| 1005 | list_to_op([Q|R],RComp,composition), | |
| 1006 | New=..[Functor,P,RComp], | |
| 1007 | append(L,[New],ResList), | |
| 1008 | list_to_op(ResList,Res,composition). | |
| 1009 | ||
| 1010 | deriv_fcomp_ran(Comp,Functor,Res) :- | |
| 1011 | Comp = composition(_,_), | |
| 1012 | op_to_list(Comp,List,composition), | |
| 1013 | append(L,[At|R],List), | |
| 1014 | At=..[Functor,P,Q], | |
| 1015 | append(L,[P],NewL), | |
| 1016 | list_to_op(NewL,LComp,composition), | |
| 1017 | New=..[Functor,LComp,Q], | |
| 1018 | list_to_op([New|R],Res,composition). | |
| 1019 | ||
| 1020 | rewrite_comp_id([X],[X]). | |
| 1021 | rewrite_comp_id([domain_restriction(S,event_b_identity),domain_restriction(T,event_b_identity)|R],Res) :- !, | |
| 1022 | rewrite_comp_id([domain_restriction(intersection(S,T),event_b_identity)|R],Res). | |
| 1023 | rewrite_comp_id([domain_restriction(S,event_b_identity),domain_subtraction(T,event_b_identity)|R],Res) :- !, | |
| 1024 | rewrite_comp_id([domain_restriction(set_subtraction(S,T),event_b_identity)|R],Res). | |
| 1025 | rewrite_comp_id([domain_subtraction(S,event_b_identity),domain_subtraction(T,event_b_identity)|R],Res) :- !, | |
| 1026 | rewrite_comp_id([domain_subtraction(union(S,T),event_b_identity)|R],Res). | |
| 1027 | rewrite_comp_id([E,F|R], [E|Res]) :- rewrite_comp_id([F|R],Res). | |
| 1028 | ||
| 1029 | ||
| 1030 | % simp_rule_with_info/4 | |
| 1031 | simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_DOMSUB_EQUAL_TYPE',Info) :- | |
| 1032 | is_equality(Eq,domain_subtraction(S,R),Ty), | |
| 1033 | type_expression(Ty,Info). | |
| 1034 | simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_RANSUB_EQUAL_TYPE',Info) :- | |
| 1035 | is_equality(Eq,range_subtraction(R,S),Ty), | |
| 1036 | type_expression(Ty,Info). | |
| 1037 | simp_rule_with_info(Eq,equal(R,reverse(Ty)),'SIMP_CONVERSE_EQUAL_TYPE',Info) :- | |
| 1038 | is_equality(Eq,reverse(R),Ty), | |
| 1039 | type_expression(Ty,Info). | |
| 1040 | simp_rule_with_info(subset(_,Ty),truth,'SIMP_TYPE_SUBSETEQ',Info) :- type_expression(Ty,Info). | |
| 1041 | simp_rule_with_info(set_subtraction(_,Ty),empty_set,'SIMP_TYPE_SETMINUS',Info) :- type_expression(Ty,Info). | |
| 1042 | simp_rule_with_info(set_subtraction(Ty,set_subtraction(Ty,S)),S,'SIMP_TYPE_SETMINUS_SETMINUS',Info) :- type_expression(Ty,Info). | |
| 1043 | simp_rule_with_info(member(_,Ty),truth,'SIMP_TYPE_IN',Info) :- type_expression(Ty,Info). | |
| 1044 | simp_rule_with_info(subset_strict(S,Ty),not_equal(S,Ty),'SIMP_TYPE_SUBSET_L',Info) :- type_expression(Ty,Info). | |
| 1045 | simp_rule_with_info(Eq,conjunct(equal(A,Ty),equal(B,empty_set)),'SIMP_SETMINUS_EQUAL_TYPE',Info) :- | |
| 1046 | is_equality(Eq,set_subtraction(A,B),Ty), | |
| 1047 | type_expression(Ty,Info). | |
| 1048 | simp_rule_with_info(Eq,Res,'SIMP_BINTER_EQUAL_TYPE',Info) :- | |
| 1049 | is_equality(Eq,I,Ty), | |
| 1050 | I = intersection(_,_), | |
| 1051 | type_expression(Ty,Info), | |
| 1052 | and_equal_type(I,Ty,Res). | |
| 1053 | simp_rule_with_info(Eq,equal(S,set_extension([Ty])),'SIMP_KINTER_EQUAL_TYPE',Info) :- | |
| 1054 | is_equality(Eq,general_intersection(S),Ty), | |
| 1055 | type_expression(Ty,Info). | |
| 1056 | simp_rule_with_info(Expr,falsity,'SIMP_TYPE_EQUAL_EMPTY',Info) :- is_empty(Expr,Ty), type_expression(Ty,Info). | |
| 1057 | simp_rule_with_info(Eq,forall([X],P,equal(E,Ty)),'SIMP_QINTER_EQUAL_TYPE',Info) :- | |
| 1058 | is_equality(Eq,quantified_intersection([X],P,E),Ty), | |
| 1059 | type_expression(Ty,Info). | |
| 1060 | simp_rule_with_info(intersection(A,B),S,'SIMP_TYPE_BINTER',Info) :- sym_unify(A,B,S,Ty), type_expression(Ty,Info). | |
| 1061 | simp_rule_with_info(Eq,falsity,'SIMP_TYPE_EQUAL_RELDOMRAN',Info) :- | |
| 1062 | is_equality(Eq,R,Ty), | |
| 1063 | type_expression(Ty,Info), | |
| 1064 | is_rel(R,_,_,_), | |
| 1065 | functor(R,Op,2), | |
| 1066 | \+ member(Op,[relations,partial_function,partial_injection]). % TODO: use facts without functor | |
| 1067 | simp_rule_with_info(member(Prj,RT),truth,Rule,Info) :- | |
| 1068 | (Prj = event_b_first_projection_v2, Rule = 'DERIV_PRJ1_SURJ' | |
| 1069 | ; Prj = event_b_second_projection_v2, Rule = 'DERIV_PRJ2_SURJ'), | |
| 1070 | is_rel(RT,_,Ty1,Ty2), | |
| 1071 | \+ is_inj(RT,Ty1,Ty2), | |
| 1072 | type_expression(Ty1,Info), | |
| 1073 | type_expression(Ty2,Info). | |
| 1074 | simp_rule_with_info(member(event_b_identity,RT),truth,'DERIV_ID_BIJ',Info) :- is_rel(RT,_,Ty,Ty), type_expression(Ty,Info). | |
| 1075 | simp_rule_with_info(domain_restriction(Ty,R),R,'SIMP_TYPE_DOMRES',Info) :- type_expression(Ty,Info). | |
| 1076 | simp_rule_with_info(range_restriction(R,Ty),R,'SIMP_TYPE_RANRES',Info) :- type_expression(Ty,Info). | |
| 1077 | simp_rule_with_info(domain_subtraction(Ty,R),R,'SIMP_TYPE_DOMSUB',Info) :- type_expression(Ty,Info). | |
| 1078 | simp_rule_with_info(range_subtraction(R,Ty),R,'SIMP_TYPE_RANSUB',Info) :- type_expression(Ty,Info). | |
| 1079 | simp_rule_with_info(image(R,Ty),range(R),'SIMP_TYPE_RELIMAGE',Info) :- type_expression(Ty,Info). | |
| 1080 | simp_rule_with_info(composition(R,Ty),cartesian_product(domain(R),Tb),'SIMP_TYPE_FCOMP_R',Info) :- | |
| 1081 | type_expression(Ty,Info), | |
| 1082 | Ty = cartesian_product(_,Tb). | |
| 1083 | simp_rule_with_info(composition(Ty,R),cartesian_product(Ta,range(R)),'SIMP_TYPE_FCOMP_L',Info) :- | |
| 1084 | type_expression(Ty,Info), | |
| 1085 | Ty = cartesian_product(Ta,_). | |
| 1086 | simp_rule_with_info(ring(Ty,R),cartesian_product(domain(R),Tb),'SIMP_TYPE_BCOMP_L',Info) :- | |
| 1087 | type_expression(Ty,Info), | |
| 1088 | Ty = cartesian_product(_,Tb). | |
| 1089 | simp_rule_with_info(ring(R,Ty),cartesian_product(Ta,range(R)),'SIMP_TYPE_BCOMP_R',Info) :- | |
| 1090 | type_expression(Ty,Info), | |
| 1091 | Ty = cartesian_product(Ta,_). | |
| 1092 | simp_rule_with_info(domain(Ty),Ta,'SIMP_TYPE_DOM',Info) :- Ty = cartesian_product(Ta,_), type_expression(Ty,Info). | |
| 1093 | simp_rule_with_info(range(Ty),Tb,'SIMP_TYPE_RAN',Info) :- Ty = cartesian_product(_,Tb), type_expression(Ty,Info). | |
| 1094 | simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(T,Tb)),'SIMP_CPROD_EQUAL_TYPE',Info) :- | |
| 1095 | is_equality(Eq,cartesian_product(S,T),Ty), | |
| 1096 | Ty = cartesian_product(Ta,Tb), | |
| 1097 | type_expression(Ty,Info). | |
| 1098 | simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(T,Tb)),'SIMP_TYPE_EQUAL_REL',Info) :- | |
| 1099 | is_equality(Eq,relations(S,T),Ty), | |
| 1100 | Ty = cartesian_product(Ta,Tb), | |
| 1101 | type_expression(Ty,Info). | |
| 1102 | simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(R,Ty)),'SIMP_DOMRES_EQUAL_TYPE',Info) :- | |
| 1103 | is_equality(Eq,domain_restriction(S,R),Ty), | |
| 1104 | Ty = cartesian_product(Ta,_), | |
| 1105 | type_expression(Ty,Info). | |
| 1106 | simp_rule_with_info(Eq,conjunct(equal(S,Tb),equal(R,Ty)),'SIMP_RANRES_EQUAL_TYPE',Info) :- | |
| 1107 | is_equality(Eq,range_restriction(R,S),Ty), | |
| 1108 | Ty = cartesian_product(_,Tb), | |
| 1109 | type_expression(Ty,Info). | |
| 1110 | simp_rule_with_info(Eq,conjunct(equal(P,cartesian_product(Ta,Tb)),equal(Q,cartesian_product(Ta,Tc))),'SIMP_DPROD_EQUAL_TYPE',Info) :- | |
| 1111 | is_equality(Eq,direct_product(P,Q),Ty), | |
| 1112 | Ty = cartesian_product(Ta,cartesian_product(Tb,Tc)), | |
| 1113 | type_expression(Ty,Info). | |
| 1114 | simp_rule_with_info(Eq,conjunct(equal(P,cartesian_product(Ta,Tc)),equal(Q,cartesian_product(Tb,Td))),'SIMP_PPROD_EQUAL_TYPE',Info) :- | |
| 1115 | is_equality(Eq,parallel_product(P,Q),Ty), | |
| 1116 | Ty = cartesian_product(cartesian_product(Ta,Tb),cartesian_product(Tc,Td)), | |
| 1117 | type_expression(Ty,Info). | |
| 1118 | simp_rule_with_info(set_subtraction(Ty,set_subtraction(S,T)),union(set_subtraction(Ty,S),T),'DERIV_TYPE_SETMINUS_SETMINUS',Info) :- | |
| 1119 | type_expression(Ty,Info). | |
| 1120 | simp_rule_with_info(Ex,disjunct(less(E,F),greater(E,F)),'DERIV_NOT_EQUAL',Info) :- | |
| 1121 | (Ex = negation(equal(E,F)) ; Ex = not_equal(E,F)), | |
| 1122 | get_meta_info(ids_types,Info,IdsTypes), | |
| 1123 | check_type(E,F,IdsTypes,integer). | |
| 1124 | simp_rule_with_info(equal(S,T),conjunct(subset(S,T),subset(T,S)),'DERIV_EQUAL',Info) :- | |
| 1125 | get_meta_info(ids_types,Info,IdsTypes), | |
| 1126 | check_type(S,T,IdsTypes,set(_)). | |
| 1127 | simp_rule_with_info(subset(S,T),subset(set_subtraction(Ty,T),set_subtraction(Ty,S)),'DERIV_SUBSETEQ',Info) :- | |
| 1128 | get_meta_info(ids_types,Info,IdsTypes), | |
| 1129 | check_type(S,T,IdsTypes,Type), | |
| 1130 | get_type_expression(Type,pow_subset(Ty)). | |
| 1131 | simp_rule_with_info(E,couple(function(event_b_first_projection_v2,E),function(event_b_second_projection_v2,E)),'DERIV_EXPAND_PRJS',Info) :- | |
| 1132 | \+ atomic(E), | |
| 1133 | get_meta_info(ids_types,Info,IdsTypes), | |
| 1134 | check_type(E,IdsTypes,couple(_,_)). | |
| 1135 | /* simp_rule_with_info(event_b_comprehension_set(Ids,E,truth),Ty,'SIMP_SPECIAL_COMPSET_BTRUE',Info) :- | |
| 1136 | get_meta_info(ids_types,Info,IdsTypes), % IdsTypes does not contain bound identifiers | |
| 1137 | pairwise_distict(E,Ids), | |
| 1138 | check_type(E,IdsTypes,Type), | |
| 1139 | get_type_expression(Type,Ty). */ | |
| 1140 | simp_rule_with_info(C,Res,Rule,Info) :- distri_r3_info(C,Res,Rule,Info). | |
| 1141 | ||
| 1142 | ||
| 1143 | %pairwise_distict(E,Ids) :- pairwise_distict(E,Ids,_). | |
| 1144 | % | |
| 1145 | %pairwise_distict(couple(E,F),Ids,Ids1) :- pairwise_distict(E,Ids,Ids0), pairwise_distict(F,Ids0,Ids1). | |
| 1146 | %pairwise_distict(E,Ids,Ids0) :- E = '$'(X), atomic(X), select(E,Ids,Ids0). | |
| 1147 | ||
| 1148 | check_type('$'(S),_,IdsTypes,Type) :- !, member(b(identifier(S),Type,_),IdsTypes). | |
| 1149 | check_type(_,'$'(T),IdsTypes,Type) :- !, member(b(identifier(T),Type,_),IdsTypes). | |
| 1150 | check_type(S,_,IdsTypes,Type) :- check_type(S,IdsTypes,Type). | |
| 1151 | ||
| 1152 | check_type(S,IdsTypes,Type) :- | |
| 1153 | new_aux_identifier(IdsTypes,X), | |
| 1154 | get_typed_identifiers(equal('$'(X),S),[identifier(IdsTypes)],L), | |
| 1155 | member(b(identifier(X),Type,_),L). | |
| 1156 | ||
| 1157 | ||
| 1158 | % simp_rule_with_descr/4 | |
| 1159 | simp_rule_with_descr(couple(function(event_b_first_projection_v2,E),function(event_b_second_projection_v2,F)),E,Rule,Rule) :- | |
| 1160 | Rule = 'SIMP_MAPSTO_PRJ1_PRJ2', | |
| 1161 | equal_terms(E,F). | |
| 1162 | simp_rule_with_descr(domain(successor),Z,Rule,Rule) :- Rule = 'SIMP_DOM_SUCC', is_integer_set(Z). | |
| 1163 | simp_rule_with_descr(range(successor),Z,Rule,Rule) :- Rule = 'SIMP_RAN_SUCC', is_integer_set(Z). | |
| 1164 | simp_rule_with_descr(predecessor,reverse(successor),Rule,Rule) :- Rule = 'DEF_PRED'. | |
| 1165 | simp_rule_with_descr(Expr,negation(member(A,SetB)),'SIMP_BINTER_SING_EQUAL_EMPTY'(A),Descr) :- | |
| 1166 | is_empty(Expr,Inter), | |
| 1167 | is_inter(Inter,SetA,SetB), | |
| 1168 | singleton_set(SetA,A), | |
| 1169 | create_descr('SIMP_BINTER_SING_EQUAL_EMPTY',A,Descr). | |
| 1170 | ||
| 1171 | ||
| 1172 | ||
| 1173 | % simp_rule_with_hyps/4 without info | |
| 1174 | simp_rule_with_hyps(domain(R),E,'DERIV_DOM_TOTALREL'(E),Hyps) :- % derive domain of a total relation | |
| 1175 | member_hyps(member(R,FT),Hyps), is_rel(FT,total,E,_). | |
| 1176 | simp_rule_with_hyps(range(R),F,'DERIV_RAN_SURJREL'(F),Hyps) :- % derive range of a surjective relation | |
| 1177 | member_hyps(member(R,FT),Hyps), is_surj(FT,_,F). | |
| 1178 | simp_rule_with_hyps(function(domain_restriction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMRES',Hyps) :- | |
| 1179 | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). | |
| 1180 | simp_rule_with_hyps(function(domain_subtraction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMSUB',Hyps) :- | |
| 1181 | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). | |
| 1182 | simp_rule_with_hyps(function(range_restriction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANRES',Hyps) :- | |
| 1183 | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). | |
| 1184 | simp_rule_with_hyps(function(range_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANSUB',Hyps) :- | |
| 1185 | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). | |
| 1186 | simp_rule_with_hyps(function(set_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_SETMINUS',Hyps) :- | |
| 1187 | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). | |
| 1188 | simp_rule_with_hyps(card(set_subtraction(S,T)),minus(card(S),card(T)),'SIMP_CARD_SETMINUS',Hyps) :- | |
| 1189 | member_hyps(subset(T,S),Hyps), | |
| 1190 | (member_hyps(finite(T),Hyps) | |
| 1191 | ; member_hyps(finite(S),Hyps)). | |
| 1192 | simp_rule_with_hyps(card(set_subtraction(S,set_extension(L))),minus(card(S),card(set_extension(L))),Rule,Hyps) :- | |
| 1193 | Rule = 'SIMP_CARD_SETMINUS_SETENUM', | |
| 1194 | all_in_set(L,S,Hyps). | |
| 1195 | simp_rule_with_hyps(L,less(A,B),'DERIV_LESS',Hyps) :- % A<=B & A/=B => A<B, own rule (not in Rodin Event-B Wiki) | |
| 1196 | is_less_eq(L,A,B), is_inequality(Ex,A,B), member(Ex,Hyps). | |
| 1197 | % allow simplifications deeper inside the term: | |
| 1198 | simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,P], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,Q]. | |
| 1199 | simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,P,R], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,Q,R]. | |
| 1200 | simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,R,P], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,R,Q]. | |
| 1201 | ||
| 1202 | ||
| 1203 | % ----------------------- | |
| 1204 | ||
| 1205 | or_equal([],_,D,D). | |
| 1206 | or_equal([A|L],E,D,Res) :- or_equal(L,E,disjunct(D,equal(E,A)),Res). | |
| 1207 | ||
| 1208 | and_empty(C,Conj,Op) :- C=..[Op,A,B], and_empty(A,ConjA,Op), and_empty(B,ConjB,Op), !, Conj = conjunct(ConjA,ConjB). | |
| 1209 | and_empty(A,equal(A,empty_set),_). | |
| 1210 | ||
| 1211 | and_imp(C,R,Conj,Op) :- C=..[Op,A,B], and_imp(A,R,ConjA,Op), and_imp(B,R,ConjB,Op), !, Conj = conjunct(ConjA,ConjB). | |
| 1212 | and_imp(A,R,implication(R,A),conjunct). | |
| 1213 | and_imp(A,R,implication(A,R),disjunct). | |
| 1214 | ||
| 1215 | union_subset(S,union(A,B),Conj) :- union_subset(S,A,ConjA), union_subset(S,B,ConjB), !, Conj = conjunct(ConjA,ConjB). | |
| 1216 | union_subset(S,A,subset(A,S)). | |
| 1217 | ||
| 1218 | union_subset_member(T,union(A,B),Conj) :- | |
| 1219 | union_subset_member(T,A,ConjA), | |
| 1220 | union_subset_member(T,B,ConjB),!, | |
| 1221 | Conj = conjunct(ConjA,ConjB). | |
| 1222 | union_subset_member(T,SetF,member(F,T)) :- singleton_set(SetF,F), !. | |
| 1223 | union_subset_member(T,A,subset(A,T)). | |
| 1224 | ||
| 1225 | ||
| 1226 | member_union(E,union(A,B),Disj) :- member_union(E,A,DisjA), member_union(E,B,DisjB), !, Disj = disjunct(DisjA,DisjB). | |
| 1227 | member_union(E,A,member(E,A)). | |
| 1228 | ||
| 1229 | subset_inter(S,intersection(A,B),Conj) :- subset_inter(S,A,ConjA), subset_inter(S,B,ConjB), Conj = conjunct(ConjA,ConjB), !. | |
| 1230 | subset_inter(S,A,subset(S,A)). | |
| 1231 | ||
| 1232 | member_intersection(E,intersection(A,B),Conj) :- | |
| 1233 | member_intersection(E,A,ConjA), | |
| 1234 | member_intersection(E,B,ConjB),!, | |
| 1235 | Conj = conjunct(ConjA,ConjB). | |
| 1236 | member_intersection(E,A,member(E,A)). | |
| 1237 | ||
| 1238 | distribute_exists(X,disjunct(A,B),Disj) :- distribute_exists(X,A,DisjA), distribute_exists(X,B,DisjB), !, Disj = disjunct(DisjA,DisjB). | |
| 1239 | distribute_exists(X,P,exists(X,P)). | |
| 1240 | ||
| 1241 | distribute_forall(X,P,conjunct(A,B),Conj) :- | |
| 1242 | distribute_forall(X,P,A,ConjA), | |
| 1243 | distribute_forall(X,P,B,ConjB),!, | |
| 1244 | Conj = conjunct(ConjA,ConjB). | |
| 1245 | distribute_forall(X,P,A,forall(X,P,A)). | |
| 1246 | ||
| 1247 | distribute_binary_minus(minus(X,Y),add(X,YY)) :- distribute_unary_minus(Y,YY). | |
| 1248 | ||
| 1249 | distribute_unary_minus(add(Y,Z),minus(YY,Z)) :- !, distribute_unary_minus(Y,YY). | |
| 1250 | distribute_unary_minus(minus(Y,Z),add(YY,Z)) :- !, distribute_unary_minus(Y,YY). | |
| 1251 | distribute_unary_minus(add(unary_minus(Y),Z),minus(YY,Z)) :- !, distribute_unary_minus(unary_minus(Y),YY). | |
| 1252 | distribute_unary_minus(minus(unary_minus(Y),Z),add(YY,Z)) :- !, distribute_unary_minus(unary_minus(Y),YY). | |
| 1253 | distribute_unary_minus(unary_minus(Y),Y) :- !. | |
| 1254 | distribute_unary_minus(Y,unary_minus(Y)). | |
| 1255 | ||
| 1256 | ||
| 1257 | left_associate_additions(add(X,Expr),Res) :- | |
| 1258 | \+ leftmost_term(Expr,_,_), !, | |
| 1259 | normalize_minus(add(X,Expr),Res). | |
| 1260 | left_associate_additions(add(X,Expr),Res) :- | |
| 1261 | leftmost_term(Expr,Term,Rest), !, | |
| 1262 | normalize_minus(add(add(X,Term),Rest),NewTerm), | |
| 1263 | left_associate_additions(NewTerm,Res). | |
| 1264 | left_associate_additions(X,X). | |
| 1265 | ||
| 1266 | leftmost_term(C,Term,Res) :- | |
| 1267 | C=..[Op,A,B], (Op = add ; Op = minus), | |
| 1268 | functor(A,OpA,2), (OpA = add ; OpA = minus),!, | |
| 1269 | leftmost_term(A,Term,Rest), | |
| 1270 | Res=..[Op,Rest,B]. | |
| 1271 | leftmost_term(add(X,Y),X,Y). | |
| 1272 | leftmost_term(minus(X,Y),X,unary_minus(Y)). | |
| 1273 | ||
| 1274 | normalize_minus(add(X,unary_minus(Y)),minus(XX,Y)) :- !, | |
| 1275 | normalize_minus(X,XX). | |
| 1276 | normalize_minus(Term,Result) :- | |
| 1277 | Term=..[F|Args], !, | |
| 1278 | maplist(normalize_minus,Args,NewArgs), | |
| 1279 | Result=..[F|NewArgs]. | |
| 1280 | normalize_minus(X,X). | |
| 1281 | ||
| 1282 | member_couples(E,F,[Q],_,[member(couple(E,F),Q)]). | |
| 1283 | member_couples(E,F,[P|Q],[X|T],[member(couple(E,X),P)|R]) :- member_couples(X,F,Q,T,R). | |
| 1284 | ||
| 1285 | distri_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse(A,UA,Op), distri_reverse(B,UB,Op), !, U=..[Op,UA,UB]. | |
| 1286 | distri_reverse(A,reverse(A),_). | |
| 1287 | ||
| 1288 | distri_reverse_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse_reverse(A,UA,Op), distri_reverse_reverse(B,UB,Op), !, U=..[Op,UB,UA]. | |
| 1289 | distri_reverse_reverse(A,reverse(A),_). | |
| 1290 | ||
| 1291 | distri_union(union(A,B),Union,Op) :- distri_union(A,L,Op), distri_union(B,R,Op), !, Union = union(L,R). | |
| 1292 | distri_union(A,C,Op) :- C=..[Op,A]. | |
| 1293 | ||
| 1294 | image_union(F,union(A,B),Union) :- image_union(F,A,L), image_union(F,B,R), !, Union = union(L,R). | |
| 1295 | image_union(F,A,image(F,A)). | |
| 1296 | ||
| 1297 | union_image(union(A,B),S,Union) :- union_image(A,S,L), union_image(B,S,R), !, Union = union(L,R). | |
| 1298 | union_image(A,S,image(A,S)). | |
| 1299 | ||
| 1300 | finite_union(union(A,B),Conj) :- finite_union(A,ConjA), finite_union(B,ConjB), !, Conj = conjunct(ConjA,ConjB). | |
| 1301 | finite_union(S,finite(S)). | |
| 1302 | ||
| 1303 | ||
| 1304 | last_overwrite(overwrite(_,B),Res) :- !, last_overwrite(B,Res). | |
| 1305 | last_overwrite(B,B). | |
| 1306 | ||
| 1307 | and_equal_type(intersection(A,B),Ty,Conj) :- and_equal_type(A,Ty,L), and_equal_type(B,Ty,R), !, Conj = conjunct(L,R). | |
| 1308 | and_equal_type(A,Ty,equal(A,Ty)). | |
| 1309 | ||
| 1310 | bwd_to_fwd_comp(ring(R,S),Res) :- | |
| 1311 | bwd_to_fwd_comp(R,R2), | |
| 1312 | bwd_to_fwd_comp(S,S2), | |
| 1313 | Res = composition(S2,R2). | |
| 1314 | bwd_to_fwd_comp(X,X) :- X \= ring(_,_). | |
| 1315 | ||
| 1316 | % ------------------ | |
| 1317 | ||
| 1318 | % change order of operation if Op is associative | |
| 1319 | reorder(C,Res,Op) :- | |
| 1320 | C=..[Op,A,B], | |
| 1321 | B=..[Op,L,Rest],!, | |
| 1322 | R=..[Op,A,L], | |
| 1323 | append_to_op(Rest,R,Res,Op). | |
| 1324 | reorder(C,C,Op) :- functor(C,Op,2). | |
| 1325 | ||
| 1326 | append_to_op(C,R,Res,Op) :- | |
| 1327 | C=..[Op,A,B], | |
| 1328 | Inner=..[Op,R,A],!, | |
| 1329 | append_to_op(B,Inner,Res,Op). | |
| 1330 | append_to_op(B,R,C,Op) :- C=..[Op,R,B]. | |
| 1331 | ||
| 1332 | % ------------------ | |
| 1333 | ||
| 1334 | remove_from_op(El,Term,NewTerm,Op) :- | |
| 1335 | op_to_list(Term,List,Op), | |
| 1336 | remove_from_list(El,List,List0), | |
| 1337 | list_to_op(List0,NewTerm,Op). | |
| 1338 | ||
| 1339 | remove_from_list(_,[],[]). | |
| 1340 | remove_from_list(E,[E|T],T2) :- remove_from_list(E,T,T2). | |
| 1341 | remove_from_list(E,[X|T],[X|T2]) :- X \= E, remove_from_list(E,T,T2). | |
| 1342 | ||
| 1343 |