| 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),[ajoin/2, 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),Id)) :- is_identity(Id), 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,Id)),finite(E),'SIMP_FINITE_ID_DOMRES') :- is_identity(Id). |
| 158 | | simp_rule(finite(domain_restriction(E,FirstPrj)),finite(E),'SIMP_FINITE_PRJ1_DOMRES') :- is_prj1(FirstPrj). |
| 159 | | simp_rule(finite(domain_restriction(E,SecondPrj)),finite(E),'SIMP_FINITE_PRJ2_DOMRES') :- is_prj2(SecondPrj). |
| 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),Id),equal(E,F),'DEF_IN_ID') :- is_identity(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,Id)),domain_restriction(intersection(S,T),Id),'SIMP_DOMRES_DOMRES_ID') :- is_identity(Id). |
| 400 | | simp_rule(domain_restriction(S,domain_subtraction(T,Id)),domain_restriction(set_subtraction(S,T),Id),'SIMP_DOMRES_DOMSUB_ID') :- is_identity(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,Id),T),domain_restriction(intersection(S,T),Id),'SIMP_RANRES_DOMRES_ID') :- is_identity(Id). |
| 404 | | simp_rule(range_restriction(domain_subtraction(S,Id),T),domain_restriction(set_subtraction(T,S),Id),'SIMP_RANRES_DOMSUB_ID') :- is_identity(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(Id,S),domain_restriction(S,Id),'SIMP_RANRES_ID') :- is_identity(Id). |
| 408 | | simp_rule(range_subtraction(Id,S),domain_subtraction(S,Id),'SIMP_RANSUB_ID') :- is_identity(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,Id)),domain_restriction(set_subtraction(T,S),Id),'SIMP_DOMSUB_DOMRES_ID') :- is_identity(Id). |
| 414 | | simp_rule(domain_subtraction(S,domain_subtraction(T,Id)),domain_subtraction(union(S,T),Id),'SIMP_DOMSUB_DOMSUB_ID') :- is_identity(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,Id),T),domain_restriction(set_subtraction(S,T),Id),'SIMP_RANSUB_DOMRES_ID') :- is_identity(Id). |
| 420 | | simp_rule(range_subtraction(domain_subtraction(S,Id),T),domain_subtraction(union(S,T),Id),'SIMP_RANSUB_DOMSUB_ID') :- is_identity(Id). |
| 421 | | simp_rule(composition(A,B),R,'SIMP_TYPE_FCOMP_ID') :- sym_unify(A,B,R,Id), is_identity(Id). |
| 422 | | simp_rule(ring(A,B),R,'SIMP_TYPE_BCOMP_ID') :- sym_unify(A,B,R,Id), is_identity(Id). |
| 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(Id,T),T,'SIMP_RELIMAGE_ID') :- is_identity(Id). |
| 434 | | simp_rule(image(domain_restriction(S,Id),T),intersection(S,T),'SIMP_RELIMAGE_DOMRES_ID') :- is_identity(Id). |
| 435 | | simp_rule(image(domain_subtraction(S,Id),T),set_subtraction(T,S),'SIMP_RELIMAGE_DOMSUB_ID') :- is_identity(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(Id),Id,'SIMP_CONVERSE_ID') :- is_identity(Id). |
| 447 | | simp_rule(member(couple(E,F),set_subtraction(_,Id)),falsity,'SIMP_SPECIAL_IN_SETMINUS_ID') :- is_identity(Id), equal_terms(E,F). |
| 448 | | simp_rule(member(couple(E,F),domain_restriction(S,Id)),member(E,S),'SIMP_SPECIAL_IN_DOMRES_ID') :- is_identity(Id), |
| 449 | | equal_terms(E,F). |
| 450 | | simp_rule(member(couple(E,F),set_subtraction(R,domain_restriction(S,Id))), |
| 451 | | member(couple(E,F),domain_subtraction(S,R)),'SIMP_SPECIAL_IN_SETMINUS_DOMRES_ID') :- is_identity(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,Id),R),domain_restriction(S,R),'SIMP_FCOMP_ID_L') :- is_identity(Id). |
| 457 | | simp_rule(composition(R,domain_restriction(S,Id)),range_restriction(R,S),'SIMP_FCOMP_ID_R') :- is_identity(Id). |
| 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(FirstPrj,couple(E,_)),E,'SIMP_FUNIMAGE_PRJ1') :- is_prj1(FirstPrj). |
| 461 | | simp_rule(function(SecondPrj,couple(_,F)),F,'SIMP_FUNIMAGE_PRJ2') :- is_prj2(SecondPrj). |
| 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,Id),set_extension([couple(E,E)]),'DERIV_ID_SING') :- is_identity(Id), 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(Id,X),X,'SIMP_FUNIMAGE_ID') :- is_identity(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,Id)),S,'SIMP_CARD_ID_DOMRES') :- is_identity(Id). |
| 543 | | simp_rule(card(domain_restriction(E,FirstPrj)),E,'SIMP_CARD_PRJ1_DOMRES') :- is_prj1(FirstPrj). |
| 544 | | simp_rule(card(domain_restriction(E,SecondPrj)),E,'SIMP_CARD_PRJ2_DOMRES') :- is_prj2(SecondPrj). |
| 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 | | |
| 582 | | simp_rule(card(typeof(Fun,Type)),card(S),Rule) :- |
| 583 | | const_rel(Fun,Abbr), |
| 584 | | const_rel_type(Type,S,_), |
| 585 | | ajoin(['SIMP_CARD_',Abbr],Rule). |
| 586 | | simp_rule(finite(typeof(Fun,Type)),finite(S),Rule) :- |
| 587 | | const_rel(Fun,Abbr), |
| 588 | | const_rel_type(Type,S,_), |
| 589 | | ajoin(['SIMP_FINITE_',Abbr],Rule). |
| 590 | | simp_rule(domain(typeof(Fun,Type)),S,Rule) :- |
| 591 | | const_rel(Fun,Abbr), |
| 592 | | const_rel_type(Type,S,_), |
| 593 | | ajoin(['SIMP_DOM_',Abbr],Rule). |
| 594 | | simp_rule(range(typeof(Fun,Type)),T,Rule) :- |
| 595 | | const_rel(Fun,Abbr), |
| 596 | | const_rel_type(Type,_,T), |
| 597 | | ajoin(['SIMP_RAN_',Abbr],Rule). |
| 598 | | |
| 599 | | simp_rule(negation(P),Q,Rule) :- seperate_negate_rule(Rule,P), negate(P,Q). |
| 600 | | simp_rule(negation(P),Q,'Propagate negation') :- |
| 601 | | \+ seperate_negate_rule(_,P), |
| 602 | | negate(P,Q), |
| 603 | | Q \= negation(_). % De-Morgan and similar rules to propagate negation |
| 604 | ? | simp_rule(P,truth,'Evaluate tautology') :- is_true(P). |
| 605 | ? | simp_rule(E,NewE,Rule) :- is_empty(E,EmptyTerm), simp_empty_rule(EmptyTerm,NewE,Rule). |
| 606 | ? | simp_rule(E,NewE,Rule) :- is_equality(E,LHS,RHS), simp_equality(LHS,RHS,NewE,Rule). |
| 607 | | |
| 608 | | new_function(Expr,F) :- used_identifiers(Expr,L), possible_function(X), F = '$'(X), \+ member(F,L), !. |
| 609 | | |
| 610 | | func_id(f). |
| 611 | | func_id(g). |
| 612 | | func_id(h). |
| 613 | | |
| 614 | | possible_function(Z) :- func_id(Z). |
| 615 | | possible_function(Z) :- func_id(X), func_id(Y), atom_concat(X,Y,Z). |
| 616 | | |
| 617 | | seperate_negate_rule('SIMP_NOT_NOT',negation(_)). |
| 618 | | seperate_negate_rule('DISTRI_NOT_AND',conjunct(_,_)). |
| 619 | | seperate_negate_rule('DISTRI_NOT_OR',disjunct(_,_)). |
| 620 | | seperate_negate_rule('DERIV_NOT_IMP',implication(_,_)). |
| 621 | | |
| 622 | | |
| 623 | | const_rel(event_b_identity,'ID'). |
| 624 | | const_rel(event_b_first_projection_v2,'PRJ1'). |
| 625 | | const_rel(event_b_second_projection_v2,'PRJ2'). |
| 626 | | |
| 627 | | const_rel_type(pow_subset(cartesian_product(S,T)),S,T). |
| 628 | | |
| 629 | | |
| 630 | ? | overwrite_type([Ty|R],_,ListOut,Info) :- type_expression(Ty,Info), !, overwrite_type(R,[Ty],ListOut,Info). |
| 631 | | overwrite_type([S|R],Prev,ListOut,Info) :- append(Prev,[S],ListIn), overwrite_type(R,ListIn,ListOut,Info). |
| 632 | | overwrite_type([],L,L,_). |
| 633 | | |
| 634 | | change_sign(L,NL,Nr) :- remove_minus(L,NL,Nr), Nr > 0. |
| 635 | | |
| 636 | ? | remove_minus([NE|R],[E|T],NrN) :- is_minus(NE,E), remove_minus(R,T,Nr), NrN is Nr + 1, !. |
| 637 | | remove_minus([E|R],[E|T],Nr) :- remove_minus(R,T,Nr). |
| 638 | | remove_minus([],[],0). |
| 639 | | |
| 640 | | remove_unused_identifier(L,P,Used) :- |
| 641 | ? | member(Z,L), |
| 642 | | used_identifiers(P,Ids), |
| 643 | | member(Z,Ids), |
| 644 | | list_intersection(L,Ids,Used). |
| 645 | | |
| 646 | | |
| 647 | | min_list([H|T], Min) :- number(H) -> min_list(T,H,Min) ; min_list(T,Min). |
| 648 | | |
| 649 | | min_list([],Min,Min). |
| 650 | | min_list([H|T],Min0,Min) :- |
| 651 | | number(H),!, |
| 652 | | Min1 is min(H,Min0), |
| 653 | | min_list(T,Min1,Min). |
| 654 | | min_list([_|T],Min0,Min) :- |
| 655 | | min_list(T,Min0,Min). |
| 656 | | |
| 657 | ? | remove_greater(L,I,Res) :- only_min(L,I,[],Res). |
| 658 | | |
| 659 | | only_min([],_,List,List). |
| 660 | | only_min([E|R],I,Filtered, Res) :- |
| 661 | | \+ number(E),!, |
| 662 | | append(Filtered,[E],New), |
| 663 | ? | only_min(R,I,New,Res). |
| 664 | | only_min([E|R],I,Filtered,Res) :- |
| 665 | | E > I, |
| 666 | ? | only_min(R,I,Filtered,Res). |
| 667 | | only_min([E|R],I,Filtered,Res) :- |
| 668 | | E =:= I, |
| 669 | | member(E,Filtered), |
| 670 | | only_min(R,I,Filtered,Res). |
| 671 | | only_min([E|R],I,Filtered,Res) :- |
| 672 | | E =:= I, |
| 673 | | \+ member(E,Filtered), |
| 674 | | append(Filtered,[E],New), |
| 675 | ? | only_min(R,I,New,Res). |
| 676 | | |
| 677 | | max_list([H|T],Max) :- number(H) -> max_list(T,H,Max) ; max_list(T,Max). |
| 678 | | |
| 679 | | max_list([],Max,Max). |
| 680 | | max_list([H|T],Max0,Max) :- |
| 681 | | number(H),!, |
| 682 | | Max1 is max(H,Max0), |
| 683 | | max_list(T,Max1,Max). |
| 684 | | max_list([_|T],Max0,Max) :- |
| 685 | | max_list(T,Max0,Max). |
| 686 | | |
| 687 | | remove_smaller(L,I,Res) :- only_max(L,I,[],Res). |
| 688 | | |
| 689 | | only_max([],_,List,List). |
| 690 | | only_max([E|R],I,Filtered, Res) :- |
| 691 | | \+ number(E),!, |
| 692 | | append(Filtered,[E],New), |
| 693 | | only_max(R,I,New,Res). |
| 694 | | only_max([E|R],I,Filtered,Res) :- |
| 695 | | E < I, |
| 696 | | only_max(R,I,Filtered,Res). |
| 697 | | only_max([E|R],I,Filtered,Res) :- |
| 698 | | E =:= I, |
| 699 | | member(E,Filtered), |
| 700 | | only_max(R,I,Filtered,Res). |
| 701 | | only_max([E|R],I,Filtered,Res) :- |
| 702 | | E =:= I, |
| 703 | | \+ member(E,Filtered), |
| 704 | | append(Filtered,[E],New), |
| 705 | | only_max(R,I,New,Res). |
| 706 | | |
| 707 | | % ----------------- |
| 708 | | |
| 709 | | |
| 710 | | % simplification rules for equality |
| 711 | | % simp_equality(LHS,RHS,NewPred,'RuleName'). |
| 712 | | simp_equality(interval(_,_),Z,falsity,Rule) :- |
| 713 | | ( is_integer_set(Z) -> Rule = 'SIMP_UPTO_EQUAL_INTEGER' |
| 714 | | ; is_natural_set(Z) -> Rule = 'SIMP_UPTO_EQUAL_NATURAL' |
| 715 | | ; is_natural1_set(Z) -> Rule = 'SIMP_UPTO_EQUAL_NATURAL1'). |
| 716 | | simp_equality(convert_bool(P),boolean_true,P,'SIMP_LIT_EQUAL_KBOOL_TRUE'). |
| 717 | | simp_equality(convert_bool(P),boolean_false,negation(P),'SIMP_LIT_EQUAL_KBOOL_FALSE'). |
| 718 | | simp_equality(T,U,subset(NewU,T),'SIMP_MULTI_EQUAL_BUNION') :- |
| 719 | | member_of(union,T,U), |
| 720 | | remove_from_op(T,U,NewU,union). |
| 721 | | simp_equality(I,T,subset(T,NewI),'SIMP_MULTI_EQUAL_BINTER') :- |
| 722 | | member_of(intersection,T,I), |
| 723 | | remove_from_op(T,I,NewI,intersection). |
| 724 | | simp_equality(function(F,X),Y,member(couple(X,Y),F),'DEF_EQUAL_FUNIMAGE'). |
| 725 | | simp_equality(card(S),0,equal(S,empty_set),'SIMP_SPECIAL_EQUAL_CARD'). |
| 726 | | simp_equality(card(S),1,exists([X],equal(S,set_extension([X]))),'SIMP_LIT_EQUAL_CARD_1') :- |
| 727 | | new_identifier(S,X). |
| 728 | | simp_equality(card(S),K,exists([F],member(F,total_bijection(interval(1,K),S))),'DEF_EQUAL_CARD') :- |
| 729 | | new_function(conjunct(S,K),F). |
| 730 | | simp_equality(E,min(S),conjunct(member(E,S),forall([X],member(X,S),less_equal(E,X))),'DEF_EQUAL_MIN') :- |
| 731 | | new_identifier(member(E,S),X). |
| 732 | | simp_equality(E,max(S),conjunct(member(E,S),forall([X],member(X,S),greater_equal(E,X))),'DEF_EQUAL_MAX') :- |
| 733 | | new_identifier(member(E,S),X). |
| 734 | | |
| 735 | | |
| 736 | | % candidates for SIMP_SPECIAL_REL_R rule rewriting to {{}} |
| 737 | | simp_relation_empty_range(relations(_,empty_set)). |
| 738 | | simp_relation_empty_range(surjection_relation(_,empty_set)). |
| 739 | | simp_relation_empty_range(partial_function(_,empty_set)). |
| 740 | | simp_relation_empty_range(partial_injection(_,empty_set)). |
| 741 | | simp_relation_empty_range(partial_surjection(_,empty_set)). |
| 742 | | |
| 743 | | % candidates for SIMP_SPECIAL_REL_L rule rewriting to {{}} |
| 744 | | simp_relation_empty_domain(relations(empty_set,_)). |
| 745 | | simp_relation_empty_domain(total_relation(empty_set,_)). |
| 746 | | simp_relation_empty_domain(partial_function(empty_set,_)). |
| 747 | | simp_relation_empty_domain(total_function(empty_set,_)). |
| 748 | | simp_relation_empty_domain(partial_injection(empty_set,_)). |
| 749 | | simp_relation_empty_domain(total_injection(empty_set,_)). |
| 750 | | |
| 751 | | % simplification rules for empty set equalities |
| 752 | | % simp_empty_rule(TermThatIsEmpty,NewPredicate,RuleName) |
| 753 | | simp_empty_rule(set_extension(L),Res,'SIMP_SETENUM_EQUAL_EMPTY') :- length(L,LL), |
| 754 | | (LL > 0 -> Res = falsity ; Res = truth). |
| 755 | | simp_empty_rule(interval(I,J),greater(I,J),'SIMP_UPTO_EQUAL_EMPTY'). |
| 756 | | simp_empty_rule(relations(_,_),falsity,'SIMP_SPECIAL_EQUAL_REL'). |
| 757 | | simp_empty_rule(total_relation(A,B),conjunct(negation(equal(A,empty_set)),equal(B,empty_set)),'SIMP_SPECIAL_EQUAL_RELDOM'). |
| 758 | | simp_empty_rule(total_function(A,B),conjunct(negation(equal(A,empty_set)),equal(B,empty_set)),'SIMP_SPECIAL_EQUAL_RELDOM'). |
| 759 | | simp_empty_rule(surjection_relation(A,B),conjunct(equal(A,empty_set),negation(equal(B,empty_set))), |
| 760 | | 'SIMP_SREL_EQUAL_EMPTY'). |
| 761 | | simp_empty_rule(total_surjection_relation(A,B),equivalence(equal(A,empty_set),negation(equal(B,empty_set))), |
| 762 | | 'SIMP_STREL_EQUAL_EMPTY'). |
| 763 | | simp_empty_rule(domain(R),equal(R,empty_set),'SIMP_DOM_EQUAL_EMPTY'). |
| 764 | | simp_empty_rule(range(R),equal(R,empty_set),'SIMP_RAN_EQUAL_EMPTY'). |
| 765 | | simp_empty_rule(composition(P,Q),equal(intersection(range(P),domain(Q)),empty_set),'SIMP_FCOMP_EQUAL_EMPTY'). |
| 766 | | simp_empty_rule(ring(P,Q),equal(intersection(range(Q),domain(P)),empty_set),'SIMP_BCOMP_EQUAL_EMPTY'). |
| 767 | | simp_empty_rule(domain_restriction(S,R),equal(intersection(domain(R),S),empty_set),'SIMP_DOMRES_EQUAL_EMPTY'). |
| 768 | | simp_empty_rule(domain_subtraction(S,R),subset(domain(R),S),'SIMP_DOMSUB_EQUAL_EMPTY'). |
| 769 | | simp_empty_rule(range_restriction(R,S),equal(intersection(range(R),S),empty_set),'SIMP_RANRES_EQUAL_EMPTY'). |
| 770 | | simp_empty_rule(range_subtraction(R,S),subset(range(R),S),'SIMP_RANSUB_EQUAL_EMPTY'). |
| 771 | | simp_empty_rule(reverse(R),equal(R,empty_set),'SIMP_CONVERSE_EQUAL_EMPTY'). |
| 772 | | simp_empty_rule(image(R,S),equal(domain_restriction(S,R),empty_set),'SIMP_RELIMAGE_EQUAL_EMPTY'). |
| 773 | | simp_empty_rule(overwrite(P,Q),Res,'SIMP_OVERL_EQUAL_EMPTY') :- |
| 774 | | and_empty(overwrite(P,Q),Res,overwrite). |
| 775 | | simp_empty_rule(direct_product(P,Q),equal(intersection(domain(P),domain(Q)),empty_set),'SIMP_DPROD_EQUAL_EMPTY'). |
| 776 | | simp_empty_rule(parallel_product(P,Q),disjunct(equal(P,empty_set),equal(Q,empty_set)),'SIMP_PPROD_EQUAL_EMPTY'). |
| 777 | | simp_empty_rule(Id,falsity,'SIMP_ID_EQUAL_EMPTY') :- is_identity(Id). |
| 778 | | simp_empty_rule(FirstPrj,falsity,'SIMP_PRJ1_EQUAL_EMPTY') :- is_prj1(FirstPrj). |
| 779 | | simp_empty_rule(SecondPrj,falsity,'SIMP_PRJ2_EQUAL_EMPTY') :- is_prj2(SecondPrj). |
| 780 | | simp_empty_rule(cartesian_product(S,T),disjunct(equal(S,empty_set),equal(T,empty_set)),'SIMP_CPROD_EQUAL_EMPTY'). |
| 781 | | simp_empty_rule(quantified_union([X],P,E),forall([X],P,equal(E,empty_set)),'SIMP_QUNION_EQUAL_EMPTY'). |
| 782 | | simp_empty_rule(union(A,B),Res,'SIMP_BUNION_EQUAL_EMPTY') :- and_empty(union(A,B),Res,union). |
| 783 | | simp_empty_rule(set_subtraction(A,B),subset(A,B),'SIMP_SETMINUS_EQUAL_EMPTY'). |
| 784 | | simp_empty_rule(event_b_comprehension_set(Ids,_,P),forall(Ids,truth,negation(P)),'SIMP_SPECIAL_EQUAL_COMPSET'). |
| 785 | | simp_empty_rule(pow_subset(_),falsity,'SIMP_POW_EQUAL_EMPTY'). |
| 786 | | simp_empty_rule(pow1_subset(S),equal(S,empty_set),'SIMP_POW1_EQUAL_EMPTY'). % TODO: similar rules for FIN/FIN1 ? |
| 787 | | simp_empty_rule(general_union(S),subset(S,set_extension([empty_set])),'SIMP_KUNION_EQUAL_EMPTY'). |
| 788 | | simp_empty_rule(I,equal(set_subtraction(I0,C),empty_set),'SIMP_BINTER_SETMINUS_EQUAL_EMPTY') :- |
| 789 | | member_of(intersection,set_subtraction(B,C),I), |
| 790 | | select_op(minus(B,C),I,B,I0,intersection). |
| 791 | | simp_empty_rule(Nat,falsity,'SIMP_NATURAL_EQUAL_EMPTY') :- is_natural_set(Nat). |
| 792 | | simp_empty_rule(Nat,falsity,'SIMP_NATURAL1_EQUAL_EMPTY') :- is_natural1_set(Nat). |
| 793 | | %simp_empty_rule(TermThatIsEmpty,NewPred,RuleName). |
| 794 | | |
| 795 | | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_PLUS') :- |
| 796 | | Ex=..[Rel,L,R], |
| 797 | | comparison(Rel), |
| 798 | | R = add(_,_), |
| 799 | ? | member_of(add,El,L), |
| 800 | ? | select_op(El,L,L0,add), |
| 801 | | select_op(El,R,R0,add), |
| 802 | | Res=..[Rel,L0,R0]. |
| 803 | | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_R') :- |
| 804 | | Ex=..[Rel,C,R], |
| 805 | | comparison(Rel), |
| 806 | | R = add(_,_), |
| 807 | | select_op(C,R,R0,add), |
| 808 | | Res=..[Rel,0,R0]. |
| 809 | | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_L') :- |
| 810 | | Ex=..[Rel,L,C], |
| 811 | | comparison(Rel), |
| 812 | | L = add(_,_), |
| 813 | | select_op(C,L,L0,add), |
| 814 | | Res=..[Rel,L0,0]. |
| 815 | | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_R') :- |
| 816 | | Ex=..[Rel,L,R], |
| 817 | | comparison(Rel), |
| 818 | | L = minus(A,C1), |
| 819 | | R = minus(B,C2), |
| 820 | | equal_terms(C1,C2), |
| 821 | | Res=..[Rel,A,B]. |
| 822 | | simp_multi_arithrel(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_L') :- |
| 823 | | Ex=..[Rel,L,R], |
| 824 | | comparison(Rel), |
| 825 | | L = minus(C1,A), |
| 826 | | R = minus(C2,B), |
| 827 | | equal_terms(C1,C2), |
| 828 | | Res=..[Rel,B,A]. |
| 829 | | |
| 830 | | select_summand(X,Y,0) :- equal_terms(X,Y). |
| 831 | | select_summand(add(L,R),X,ResTerm) :- select_summand(L,X,NewL), if_zero(NewL,R,add(NewL,R),ResTerm). |
| 832 | ? | select_summand(add(L,R),X,ResTerm) :- select_summand(R,X,NewR), if_zero(NewR,L,add(L,NewR),ResTerm). |
| 833 | | select_summand(minus(L,R),X,ResTerm) :- select_summand(L,X,NewL), if_zero(NewL,unary_minus(R),minus(NewL,R),ResTerm). |
| 834 | | |
| 835 | ? | select_subtrahend(MinusY,X,0) :- is_minus(MinusY,Y), equal_terms(X,Y). |
| 836 | | select_subtrahend(minus(Y,X),X,Y). |
| 837 | | select_subtrahend(add(MinusX,Y),X,Res) :- select_subtrahend(MinusX,X,NewR), if_zero(NewR,Y,add(NewR,Y),Res). |
| 838 | | select_subtrahend(add(Y,MinusX),X,Res) :- select_subtrahend(MinusX,X,NewR), if_zero(NewR,Y,add(Y,NewR),Res). |
| 839 | | select_subtrahend(minus(L,Y),X,Res) :- select_subtrahend(L,X,NewL), if_zero(NewL,unary_minus(Y),minus(NewL,Y),Res). |
| 840 | | |
| 841 | | if_zero(Term,Then,Else,Res) :- |
| 842 | | (Term = 0 |
| 843 | | -> Res = Then |
| 844 | | ; Res = Else). |
| 845 | | |
| 846 | | |
| 847 | | all_pairs(L,Pairs) :- findall([X,Y], (combination(L,[X,Y])), Pairs). |
| 848 | | |
| 849 | | combination(_,[]). |
| 850 | ? | combination([X|T],[X|C]) :- combination(T,C). |
| 851 | | combination([_|T],[X|C]) :- combination(T,[X|C]). |
| 852 | | |
| 853 | | |
| 854 | | all_in_set([E],S,Hyps) :- member_hyps(member(E,S),Hyps). |
| 855 | ? | all_in_set([E|R],S,Hyps) :- member_hyps(member(E,S),Hyps), all_in_set(R,S,Hyps). |
| 856 | | |
| 857 | | map_dom([couple(X,_)],[X]) :- !. |
| 858 | | map_dom([couple(X,_)|T],[X|R]) :- map_dom(T,R). |
| 859 | | |
| 860 | | map_ran([couple(_,A)],[A]) :- !. |
| 861 | | map_ran([couple(_,B)|T],[B|R]) :- map_ran(T,R). |
| 862 | | |
| 863 | | all_map_to([couple(_,F)],E) :- equal_terms(E,F), !. |
| 864 | | all_map_to([couple(_,F)|T],E) :- equal_terms(E,F), all_map_to(T,E). |
| 865 | | |
| 866 | | convert_map_to([couple(X,Y)],[couple(Y,X)]) :- !. |
| 867 | | convert_map_to([couple(X,Y)|T],[couple(Y,X)|R]) :- convert_map_to(T,R). |
| 868 | | |
| 869 | | list_subset([],_). |
| 870 | | list_subset([E|T],L) :- memberchk(E,L), list_subset(T,L). |
| 871 | | |
| 872 | | |
| 873 | | |
| 874 | | % ----------------- |
| 875 | | |
| 876 | | |
| 877 | | distri(C,Res,Op1,Op2) :- |
| 878 | | C=..[Op1,A,B], |
| 879 | | (X = A ; X = B), |
| 880 | | functor(X,Op2,2), |
| 881 | ? | distribute_op(C,X,Op1,Op2,Res). |
| 882 | | |
| 883 | | distri_r2(C,Res,Rule) :- |
| 884 | | C=..[Op1,_,X], |
| 885 | | functor(X,Op2,2), |
| 886 | ? | distri_r2_name(Op1,Op2,Rule), |
| 887 | ? | distribute_op(C,X,Op1,Op2,Res). |
| 888 | | distri_r2_name(ring,union,'DISTRI_BCOMP_BUNION'). |
| 889 | | distri_r2_name(direct_product,union,'DISTRI_DPROD_BUNION'). |
| 890 | | distri_r2_name(direct_product,set_subtraction,'DISTRI_DPROD_SETMINUS'). |
| 891 | | distri_r2_name(direct_product,intersection,'DISTRI_DPROD_BINTER'). |
| 892 | | distri_r2_name(direct_product,overwrite,'DISTRI_DPROD_OVERL'). |
| 893 | | distri_r2_name(parallel_product,union,'DISTRI_PPROD_BUNION'). |
| 894 | | distri_r2_name(parallel_product,intersection,'DISTRI_PPROD_BINTER'). |
| 895 | | distri_r2_name(parallel_product,set_subtraction,'DISTRI_PPROD_SETMINUS'). |
| 896 | | distri_r2_name(parallel_product,overwrite,'DISTRI_PPROD_OVERL'). |
| 897 | | distri_r2_name(domain_restriction,union,'DISTRI_DOMRES_BUNION_R'). |
| 898 | | distri_r2_name(domain_restriction,intersection,'DISTRI_DOMRES_BINTER_R'). |
| 899 | | distri_r2_name(domain_restriction,set_subtraction,'DISTRI_DOMRES_SETMINUS_R'). |
| 900 | | distri_r2_name(domain_restriction,direct_product,'DISTRI_DOMRES_DPROD'). |
| 901 | | distri_r2_name(domain_restriction,overwrite,'DISTRI_DOMRES_OVERL'). |
| 902 | | distri_r2_name(domain_subtraction,union,'DISTRI_DOMSUB_BUNION_R'). |
| 903 | | distri_r2_name(domain_subtraction,intersection,'DISTRI_DOMSUB_BINTER_R'). |
| 904 | | distri_r2_name(domain_subtraction,direct_product,'DISTRI_DOMSUB_DPROD'). |
| 905 | | distri_r2_name(domain_subtraction,overwrite,'DISTRI_DOMSUB_OVERL'). |
| 906 | | distri_r2_name(composition,union,'DISTRI_FCOMP_BUNION_R'). |
| 907 | | distri_r2_name(range_restriction,union,'DISTRI_RANRES_BUNION_R'). |
| 908 | | distri_r2_name(range_restriction,intersection,'DISTRI_RANRES_BINTER_R'). |
| 909 | | distri_r2_name(range_restriction,set_subtraction,'DISTRI_RANRES_SETMINUS_R'). |
| 910 | | |
| 911 | | distri_l2(C,Res,RuleName) :- |
| 912 | | distri_l2_arg1(C,Op1,X), |
| 913 | | functor(X,Op2,2), |
| 914 | ? | distri_l2_name(Op1,Op2,RuleName), |
| 915 | ? | distribute_op(C,X,Op1,Op2,Res). |
| 916 | | distri_l2_arg1(overwrite(X,_),overwrite,X). |
| 917 | | distri_l2_arg1(composition(X,_),composition,X). |
| 918 | | distri_l2_arg1(domain_restriction(X,_),domain_restriction,X). |
| 919 | | distri_l2_arg1(range_restriction(X,_),range_restriction,X). |
| 920 | | distri_l2_arg1(range_subtraction(X,_),range_subtraction,X). |
| 921 | | distri_l2_name(overwrite,union,'DISTRI_OVERL_BUNION_L'). |
| 922 | | distri_l2_name(overwrite,intersection,'DISTRI_OVERL_BINTER_L'). |
| 923 | | distri_l2_name(composition,union,'DISTRI_FCOMP_BUNION_L'). |
| 924 | | distri_l2_name(domain_restriction,union,'DISTRI_DOMRES_BUNION_L'). |
| 925 | | distri_l2_name(domain_restriction,intersection,'DISTRI_DOMRES_BINTER_L'). |
| 926 | | distri_l2_name(domain_restriction,set_subtraction,'DISTRI_DOMRES_SETMINUS_L'). |
| 927 | | distri_l2_name(range_restriction,union,'DISTRI_RANRES_BUNION_L'). |
| 928 | | distri_l2_name(range_restriction,intersection,'DISTRI_RANRES_BINTER_L'). |
| 929 | | distri_l2_name(range_restriction,set_subtraction,'DISTRI_RANRES_SETMINUS_L'). |
| 930 | | distri_l2_name(range_subtraction,union,'DISTRI_RANSUB_BUNION_L'). |
| 931 | | distri_l2_name(range_subtraction,intersection,'DISTRI_RANSUB_BINTER_L'). |
| 932 | | |
| 933 | | distribute_op(C,X,Op1,Op2,Res) :- |
| 934 | | op_to_list(X,L,Op2), |
| 935 | ? | distribute(C,X,L,CN,Op1), |
| 936 | | list_to_op(CN,Res,Op2). |
| 937 | | |
| 938 | | distribute(_,_,[],[],_). |
| 939 | ? | distribute(C,X,[D|T],[N|R],Op) :- select_op(X,C,D,N,Op), distribute(C,X,T,R,Op). |
| 940 | | |
| 941 | | distri_r3(C,Res,Rule) :- |
| 942 | | C = range_subtraction(_,X), Op1=range_subtraction, %C=..[Op1,_,X], |
| 943 | ? | distri_r3_name_ransub(Op2,Op3,Rule), |
| 944 | ? | distri_and_change(C,X,Op1,Op2,Op3,Res). |
| 945 | | distri_r3_name_ransub(union,intersection,'DISTRI_RANSUB_BUNION_R'). |
| 946 | | distri_r3_name_ransub(intersection,union,'DISTRI_RANSUB_BINTER_R'). |
| 947 | | |
| 948 | | distri_r3_info(C,Res,Rule,Info) :- |
| 949 | | C = set_subtraction(Ty,X), Op1=set_subtraction, |
| 950 | ? | type_expression(Ty,Info), |
| 951 | ? | distri_r3_name_setsub(Op2,Op3,Rule), |
| 952 | ? | distri_and_change(C,X,Op1,Op2,Op3,Res). |
| 953 | | distri_r3_name_setsub(intersection,union,'DERIV_TYPE_SETMINUS_BINTER'). % Ty \ (S /\ T) == (Ty \ S) \/ (Ty \ T) |
| 954 | | distri_r3_name_setsub(union,intersection,'DERIV_TYPE_SETMINUS_BUNION'). |
| 955 | | |
| 956 | | distri_l3(C,Res,Op1,Op2,Op3) :- |
| 957 | | C=..[Op1,X,_], |
| 958 | ? | distri_and_change(C,X,Op1,Op2,Op3,Res). |
| 959 | | |
| 960 | | % Op2 changes to Op3 |
| 961 | | distri_and_change(C,X,Op1,Op2,Op3,Res) :- |
| 962 | | functor(X,Op2,2), |
| 963 | | op_to_list(X,L,Op2), |
| 964 | ? | distribute(C,X,L,CN,Op1), |
| 965 | | list_to_op(CN,Res,Op3). |
| 966 | | |
| 967 | | distri_setminus(U,X,Res) :- |
| 968 | | C = set_subtraction(U,X), X = union(_,_), |
| 969 | | select_op(X,C,NewC,set_subtraction), |
| 970 | | op_to_list(NewC,CL,set_subtraction), |
| 971 | | op_to_list(X,L,union), |
| 972 | | append(CL,L,L2), |
| 973 | | list_to_op(L2,Res,set_subtraction). |
| 974 | | |
| 975 | | |
| 976 | | % ----------------- |
| 977 | | |
| 978 | | %simp_rule(X,X,'EQ'(F,N,X)) :- functor(X,F,N). |
| 979 | | |
| 980 | | % simp_rule/4 |
| 981 | | simp_rule(D,implication(negation(P),D0),'DEF_OR',OuterOp) :- OuterOp \= disjunct, D = disjunct(_,_), select_op(P,D,D0,disjunct). |
| 982 | | simp_rule(C,falsity,'SIMP_SPECIAL_AND_BFALSE',OuterOp) :- OuterOp \= conjunct, |
| 983 | | member_of_bin_op(conjunct,falsity,C). |
| 984 | | simp_rule(D,truth,'SIMP_SPECIAL_OR_BTRUE',OuterOp) :- OuterOp \= disjunct, |
| 985 | ? | member_of_bin_op(disjunct,truth,D). |
| 986 | | simp_rule(C,Res,'SIMP_MULTI_AND',OuterOp) :- OuterOp \= conjunct, remove_duplicates_for_op(C,Res,conjunct). |
| 987 | | simp_rule(D,Res,'SIMP_MULTI_OR',OuterOp) :- OuterOp \= disjunct, remove_duplicates_for_op(D,Res,disjunct). |
| 988 | | simp_rule(C,falsity,'SIMP_MULTI_AND_NOT',OuterOp) :- |
| 989 | | OuterOp \= conjunct, |
| 990 | ? | member_of(conjunct,Q,C), |
| 991 | ? | member_of(conjunct,NotQ,C), |
| 992 | | is_negation(Q,NotQ). |
| 993 | | simp_rule(D,truth,'SIMP_MULTI_OR_NOT',OuterOp) :- |
| 994 | | OuterOp \= disjunct, |
| 995 | ? | member_of(disjunct,Q,D), |
| 996 | ? | member_of(disjunct,NotQ,D), |
| 997 | | is_negation(Q,NotQ). |
| 998 | | simp_rule(I,empty_set,'SIMP_SPECIAL_BINTER',OuterOp) :- OuterOp \= intersection, |
| 999 | ? | member_of_bin_op(intersection,empty_set,I). |
| 1000 | | simp_rule(I,Res,'SIMP_MULTI_BINTER',OuterOp) :- OuterOp \= intersection, remove_duplicates_for_op(I,Res,intersection). |
| 1001 | | simp_rule(U,Res,'SIMP_MULTI_BUNION',OuterOp) :- OuterOp \= union, remove_duplicates_for_op(U,Res,union). |
| 1002 | | simp_rule(C,empty_set,'SIMP_SPECIAL_CPROD',OuterOp) :- OuterOp \= cartesian_product, % SIMP_SPECIAL_CPROD_L / SIMP_SPECIAL_CPROD_R |
| 1003 | | member_of_bin_op(cartesian_product,empty_set,C). |
| 1004 | | simp_rule(C,empty_set,'SIMP_SPECIAL_FCOMP',OuterOp) :- OuterOp \= composition, |
| 1005 | | member_of_bin_op(composition,empty_set,C). |
| 1006 | | simp_rule(Comp,empty_set,'SIMP_SPECIAL_BCOMP',OuterOp) :- OuterOp \= ring, |
| 1007 | | member_of_bin_op(ring,empty_set,Comp). |
| 1008 | | simp_rule(C,Res,'DEF_BCOMP',OuterOp) :- OuterOp \= ring, C = ring(_,_), |
| 1009 | ? | bwd_to_fwd_comp(C,Comp), reorder(Comp,Res,composition). |
| 1010 | ? | simp_rule(P,0,'SIMP_SPECIAL_PROD_0',OuterOp) :- OuterOp \= multiplication, member_of(multiplication,0,P). |
| 1011 | | simp_rule(ring(P,Q),Res,'SIMP_BCOMP_ID',OuterOp) :- OuterOp \= ring, |
| 1012 | | op_to_list(ring(P,Q),List,ring), |
| 1013 | ? | rewrite_comp_id(List,List2), |
| 1014 | | list_to_op(List2,Res,ring). |
| 1015 | | simp_rule(composition(P,Q),Res,'SIMP_FCOMP_ID',OuterOp) :- OuterOp \= composition, |
| 1016 | | op_to_list(composition(P,Q),List,composition), |
| 1017 | ? | rewrite_comp_id(List,List2), |
| 1018 | | list_to_op(List2,Res,composition). |
| 1019 | ? | simp_rule(Comp,Res,'DERIV_FCOMP_DOMRES',OuterOp) :- OuterOp \= composition, deriv_fcomp_dom(Comp,domain_restriction,Res). |
| 1020 | ? | simp_rule(Comp,Res,'DERIV_FCOMP_DOMSUB',OuterOp) :- OuterOp \= composition, deriv_fcomp_dom(Comp,domain_subtraction,Res). |
| 1021 | ? | simp_rule(Comp,Res,'DERIV_FCOMP_RANRES',OuterOp) :- OuterOp \= composition, deriv_fcomp_ran(Comp,range_restriction,Res). |
| 1022 | | simp_rule(Comp,Res,'DERIV_FCOMP_RANSUB',OuterOp) :- OuterOp \= composition, deriv_fcomp_ran(Comp,range_subtraction,Res). |
| 1023 | | |
| 1024 | | |
| 1025 | | deriv_fcomp_dom(Comp,Functor,Res) :- |
| 1026 | | Comp = composition(_,_), |
| 1027 | | op_to_list(Comp,List,composition), |
| 1028 | | append(L,[At|R],List), |
| 1029 | | At=..[Functor,P,Q], |
| 1030 | | list_to_op([Q|R],RComp,composition), |
| 1031 | | New=..[Functor,P,RComp], |
| 1032 | | append(L,[New],ResList), |
| 1033 | | list_to_op(ResList,Res,composition). |
| 1034 | | |
| 1035 | | deriv_fcomp_ran(Comp,Functor,Res) :- |
| 1036 | | Comp = composition(_,_), |
| 1037 | | op_to_list(Comp,List,composition), |
| 1038 | | append(L,[At|R],List), |
| 1039 | | At=..[Functor,P,Q], |
| 1040 | | append(L,[P],NewL), |
| 1041 | | list_to_op(NewL,LComp,composition), |
| 1042 | | New=..[Functor,LComp,Q], |
| 1043 | | list_to_op([New|R],Res,composition). |
| 1044 | | |
| 1045 | | rewrite_comp_id([X],[X]). |
| 1046 | | rewrite_comp_id([domain_restriction(S,Id),domain_restriction(T,Id)|R],Res) :- is_identity(Id), !, |
| 1047 | ? | rewrite_comp_id([domain_restriction(intersection(S,T),Id)|R],Res). |
| 1048 | | rewrite_comp_id([domain_restriction(S,Id),domain_subtraction(T,Id)|R],Res) :- is_identity(Id), !, |
| 1049 | ? | rewrite_comp_id([domain_restriction(set_subtraction(S,T),Id)|R],Res). |
| 1050 | | rewrite_comp_id([domain_subtraction(S,Id),domain_subtraction(T,Id)|R],Res) :- is_identity(Id), !, |
| 1051 | ? | rewrite_comp_id([domain_subtraction(union(S,T),Id)|R],Res). |
| 1052 | ? | rewrite_comp_id([E,F|R], [E|Res]) :- rewrite_comp_id([F|R],Res). |
| 1053 | | |
| 1054 | | |
| 1055 | | % simp_rule_with_info/4 |
| 1056 | | simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_DOMSUB_EQUAL_TYPE',Info) :- |
| 1057 | | is_equality(Eq,domain_subtraction(S,R),Ty), |
| 1058 | | type_expression(Ty,Info). |
| 1059 | | simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_RANSUB_EQUAL_TYPE',Info) :- |
| 1060 | | is_equality(Eq,range_subtraction(R,S),Ty), |
| 1061 | | type_expression(Ty,Info). |
| 1062 | | simp_rule_with_info(Eq,equal(R,reverse(Ty)),'SIMP_CONVERSE_EQUAL_TYPE',Info) :- |
| 1063 | | is_equality(Eq,reverse(R),Ty), |
| 1064 | | type_expression(Ty,Info). |
| 1065 | ? | simp_rule_with_info(subset(_,Ty),truth,'SIMP_TYPE_SUBSETEQ',Info) :- type_expression(Ty,Info). |
| 1066 | ? | simp_rule_with_info(set_subtraction(_,Ty),empty_set,'SIMP_TYPE_SETMINUS',Info) :- type_expression(Ty,Info). |
| 1067 | ? | simp_rule_with_info(set_subtraction(Ty,set_subtraction(Ty,S)),S,'SIMP_TYPE_SETMINUS_SETMINUS',Info) :- type_expression(Ty,Info). |
| 1068 | ? | simp_rule_with_info(member(_,Ty),truth,'SIMP_TYPE_IN',Info) :- type_expression(Ty,Info). |
| 1069 | | simp_rule_with_info(subset_strict(S,Ty),not_equal(S,Ty),'SIMP_TYPE_SUBSET_L',Info) :- type_expression(Ty,Info). |
| 1070 | | simp_rule_with_info(Eq,conjunct(equal(A,Ty),equal(B,empty_set)),'SIMP_SETMINUS_EQUAL_TYPE',Info) :- |
| 1071 | ? | is_equality(Eq,set_subtraction(A,B),Ty), |
| 1072 | | type_expression(Ty,Info). |
| 1073 | | simp_rule_with_info(Eq,Res,'SIMP_BINTER_EQUAL_TYPE',Info) :- |
| 1074 | ? | is_equality(Eq,I,Ty), |
| 1075 | | I = intersection(_,_), |
| 1076 | | type_expression(Ty,Info), |
| 1077 | | and_equal_type(I,Ty,Res). |
| 1078 | | simp_rule_with_info(Eq,equal(S,set_extension([Ty])),'SIMP_KINTER_EQUAL_TYPE',Info) :- |
| 1079 | | is_equality(Eq,general_intersection(S),Ty), |
| 1080 | | type_expression(Ty,Info). |
| 1081 | | simp_rule_with_info(Expr,falsity,'SIMP_TYPE_EQUAL_EMPTY',Info) :- is_empty(Expr,Ty), type_expression(Ty,Info). |
| 1082 | | simp_rule_with_info(Eq,forall([X],P,equal(E,Ty)),'SIMP_QINTER_EQUAL_TYPE',Info) :- |
| 1083 | | is_equality(Eq,quantified_intersection([X],P,E),Ty), |
| 1084 | | type_expression(Ty,Info). |
| 1085 | ? | simp_rule_with_info(intersection(A,B),S,'SIMP_TYPE_BINTER',Info) :- sym_unify(A,B,S,Ty), type_expression(Ty,Info). |
| 1086 | | simp_rule_with_info(Eq,falsity,'SIMP_TYPE_EQUAL_RELDOMRAN',Info) :- |
| 1087 | ? | is_equality(Eq,R,Ty), |
| 1088 | | type_expression(Ty,Info), |
| 1089 | | is_rel(R,_,_,_), |
| 1090 | | functor(R,Op,2), |
| 1091 | | \+ member(Op,[relations,partial_function,partial_injection]). % TODO: use facts without functor |
| 1092 | | simp_rule_with_info(member(Prj,RT),truth,Rule,Info) :- |
| 1093 | | ( is_prj1(Prj), Rule = 'DERIV_PRJ1_SURJ' |
| 1094 | | ; is_prj2(Prj), Rule = 'DERIV_PRJ2_SURJ'), |
| 1095 | | is_rel(RT,_,Ty1,Ty2), |
| 1096 | | \+ is_inj(RT,Ty1,Ty2), |
| 1097 | | type_expression(Ty1,Info), |
| 1098 | | type_expression(Ty2,Info). |
| 1099 | | simp_rule_with_info(member(Id,RT),truth,'DERIV_ID_BIJ',Info) :- is_identity(Id), is_rel(RT,_,Ty,Ty), type_expression(Ty,Info). |
| 1100 | | simp_rule_with_info(domain_restriction(Ty,R),R,'SIMP_TYPE_DOMRES',Info) :- type_expression(Ty,Info). |
| 1101 | | simp_rule_with_info(range_restriction(R,Ty),R,'SIMP_TYPE_RANRES',Info) :- type_expression(Ty,Info). |
| 1102 | | simp_rule_with_info(domain_subtraction(Ty,R),R,'SIMP_TYPE_DOMSUB',Info) :- type_expression(Ty,Info). |
| 1103 | | simp_rule_with_info(range_subtraction(R,Ty),R,'SIMP_TYPE_RANSUB',Info) :- type_expression(Ty,Info). |
| 1104 | | simp_rule_with_info(image(R,Ty),range(R),'SIMP_TYPE_RELIMAGE',Info) :- type_expression(Ty,Info). |
| 1105 | | simp_rule_with_info(composition(R,Ty),cartesian_product(domain(R),Tb),'SIMP_TYPE_FCOMP_R',Info) :- |
| 1106 | ? | type_expression(Ty,Info), |
| 1107 | | Ty = cartesian_product(_,Tb). |
| 1108 | | simp_rule_with_info(composition(Ty,R),cartesian_product(Ta,range(R)),'SIMP_TYPE_FCOMP_L',Info) :- |
| 1109 | | type_expression(Ty,Info), |
| 1110 | | Ty = cartesian_product(Ta,_). |
| 1111 | | simp_rule_with_info(ring(Ty,R),cartesian_product(domain(R),Tb),'SIMP_TYPE_BCOMP_L',Info) :- |
| 1112 | | type_expression(Ty,Info), |
| 1113 | | Ty = cartesian_product(_,Tb). |
| 1114 | | simp_rule_with_info(ring(R,Ty),cartesian_product(Ta,range(R)),'SIMP_TYPE_BCOMP_R',Info) :- |
| 1115 | | type_expression(Ty,Info), |
| 1116 | | Ty = cartesian_product(Ta,_). |
| 1117 | ? | simp_rule_with_info(domain(Ty),Ta,'SIMP_TYPE_DOM',Info) :- Ty = cartesian_product(Ta,_), type_expression(Ty,Info). |
| 1118 | ? | simp_rule_with_info(range(Ty),Tb,'SIMP_TYPE_RAN',Info) :- Ty = cartesian_product(_,Tb), type_expression(Ty,Info). |
| 1119 | | simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(T,Tb)),'SIMP_CPROD_EQUAL_TYPE',Info) :- |
| 1120 | | is_equality(Eq,cartesian_product(S,T),Ty), |
| 1121 | | Ty = cartesian_product(Ta,Tb), |
| 1122 | | type_expression(Ty,Info). |
| 1123 | | simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(T,Tb)),'SIMP_TYPE_EQUAL_REL',Info) :- |
| 1124 | | is_equality(Eq,relations(S,T),Ty), |
| 1125 | | Ty = cartesian_product(Ta,Tb), |
| 1126 | | type_expression(Ty,Info). |
| 1127 | | simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(R,Ty)),'SIMP_DOMRES_EQUAL_TYPE',Info) :- |
| 1128 | | is_equality(Eq,domain_restriction(S,R),Ty), |
| 1129 | | Ty = cartesian_product(Ta,_), |
| 1130 | | type_expression(Ty,Info). |
| 1131 | | simp_rule_with_info(Eq,conjunct(equal(S,Tb),equal(R,Ty)),'SIMP_RANRES_EQUAL_TYPE',Info) :- |
| 1132 | | is_equality(Eq,range_restriction(R,S),Ty), |
| 1133 | | Ty = cartesian_product(_,Tb), |
| 1134 | | type_expression(Ty,Info). |
| 1135 | | simp_rule_with_info(Eq,conjunct(equal(P,cartesian_product(Ta,Tb)),equal(Q,cartesian_product(Ta,Tc))),'SIMP_DPROD_EQUAL_TYPE',Info) :- |
| 1136 | | is_equality(Eq,direct_product(P,Q),Ty), |
| 1137 | | Ty = cartesian_product(Ta,cartesian_product(Tb,Tc)), |
| 1138 | | type_expression(Ty,Info). |
| 1139 | | simp_rule_with_info(Eq,conjunct(equal(P,cartesian_product(Ta,Tc)),equal(Q,cartesian_product(Tb,Td))),'SIMP_PPROD_EQUAL_TYPE',Info) :- |
| 1140 | | is_equality(Eq,parallel_product(P,Q),Ty), |
| 1141 | | Ty = cartesian_product(cartesian_product(Ta,Tb),cartesian_product(Tc,Td)), |
| 1142 | | type_expression(Ty,Info). |
| 1143 | | simp_rule_with_info(set_subtraction(Ty,set_subtraction(S,T)),union(set_subtraction(Ty,S),T),'DERIV_TYPE_SETMINUS_SETMINUS',Info) :- |
| 1144 | | type_expression(Ty,Info). |
| 1145 | | simp_rule_with_info(Ex,disjunct(less(E,F),greater(E,F)),'DERIV_NOT_EQUAL',Info) :- |
| 1146 | | (Ex = negation(equal(E,F)) ; Ex = not_equal(E,F)), |
| 1147 | | get_meta_info(ids_types,Info,IdsTypes), |
| 1148 | | check_expr_type(E,F,IdsTypes,integer). |
| 1149 | | simp_rule_with_info(equal(S,T),conjunct(subset(S,T),subset(T,S)),'DERIV_EQUAL',Info) :- |
| 1150 | | get_meta_info(ids_types,Info,IdsTypes), |
| 1151 | | check_expr_type(S,T,IdsTypes,set(_)). |
| 1152 | | simp_rule_with_info(subset(S,T),subset(set_subtraction(Ty,T),set_subtraction(Ty,S)),'DERIV_SUBSETEQ',Info) :- |
| 1153 | | get_meta_info(ids_types,Info,IdsTypes), |
| 1154 | | check_expr_type(S,T,IdsTypes,Type), |
| 1155 | | get_type_expression(Type,pow_subset(Ty)). |
| 1156 | | simp_rule_with_info(E,Res,'DERIV_EXPAND_PRJS',Info) :- |
| 1157 | | get_meta_info(ids_types,Info,IdsTypes), |
| 1158 | ? | check_expr_type(E,IdsTypes,Type), |
| 1159 | | get_type_expression(Type,cartesian_product(S,T)), |
| 1160 | | const_rel_type(Ty1,cartesian_product(S,T),S), |
| 1161 | | const_rel_type(Ty2,cartesian_product(S,T),T), |
| 1162 | | Res = couple(function(typeof(event_b_first_projection_v2,Ty1),E),function(typeof(event_b_second_projection_v2,Ty2),E)). |
| 1163 | | /* simp_rule_with_info(event_b_comprehension_set(Ids,E,truth),Ty,'SIMP_SPECIAL_COMPSET_BTRUE',Info) :- |
| 1164 | | get_meta_info(ids_types,Info,IdsTypes), % IdsTypes does not contain bound identifiers |
| 1165 | | pairwise_distict(E,Ids), |
| 1166 | | check_expr_type(E,IdsTypes,Type), |
| 1167 | | get_type_expression(Type,Ty). */ |
| 1168 | ? | simp_rule_with_info(C,Res,Rule,Info) :- distri_r3_info(C,Res,Rule,Info). |
| 1169 | | |
| 1170 | | |
| 1171 | | %pairwise_distict(E,Ids) :- pairwise_distict(E,Ids,_). |
| 1172 | | % |
| 1173 | | %pairwise_distict(couple(E,F),Ids,Ids1) :- pairwise_distict(E,Ids,Ids0), pairwise_distict(F,Ids0,Ids1). |
| 1174 | | %pairwise_distict(E,Ids,Ids0) :- E = '$'(X), atomic(X), select(E,Ids,Ids0). |
| 1175 | | |
| 1176 | | |
| 1177 | | % simp_rule_with_descr/4 |
| 1178 | | simp_rule_with_descr(couple(function(FirstPrj,E),function(SecondPrj,F)),E,Rule,Rule) :- |
| 1179 | | is_prj1(FirstPrj), |
| 1180 | | is_prj2(SecondPrj), |
| 1181 | | Rule = 'SIMP_MAPSTO_PRJ1_PRJ2', |
| 1182 | | equal_terms(E,F). |
| 1183 | | simp_rule_with_descr(domain(successor),Z,Rule,Rule) :- Rule = 'SIMP_DOM_SUCC', is_integer_set(Z). |
| 1184 | | simp_rule_with_descr(range(successor),Z,Rule,Rule) :- Rule = 'SIMP_RAN_SUCC', is_integer_set(Z). |
| 1185 | | simp_rule_with_descr(predecessor,reverse(successor),Rule,Rule) :- Rule = 'DEF_PRED'. |
| 1186 | | simp_rule_with_descr(Expr,negation(member(A,SetB)),'SIMP_BINTER_SING_EQUAL_EMPTY'(A),Descr) :- |
| 1187 | | is_empty(Expr,Inter), |
| 1188 | | is_inter(Inter,SetA,SetB), |
| 1189 | | singleton_set(SetA,A), |
| 1190 | | create_descr('SIMP_BINTER_SING_EQUAL_EMPTY',A,Descr). |
| 1191 | | |
| 1192 | | |
| 1193 | | |
| 1194 | | % simp_rule_with_hyps/4 without info |
| 1195 | | simp_rule_with_hyps(domain(R),E,'DERIV_DOM_TOTALREL'(E),Hyps) :- % derive domain of a total relation |
| 1196 | | member_hyps(member(R,FT),Hyps), is_rel(FT,total,E,_). |
| 1197 | | simp_rule_with_hyps(range(R),F,'DERIV_RAN_SURJREL'(F),Hyps) :- % derive range of a surjective relation |
| 1198 | | member_hyps(member(R,FT),Hyps), is_surj(FT,_,F). |
| 1199 | | simp_rule_with_hyps(function(domain_restriction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMRES',Hyps) :- |
| 1200 | | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). |
| 1201 | | simp_rule_with_hyps(function(domain_subtraction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMSUB',Hyps) :- |
| 1202 | | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). |
| 1203 | | simp_rule_with_hyps(function(range_restriction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANRES',Hyps) :- |
| 1204 | | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). |
| 1205 | | simp_rule_with_hyps(function(range_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANSUB',Hyps) :- |
| 1206 | | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). |
| 1207 | | simp_rule_with_hyps(function(set_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_SETMINUS',Hyps) :- |
| 1208 | | member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_). |
| 1209 | | simp_rule_with_hyps(card(set_subtraction(S,T)),minus(card(S),card(T)),'SIMP_CARD_SETMINUS',Hyps) :- |
| 1210 | | member_hyps(subset(T,S),Hyps), |
| 1211 | | (member_hyps(finite(T),Hyps) |
| 1212 | | ; member_hyps(finite(S),Hyps)). |
| 1213 | | simp_rule_with_hyps(card(set_subtraction(S,set_extension(L))),minus(card(S),card(set_extension(L))),Rule,Hyps) :- |
| 1214 | | Rule = 'SIMP_CARD_SETMINUS_SETENUM', |
| 1215 | ? | all_in_set(L,S,Hyps). |
| 1216 | | 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) |
| 1217 | ? | is_less_eq(L,A,B), is_inequality(Ex,A,B), member(Ex,Hyps). |
| 1218 | | % allow simplifications deeper inside the term: |
| 1219 | | simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,P], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,Q]. |
| 1220 | | simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,P,R], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,Q,R]. |
| 1221 | ? | simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,R,P], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,R,Q]. |
| 1222 | | |
| 1223 | | |
| 1224 | | % ----------------------- |
| 1225 | | |
| 1226 | | or_equal([],_,D,D). |
| 1227 | | or_equal([A|L],E,D,Res) :- or_equal(L,E,disjunct(D,equal(E,A)),Res). |
| 1228 | | |
| 1229 | | and_empty(C,Conj,Op) :- C=..[Op,A,B], and_empty(A,ConjA,Op), and_empty(B,ConjB,Op), !, Conj = conjunct(ConjA,ConjB). |
| 1230 | | and_empty(A,equal(A,empty_set),_). |
| 1231 | | |
| 1232 | ? | 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). |
| 1233 | | and_imp(A,R,implication(R,A),conjunct). |
| 1234 | | and_imp(A,R,implication(A,R),disjunct). |
| 1235 | | |
| 1236 | | union_subset(S,union(A,B),Conj) :- union_subset(S,A,ConjA), union_subset(S,B,ConjB), !, Conj = conjunct(ConjA,ConjB). |
| 1237 | | union_subset(S,A,subset(A,S)). |
| 1238 | | |
| 1239 | | union_subset_member(T,union(A,B),Conj) :- |
| 1240 | | union_subset_member(T,A,ConjA), |
| 1241 | | union_subset_member(T,B,ConjB),!, |
| 1242 | | Conj = conjunct(ConjA,ConjB). |
| 1243 | | union_subset_member(T,SetF,member(F,T)) :- singleton_set(SetF,F), !. |
| 1244 | | union_subset_member(T,A,subset(A,T)). |
| 1245 | | |
| 1246 | | |
| 1247 | | member_union(E,union(A,B),Disj) :- member_union(E,A,DisjA), member_union(E,B,DisjB), !, Disj = disjunct(DisjA,DisjB). |
| 1248 | | member_union(E,A,member(E,A)). |
| 1249 | | |
| 1250 | | subset_inter(S,intersection(A,B),Conj) :- subset_inter(S,A,ConjA), subset_inter(S,B,ConjB), Conj = conjunct(ConjA,ConjB), !. |
| 1251 | | subset_inter(S,A,subset(S,A)). |
| 1252 | | |
| 1253 | | member_intersection(E,intersection(A,B),Conj) :- |
| 1254 | | member_intersection(E,A,ConjA), |
| 1255 | | member_intersection(E,B,ConjB),!, |
| 1256 | | Conj = conjunct(ConjA,ConjB). |
| 1257 | | member_intersection(E,A,member(E,A)). |
| 1258 | | |
| 1259 | | distribute_exists(X,disjunct(A,B),Disj) :- distribute_exists(X,A,DisjA), distribute_exists(X,B,DisjB), !, Disj = disjunct(DisjA,DisjB). |
| 1260 | | distribute_exists(X,P,exists(X,P)). |
| 1261 | | |
| 1262 | | distribute_forall(X,P,conjunct(A,B),Conj) :- |
| 1263 | | distribute_forall(X,P,A,ConjA), |
| 1264 | | distribute_forall(X,P,B,ConjB),!, |
| 1265 | | Conj = conjunct(ConjA,ConjB). |
| 1266 | | distribute_forall(X,P,A,forall(X,P,A)). |
| 1267 | | |
| 1268 | | distribute_binary_minus(minus(X,Y),add(X,YY)) :- distribute_unary_minus(Y,YY). |
| 1269 | | |
| 1270 | | distribute_unary_minus(add(Y,Z),minus(YY,Z)) :- !, distribute_unary_minus(Y,YY). |
| 1271 | | distribute_unary_minus(minus(Y,Z),add(YY,Z)) :- !, distribute_unary_minus(Y,YY). |
| 1272 | | distribute_unary_minus(add(unary_minus(Y),Z),minus(YY,Z)) :- !, distribute_unary_minus(unary_minus(Y),YY). |
| 1273 | | distribute_unary_minus(minus(unary_minus(Y),Z),add(YY,Z)) :- !, distribute_unary_minus(unary_minus(Y),YY). |
| 1274 | | distribute_unary_minus(unary_minus(Y),Y) :- !. |
| 1275 | | distribute_unary_minus(Y,unary_minus(Y)). |
| 1276 | | |
| 1277 | | |
| 1278 | | left_associate_additions(add(X,Expr),Res) :- |
| 1279 | | \+ leftmost_term(Expr,_,_), !, |
| 1280 | | normalize_minus(add(X,Expr),Res). |
| 1281 | | left_associate_additions(add(X,Expr),Res) :- |
| 1282 | | leftmost_term(Expr,Term,Rest), !, |
| 1283 | | normalize_minus(add(add(X,Term),Rest),NewTerm), |
| 1284 | | left_associate_additions(NewTerm,Res). |
| 1285 | | left_associate_additions(X,X). |
| 1286 | | |
| 1287 | | leftmost_term(C,Term,Res) :- |
| 1288 | | C=..[Op,A,B], (Op = add ; Op = minus), |
| 1289 | | functor(A,OpA,2), (OpA = add ; OpA = minus),!, |
| 1290 | | leftmost_term(A,Term,Rest), |
| 1291 | | Res=..[Op,Rest,B]. |
| 1292 | | leftmost_term(add(X,Y),X,Y). |
| 1293 | | leftmost_term(minus(X,Y),X,unary_minus(Y)). |
| 1294 | | |
| 1295 | | normalize_minus(add(X,unary_minus(Y)),minus(XX,Y)) :- !, |
| 1296 | | normalize_minus(X,XX). |
| 1297 | | normalize_minus(Term,Result) :- |
| 1298 | | Term=..[F|Args], !, |
| 1299 | | maplist(normalize_minus,Args,NewArgs), |
| 1300 | | Result=..[F|NewArgs]. |
| 1301 | | normalize_minus(X,X). |
| 1302 | | |
| 1303 | | member_couples(E,F,[Q],_,[member(couple(E,F),Q)]). |
| 1304 | ? | member_couples(E,F,[P|Q],[X|T],[member(couple(E,X),P)|R]) :- member_couples(X,F,Q,T,R). |
| 1305 | | |
| 1306 | | distri_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse(A,UA,Op), distri_reverse(B,UB,Op), !, U=..[Op,UA,UB]. |
| 1307 | | distri_reverse(A,reverse(A),_). |
| 1308 | | |
| 1309 | | 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]. |
| 1310 | | distri_reverse_reverse(A,reverse(A),_). |
| 1311 | | |
| 1312 | | distri_union(union(A,B),Union,Op) :- distri_union(A,L,Op), distri_union(B,R,Op), !, Union = union(L,R). |
| 1313 | | distri_union(A,C,Op) :- C=..[Op,A]. |
| 1314 | | |
| 1315 | | image_union(F,union(A,B),Union) :- image_union(F,A,L), image_union(F,B,R), !, Union = union(L,R). |
| 1316 | | image_union(F,A,image(F,A)). |
| 1317 | | |
| 1318 | | union_image(union(A,B),S,Union) :- union_image(A,S,L), union_image(B,S,R), !, Union = union(L,R). |
| 1319 | | union_image(A,S,image(A,S)). |
| 1320 | | |
| 1321 | | finite_union(union(A,B),Conj) :- finite_union(A,ConjA), finite_union(B,ConjB), !, Conj = conjunct(ConjA,ConjB). |
| 1322 | | finite_union(S,finite(S)). |
| 1323 | | |
| 1324 | | |
| 1325 | | last_overwrite(overwrite(_,B),Res) :- !, last_overwrite(B,Res). |
| 1326 | | last_overwrite(B,B). |
| 1327 | | |
| 1328 | | and_equal_type(intersection(A,B),Ty,Conj) :- and_equal_type(A,Ty,L), and_equal_type(B,Ty,R), !, Conj = conjunct(L,R). |
| 1329 | | and_equal_type(A,Ty,equal(A,Ty)). |
| 1330 | | |
| 1331 | | bwd_to_fwd_comp(ring(R,S),Res) :- |
| 1332 | ? | bwd_to_fwd_comp(R,R2), |
| 1333 | | bwd_to_fwd_comp(S,S2), |
| 1334 | | Res = composition(S2,R2). |
| 1335 | | bwd_to_fwd_comp(X,X) :- X \= ring(_,_). |
| 1336 | | |
| 1337 | | % ------------------ |
| 1338 | | |
| 1339 | | % change order of operation if Op is associative |
| 1340 | | reorder(C,Res,Op) :- |
| 1341 | | C=..[Op,A,B], |
| 1342 | | B=..[Op,L,Rest],!, |
| 1343 | | R=..[Op,A,L], |
| 1344 | | append_to_op(Rest,R,Res,Op). |
| 1345 | | reorder(C,C,Op) :- functor(C,Op,2). |
| 1346 | | |
| 1347 | | append_to_op(C,R,Res,Op) :- |
| 1348 | | C=..[Op,A,B], |
| 1349 | | Inner=..[Op,R,A],!, |
| 1350 | | append_to_op(B,Inner,Res,Op). |
| 1351 | | append_to_op(B,R,C,Op) :- C=..[Op,R,B]. |
| 1352 | | |
| 1353 | | % ------------------ |
| 1354 | | |
| 1355 | | remove_from_op(El,Term,NewTerm,Op) :- |
| 1356 | | op_to_list(Term,List,Op), |
| 1357 | ? | remove_from_list(El,List,List0), |
| 1358 | | list_to_op(List0,NewTerm,Op). |
| 1359 | | |
| 1360 | | remove_from_list(_,[],[]). |
| 1361 | ? | remove_from_list(E,[E|T],T2) :- remove_from_list(E,T,T2). |
| 1362 | | remove_from_list(E,[X|T],[X|T2]) :- X \= E, remove_from_list(E,T,T2). |
| 1363 | | |
| 1364 | | |