| 1 | % Heinrich Heine Universitaet Duesseldorf | |
| 2 | % (c) 2025-2025 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 | :- module(test_sequent_prover,[]). | |
| 6 | ||
| 7 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 8 | :- module_info(group,sequent_prover). | |
| 9 | :- module_info(description,'This module provides tests for the sequent prover.'). | |
| 10 | ||
| 11 | :- use_module(probsrc(self_check)). | |
| 12 | ||
| 13 | test_simp_rule(Rule,Hyp,NewHyp) :- | |
| 14 | ? | sequent_prover:sequent_prover_trans_desc(simplify_hyp(Rule,_),state(sequent([Hyp],truth,success),[]), |
| 15 | state(sequent([NewHyp],truth,success),_),_). | |
| 16 | ||
| 17 | test_transition(Rule,Sequent,NewSequent) :- | |
| 18 | sequent_prover:sequent_prover_trans_desc(Rule,state(Sequent,[]),state(NewSequent,[]),_) ; | |
| 19 | ? | sequent_prover:sequent_prover_trans(Rule,state(Sequent,[]),state(NewSequent,_)). |
| 20 | ||
| 21 | test_simp_rule_with_hyps(Rule,Hyps,Hyp,NewHyp) :- | |
| 22 | ? | sequent_prover:sequent_prover_trans_desc(simplify_hyp(Rule,_),state(sequent([Hyp|Hyps],truth,success),[]), |
| 23 | state(sequent(NewHyps,truth,success),_),_), | |
| 24 | ? | member(NewHyp,NewHyps), |
| 25 | \+ member(NewHyp,Hyps). | |
| 26 | ||
| 27 | test_simp_rule_with_types(Rule,Hyps,Hyp,NewHyp) :- | |
| 28 | ? | sequent_prover:get_scope(Hyps,[],[identifier(IdsTypes)]), |
| 29 | sequent_prover:add_meta_infos(ids_types,[],IdsTypes,Info), | |
| 30 | ? | sequent_prover:sequent_prover_trans_desc(simplify_hyp(Rule,_),state(sequent([Hyp|Hyps],truth,success),Info), |
| 31 | state(sequent(NewHyps,truth,success),_),_), | |
| 32 | ? | member(NewHyp,NewHyps), |
| 33 | \+ member(NewHyp,Hyps). | |
| 34 | ||
| 35 | test_transition_with_types_r(Rule,Hyps,Goal,NewGoal) :- | |
| 36 | ? | sequent_prover:get_scope(Hyps,[],[identifier(IdsTypes)]), |
| 37 | sequent_prover:add_meta_infos(ids_types,[],IdsTypes,Info), | |
| 38 | ? | sequent_prover:trans_with_info(Rule,sequent(Hyps,Goal,success),sequent(Hyps,NewGoal,success),Info). |
| 39 | ||
| 40 | test_transition_with_types_l(Rule,Hyps,Hyp,NewHyp) :- | |
| 41 | ? | sequent_prover:get_scope(Hyps,[],[identifier(IdsTypes)]), |
| 42 | sequent_prover:add_meta_infos(ids_types,[],IdsTypes,Info), | |
| 43 | ? | sequent_prover:trans_with_info(Rule,sequent([Hyp|Hyps],truth,success),sequent(NewHyps,truth,success),Info), |
| 44 | ? | member(NewHyp,NewHyps), |
| 45 | \+ member(NewHyp,Hyps). | |
| 46 | ||
| 47 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_AND_BTRUE',conjunct(truth,'$'(v)),R), R='$'(v) )). | |
| 48 | :- assert_must_succeed((test_simp_rule('SIMP_SPECIAL_AND_BTRUE',conjunct(truth,conjunct('$'(v),truth)),R), | |
| 49 | R=conjunct('$'(v),truth) )). | |
| 50 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_AND_BFALSE',conjunct(conjunct('$'(v),'$'(v)),falsity),R), | |
| 51 | R=falsity)). | |
| 52 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND',conjunct(conjunct('$'(v),'$'(w)),'$'(w)),R), | |
| 53 | R=conjunct('$'(v),'$'(w)) )). | |
| 54 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND',conjunct('$'(v),'$'(v)),R), R='$'(v) )). | |
| 55 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND',conjunct(conjunct(conjunct('$'(v),'$'(u)),'$'(u)),'$'(u)),R), | |
| 56 | R=conjunct('$'(v),'$'(u)) )). | |
| 57 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND_NOT',conjunct(conjunct(negation('$'(v)),'$'(w)),'$'(v)),R), R=falsity )). | |
| 58 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND_NOT',conjunct(negation(equal('$'(w),'$'(v))),equal('$'(v),'$'(w))),R), | |
| 59 | R=falsity )). | |
| 60 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OR_BTRUE',disjunct(disjunct('$'(w),truth),'$'(v)),R), R=truth )). | |
| 61 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OR_BFALSE',disjunct(disjunct(falsity,'$'(v)),falsity),R), | |
| 62 | R=disjunct('$'(v),falsity) )). | |
| 63 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_OR',disjunct('$'(v),'$'(v)),R), R='$'(v))). | |
| 64 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_OR_NOT',disjunct('$'(v),negation('$'(v))),R), R=truth)). | |
| 65 | :- assert_must_succeed(( test_simp_rule('Evaluate tautology',implication(not_equal('$'(w),'$'(v)),truth),R), | |
| 66 | R=truth )). % SIMP_SPECIAL_IMP_BTRUE_R | |
| 67 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_IMP_BTRUE_L',implication(truth,not_equal('$'(w),'$'(v))),R), | |
| 68 | R=not_equal('$'(w),'$'(v)) )). | |
| 69 | :- assert_must_succeed(( test_simp_rule('Evaluate tautology',implication(equal('$'(v),'$'(w)),equal('$'(w),'$'(v))),R), | |
| 70 | R=truth )). % SIMP_MULTI_IMP | |
| 71 | :- assert_must_succeed(( test_simp_rule('Propagate negation',negation(less_equal('$'(v),'$'(w))),R), | |
| 72 | R=greater('$'(v),'$'(w)) )). % SIMP_NOT_LE | |
| 73 | :- assert_must_succeed(( test_simp_rule('Propagate negation',negation(conjunct('$'(v),'$'(w))),R), | |
| 74 | R=disjunct(negation('$'(v)),negation('$'(w))))). % DISTRI_NOT_AND | |
| 75 | :- assert_must_succeed(( test_simp_rule('Propagate negation',negation(conjunct(conjunct('$'(u),'$'(v)),'$'(w))),R), | |
| 76 | R=disjunct(disjunct(negation('$'(u)),negation('$'(v))),negation('$'(w))))). | |
| 77 | :- assert_must_succeed(( test_simp_rule('Propagate negation',negation(implication('$'(u),'$'(v))),R), | |
| 78 | R=conjunct('$'(u),negation('$'(v))))). % DERIV_NOT_IMP | |
| 79 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_NOT_EQUAL_FALSE',negation(equal(boolean_false,'$'(e))),R), | |
| 80 | R=equal('$'(e),boolean_true))). % SIMP_SPECIAL_NOT_EQUAL_FALSE_L | |
| 81 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_NOT_EQUAL_TRUE',negation(equal('$'(e),boolean_true)),R), | |
| 82 | R=equal('$'(e),boolean_false))). % SIMP_SPECIAL_NOT_EQUAL_TRUE_R | |
| 83 | :- assert_must_succeed(( test_simp_rule('SIMP_FORALL_AND', | |
| 84 | forall(['$'(x)],member('$'(x),natural1_set),conjunct(greater('$'(x),0),not_equal('$'(x),'$'(y)))),R), | |
| 85 | R=conjunct(forall(['$'(x)],member('$'(x),natural1_set),greater('$'(x),0)),forall(['$'(x)],member('$'(x),natural1_set),not_equal('$'(x),'$'(y)))))). | |
| 86 | :- assert_must_succeed(( test_simp_rule('SIMP_FORALL_AND',forall(['$'(x),'$'(y)],'$'(p),conjunct(conjunct('$'(v),'$'(w)),'$'(u))),R), | |
| 87 | R=conjunct(conjunct(forall(['$'(x),'$'(y)],'$'(p),'$'(v)),forall(['$'(x),'$'(y)],'$'(p),'$'(w))),forall(['$'(x),'$'(y)],'$'(p),'$'(u))) )). | |
| 88 | :- assert_must_succeed(( test_simp_rule('SIMP_EXISTS_OR',exists(['$'(x)],disjunct('$'(p),'$'(q))),R), | |
| 89 | R=disjunct(exists(['$'(x)],'$'(p)),exists(['$'(x)],'$'(q))) )). | |
| 90 | :- assert_must_succeed(( test_simp_rule('SIMP_FORALL',forall(['$'(x),'$'(y)],greater('$'(x),0),'$'(q)),R), | |
| 91 | R=forall(['$'(x)],greater('$'(x),0),'$'(q)) )). | |
| 92 | :- assert_must_succeed(( test_simp_rule('SIMP_FORALL',forall(['$'(y),'$'(z),'$'(x)],greater('$'(x),0),'$'(q)),R), | |
| 93 | R=forall(['$'(x)],greater('$'(x),0),'$'(q)) )). | |
| 94 | :- assert_must_succeed(( test_simp_rule('SIMP_FORALL',forall(['$'(y),'$'(z),'$'(x)],disjunct(greater('$'(x),0),greater('$'(y),0)),'$'(q)),R), | |
| 95 | R=forall(['$'(y),'$'(x)],disjunct(greater('$'(x),0),greater('$'(y),0)),'$'(q)) )). | |
| 96 | :- assert_must_succeed(( test_simp_rule('SIMP_EQUAL_MAPSTO',equal(couple('$'(e),'$'(f)),couple('$'(g),'$'(h))),R), | |
| 97 | R=conjunct(equal('$'(e),'$'(g)),equal('$'(f),'$'(h))) )). | |
| 98 | :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_IN',event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),'$'(s))),R),R='$'(s) )). | |
| 99 | :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_IN', | |
| 100 | event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),member(couple('$'(x),'$'(y)),'$'(s))),R),R='$'(s) )). | |
| 101 | :- assert_must_fail( test_simp_rule('SIMP_COMPSET_IN', | |
| 102 | event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),set_extension(['$'(w),'$'(x),'$'(y)]))),_) ). | |
| 103 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_SUBSETEQ',subset('$'(s),bool_set),R),R=truth )). | |
| 104 | :- assert_must_succeed((test_simp_rule('Evaluate tautology',subset(set_extension(['$'(red),'$'(blu)]),set_extension(['$'(blu),'$'(red)])),R), | |
| 105 | R=truth )). % SIMP_MULTI_SUBSETEQ | |
| 106 | :- assert_must_succeed(( test_simp_rule('DERIV_SUBSETEQ_BUNION',subset(union(union('$'(r),'$'(b)),'$'(p)),'$'(c)),R), | |
| 107 | R=conjunct(conjunct(subset('$'(r),'$'(c)),subset('$'(b),'$'(c))),subset('$'(p),'$'(c))) )). | |
| 108 | :- assert_must_succeed(( test_simp_rule('DERIV_SUBSETEQ_BINTER',subset('$'(c),intersection('$'(a),'$'(b))),R), | |
| 109 | R=conjunct(subset('$'(c),'$'(a)),subset('$'(c),'$'(b))) )). | |
| 110 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_SETENUM',set_extension(['$'(a),'$'(a),'$'(b),'$'(b)]),R), | |
| 111 | R=set_extension(['$'(a),'$'(b)]) )). | |
| 112 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_BINTER',intersection('$'(a),intersection(empty_set,'$'(w))),R), R=empty_set)). | |
| 113 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_BINTER',intersection('$'(a),intersection('INTEGER','$'(b))),R), | |
| 114 | R=intersection('$'(a),'$'(b)) )). | |
| 115 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_BUNION',union('$'(a),union(pow_subset(bool_set),'$'(b))),R), | |
| 116 | R=pow_subset(bool_set))). | |
| 117 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_SETMINUS',set_subtraction('$'(s),cartesian_product(bool_set,bool_set)),R), | |
| 118 | R=empty_set)). | |
| 119 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_SETMINUS_SETMINUS', | |
| 120 | set_subtraction(bool_set,set_subtraction(bool_set,'$'(s))),R), R='$'(s))). | |
| 121 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_CPROD',cartesian_product('$'(s),empty_set),R), R=empty_set )). | |
| 122 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_CPROD',cartesian_product(cartesian_product('$'(t),'$'(s)),empty_set),R), | |
| 123 | R=empty_set)). % SIMP_SPECIAL_CPROD_R, SIMP_SPECIAL_CPROD_L | |
| 124 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OVERL',overwrite(empty_set,'$'(t)),R), R='$'(t) )). | |
| 125 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OVERL',overwrite(overwrite('$'(t),'$'(s)),empty_set),R), | |
| 126 | R=overwrite('$'(t),'$'(s)) )). | |
| 127 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OVERL',overwrite(overwrite(empty_set,'$'(t)),'$'(s)),R), | |
| 128 | R=overwrite('$'(t),'$'(s)) )). | |
| 129 | :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_BUNION',finite(union('$'(s),'$'(t))),R), R=conjunct(finite('$'(s)),finite('$'(t))) )). | |
| 130 | :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_CONVERSE',finite(reverse(set_extension([couple(1,2)]))),R), | |
| 131 | R=finite(set_extension([couple(1,2)])) )). | |
| 132 | :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_ID_DOMRES',finite(domain_restriction('$'(e),event_b_identity)),R), | |
| 133 | R=finite('$'(e)) )). | |
| 134 | :- assert_must_succeed(( test_simp_rule('DISTRI_AND_OR',conjunct('$'(p),disjunct('$'(q),'$'(r))),R), | |
| 135 | R=disjunct(conjunct('$'(p),'$'(q)),conjunct('$'(p),'$'(r))) )). | |
| 136 | :- assert_must_succeed(( test_simp_rule('DISTRI_AND_OR',conjunct(disjunct(disjunct('$'(q),'$'(s)),'$'(r)),'$'(t)),R), | |
| 137 | R=disjunct(disjunct(conjunct('$'(q),'$'(t)),conjunct('$'(s),'$'(t))),conjunct('$'(r),'$'(t))) )). | |
| 138 | :- assert_must_succeed(( test_simp_rule('DEF_OR',disjunct(disjunct(disjunct('$'(q),'$'(s)),'$'(r)),'$'(t)),R), | |
| 139 | R=implication(negation('$'(q)),disjunct(disjunct('$'(s),'$'(r)),'$'(t))) )). | |
| 140 | :- assert_must_succeed(( test_simp_rule('DISTRI_SUBSETEQ_BUNION_SING',subset(union('$'(s),set_extension(['$'(f)])),'$'(t)),R), | |
| 141 | R=conjunct(subset('$'(s),'$'(t)),member('$'(f),'$'(t))) )). | |
| 142 | :- assert_must_succeed(( test_simp_rule('DISTRI_SUBSETEQ_BUNION_SING', | |
| 143 | subset(union(union('$'(s),set_extension(['$'(f)])),'$'(g)),'$'(t)),R), | |
| 144 | R=conjunct(conjunct(subset('$'(s),'$'(t)),member('$'(f),'$'(t))),subset('$'(g),'$'(t))) )). | |
| 145 | :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_NATURAL',disjunct('$'(p),finite(natural_set)),R), | |
| 146 | R=disjunct('$'(p),falsity))). % subterm | |
| 147 | :- assert_must_succeed(( test_simp_rule('DEF_IN_MAPSTO',member(couple('$'(a),'$'(b)),cartesian_product('$'(n),'$'(m))),R), | |
| 148 | R=conjunct(member('$'(a),'$'(n)),member('$'(b),'$'(m))) )). | |
| 149 | :- assert_must_succeed(( test_simp_rule('DEF_IN_MAPSTO', | |
| 150 | member(couple(couple('$'(a),'$'(b)),'$'(c)),cartesian_product(cartesian_product('$'(n),'$'(m)),'$'(o))),R), | |
| 151 | R=conjunct(member(couple('$'(a),'$'(b)),cartesian_product('$'(n),'$'(m))),member('$'(c),'$'(o))) )). | |
| 152 | :- assert_must_succeed(( test_simp_rule('DEF_IN_POW',member(set_extension(['$'(a)]),pow_subset(natural1_set)),R), | |
| 153 | R=subset(set_extension(['$'(a)]),natural1_set) )). | |
| 154 | :- assert_must_succeed(( test_simp_rule('DEF_IN_POW1',member(set_extension(['$'(a)]),pow1_subset(natural1_set)),R), | |
| 155 | R=conjunct(member(set_extension(['$'(a)]),pow_subset(natural1_set)),not_equal(natural1_set,empty_set)) )). | |
| 156 | :- assert_must_succeed(( test_simp_rule('DEF_SUBSETEQ',subset('$'(s),'$'(t)),R), | |
| 157 | R=forall(['$'(x)],member('$'(x),'$'(s)),member('$'(x),'$'(t))) )). | |
| 158 | :- assert_must_succeed(( test_simp_rule('DEF_SUBSETEQ',subset(set_extension(['$'(x)]),'$'(y)),R), | |
| 159 | R=forall(['$'(z)],member('$'(z),set_extension(['$'(x)])),member('$'(z),'$'(y))) )). % new identifier | |
| 160 | :- assert_must_succeed(( test_simp_rule('DEF_IN_BUNION',member('$'(e),union('$'(x),'$'(y))),R), | |
| 161 | R=disjunct(member('$'(e),'$'(x)),member('$'(e),'$'(y))) )). | |
| 162 | :- assert_must_succeed(( test_simp_rule('DEF_IN_BINTER',member('$'(e),intersection('$'(x),intersection('$'(y),'$'(z)))),R), | |
| 163 | R=conjunct(member('$'(e),'$'(x)),conjunct(member('$'(e),'$'(y)),member('$'(e),'$'(z)))) )). | |
| 164 | :- assert_must_succeed(( test_simp_rule('DEF_IN_SETMINUS',member('$'(e),set_subtraction(set_extension(['$'(x)]),'$'(y))),R), | |
| 165 | R=conjunct(member('$'(e),set_extension(['$'(x)])),negation(member('$'(e),'$'(y)))) )). | |
| 166 | :- assert_must_succeed(( test_simp_rule('DEF_IN_SETENUM',member('$'(e),set_extension([1,2,3])),R), | |
| 167 | R=disjunct(disjunct(equal('$'(e),1),equal('$'(e),2)),equal('$'(e),3)) )). | |
| 168 | :- assert_must_succeed(( test_simp_rule('DEF_IN_KUNION',member(22,general_union('$'(s))),R), | |
| 169 | R=exists(['$'(x)],conjunct(member('$'(x),'$'(s)),member(22,'$'(x)))) )). | |
| 170 | :- assert_must_succeed(( test_simp_rule('DEF_IN_KUNION',member(23,general_union('$'(x))),R), | |
| 171 | R=exists(['$'(y)],conjunct(member('$'(y),'$'(x)),member(23,'$'(y)))) )). | |
| 172 | :- assert_must_succeed(( test_simp_rule('DISTRI_BINTER_SETMINUS',intersection('$'(a),set_subtraction('$'(s),'$'(t))),R), | |
| 173 | R=set_subtraction(intersection('$'(a),'$'(s)),intersection('$'(a),'$'(t))) )). | |
| 174 | :- assert_must_succeed(( test_simp_rule('DISTRI_SETMINUS_BUNION',set_subtraction('$'(a),union('$'(s),'$'(t))),R), | |
| 175 | R=set_subtraction(set_subtraction('$'(a),'$'(s)),'$'(t)) )). | |
| 176 | :- assert_must_succeed(( test_simp_rule('DERIV_SUBSETEQ_SETMINUS_L',subset(set_subtraction('$'(a),'$'(s)),'$'(t)),R), | |
| 177 | R=subset('$'(a),union('$'(s),'$'(t))) )). | |
| 178 | :- assert_must_succeed(( test_simp_rule('SIMP_DOM_SETENUM',domain(set_extension([couple(1,2),couple(2,3)])),R), | |
| 179 | R=set_extension([1,2]) )). | |
| 180 | :- assert_must_succeed(( test_simp_rule('SIMP_DOM_SETENUM',domain(set_extension([couple(1,2),couple(1,3)])),R), | |
| 181 | R=set_extension([1]) )). | |
| 182 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_OVERL_CPROD',overwrite(overwrite(overwrite('$'(r),'$'(s)),bool_set),'$'(t)),R), | |
| 183 | R=overwrite(bool_set,'$'(t)) )). | |
| 184 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_OVERL_CPROD',overwrite(overwrite(overwrite('$'(t),'$'(s)),'$'(r)),bool_set),R), | |
| 185 | R=bool_set )). | |
| 186 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_OVERL_CPROD',overwrite(overwrite(overwrite(bool_set,'$'(s)),bool_set),'$'(r)),R), | |
| 187 | R=overwrite(bool_set,'$'(r)) )). | |
| 188 | :- assert_must_succeed(( test_simp_rule('SIMP_DPROD_CPROD', | |
| 189 | direct_product(cartesian_product('$'(a),'$'(b)),cartesian_product('$'(c),'$'(d))),R), | |
| 190 | R=cartesian_product(intersection('$'(a),'$'(c)),cartesian_product('$'(b),'$'(d))) )). | |
| 191 | :- assert_must_succeed(( test_simp_rule('SIMP_PPROD_CPROD', | |
| 192 | parallel_product(cartesian_product('$'(s),'$'(t)),cartesian_product('$'(u),'$'(v))),R), | |
| 193 | R=cartesian_product(cartesian_product('$'(s),'$'(u)),cartesian_product('$'(t),'$'(v))) )). | |
| 194 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_RELIMAGE_CPROD_SING', | |
| 195 | image(cartesian_product(set_extension(['$'(e)]),'$'(s)),set_extension(['$'(e)])),R),R='$'(s) )). | |
| 196 | :- assert_must_succeed(( test_simp_rule('SIMP_CONVERSE_SETENUM', | |
| 197 | reverse(set_extension([couple('$'(a),'$'(b)),couple('$'(c),'$'(d))])),R), | |
| 198 | R=set_extension([couple('$'(b),'$'(a)),couple('$'(d),'$'(c))]) )). | |
| 199 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_REL_R',partial_function('$'(s),empty_set),R),R=set_extension([empty_set]) )). | |
| 200 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_REL_R',surjection_relation('$'(s),empty_set),R), | |
| 201 | R=set_extension([empty_set]) )). | |
| 202 | :- assert_must_fail( test_simp_rule('SIMP_SPECIAL_REL_R',total_relation('$'(s),empty_set),_) ). | |
| 203 | :- assert_must_succeed(( test_simp_rule('SIMP_DOM_LAMBDA', | |
| 204 | domain(event_b_comprehension_set(['$'(x),'$'(y)],couple(add('$'(x),'$'(x)),'$'(y)),member(couple('$'(x),'$'(y)),'$'(p)))),R), | |
| 205 | R=event_b_comprehension_set(['$'(x),'$'(y)],add('$'(x),'$'(x)),member(couple('$'(x),'$'(y)),'$'(p))) )). | |
| 206 | :- assert_must_fail( test_simp_rule('SIMP_DOM_LAMBDA', | |
| 207 | domain(event_b_comprehension_set(['$'(x),'$'(y)],add('$'(x),'$'(x)),member(couple('$'(x),'$'(y)),'$'(p)))),_) ). | |
| 208 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LL',function(set_extension([couple('$'(a),1)]),'$'(x)),R), | |
| 209 | R=1)). | |
| 210 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LL', | |
| 211 | function(set_extension([couple(1,1),couple(2,1),couple(3,1)]),1),R),R=1 )). | |
| 212 | :- assert_must_fail( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LL', | |
| 213 | function(set_extension([couple(1,1),couple(2,2),couple(3,1)]),1),_) ). | |
| 214 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LR', | |
| 215 | function(set_extension([couple(1,1),couple(2,3),couple(4,5)]),2),R),R=3 )). | |
| 216 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LR', | |
| 217 | function(set_extension([couple(add('$'(x),1),'$'(y))]),add(1,'$'(x))),R),R='$'(y) )). | |
| 218 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_OVERL_SETENUM', | |
| 219 | function(overwrite(overwrite('$'(r),'$'(s)),set_extension([couple('$'(x),'$'(y))])),'$'(x)),R),R='$'(y) )). | |
| 220 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_BUNION_SETENUM', | |
| 221 | function(union(union('$'(r),'$'(s)),set_extension([couple(1,2),couple(2,'$'(x))])),2),R),R='$'(x) )). | |
| 222 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_BUNION_SETENUM', | |
| 223 | function(union(set_extension([couple(1,2),couple(2,'$'(x))]),union('$'(r),'$'(s))),2),R),R='$'(x) )). | |
| 224 | :- assert_must_succeed(( test_simp_rule('SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM', | |
| 225 | function(set_extension([couple(1,2),couple(2,3),couple(2,4)]),function(set_extension([couple(4,2),couple(3,2),couple(2,1)]),'$'(x))),R), | |
| 226 | R='$'(x) )). | |
| 227 | :- assert_must_succeed(( test_simp_rule_with_hyps('SIMP_FUNIMAGE_DOMRES',[member('$'(f),total_function('$'(a),'$'(b)))], | |
| 228 | function(domain_restriction('$'(e),'$'(f)),'$'(g)),R), | |
| 229 | R=function('$'(f),'$'(g)) )). | |
| 230 | :- assert_must_succeed(( test_simp_rule('DEF_EQUAL_FUNIMAGE',equal(function('$'(f),'$'(x)),'$'(y)),R), | |
| 231 | R=member(couple('$'(x),'$'(y)),'$'(f)) )). | |
| 232 | :- assert_must_succeed(( test_simp_rule('DEF_EQUAL_FUNIMAGE',equal(function('$'(f),couple('$'(x),'$'(z))),'$'(y)),R), | |
| 233 | R=member(couple(couple('$'(x),'$'(z)),'$'(y)),'$'(f)) )). | |
| 234 | :- assert_must_succeed(( test_simp_rule('DEF_BCOMP',ring(ring(ring('$'(a),'$'(b)),'$'(c)),'$'(d)),R), | |
| 235 | R=composition(composition(composition('$'(d),'$'(c)),'$'(b)),'$'(a)) )). | |
| 236 | :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_SING', | |
| 237 | composition(set_extension([couple('$'(e),'$'(f))]),set_extension([couple('$'(f),'$'(g))])),R), R=set_extension([couple('$'(e),'$'(g))]) )). | |
| 238 | :- assert_must_succeed(( test_simp_rule('DEF_IN_DOM',member('$'(a),domain('$'(r))),R), | |
| 239 | R=exists(['$'(x)],member(couple('$'(a),'$'(x)),'$'(r))) )). | |
| 240 | :- assert_must_succeed(( test_simp_rule('DEF_IN_DOM',member('$'(x),domain('$'(r))),R), | |
| 241 | R=exists(['$'(y)],member(couple('$'(x),'$'(y)),'$'(r))) )). | |
| 242 | :- assert_must_succeed(( test_simp_rule('DEF_IN_DOM',member('$'(a),domain(set_extension([couple(1,'$'(x))]))),R), | |
| 243 | R=exists(['$'(y)],member(couple('$'(a),'$'(y)),set_extension([couple(1,'$'(x))]))) )). | |
| 244 | :- assert_must_succeed(( test_simp_rule('DEF_IN_FCOMP', | |
| 245 | member(couple('$'(a),'$'(b)),composition(event_b_identity,set_extension([couple(0,1)]))),R), | |
| 246 | R=exists(['$'(x)],conjunct(member(couple('$'(a),'$'(x)),event_b_identity),member(couple('$'(x),'$'(b)),set_extension([couple(0,1)])))))). | |
| 247 | :- assert_must_succeed(( test_simp_rule('DEF_IN_FCOMP',member(couple('$'(a),'$'(x)),composition(composition('$'(r),'$'(s)),'$'(t))),R), | |
| 248 | R=exists(['$'(y1),'$'(y2)],conjunct(conjunct(member(couple('$'(a),'$'(y1)),'$'(r)), | |
| 249 | member(couple('$'(y1),'$'(y2)),'$'(s))),member(couple('$'(y2),'$'(x)),'$'(t)))) )). | |
| 250 | :- assert_must_succeed(( test_simp_rule('DISTRI_DPROD_BUNION',direct_product('$'(r),union('$'(s),'$'(t))),R), | |
| 251 | R=union(direct_product('$'(r),'$'(s)),direct_product('$'(r),'$'(t))) )). % distri_r | |
| 252 | :- assert_must_fail( test_simp_rule('DISTRI_DPROD_BUNION',direct_product(union('$'(s),'$'(t)),'$'(r)),_) ). | |
| 253 | :- assert_must_succeed(( test_simp_rule('DISTRI_OVERL_BUNION_L',overwrite(union('$'(p),'$'(q)),'$'(r)),R), | |
| 254 | R=union(overwrite('$'(p),'$'(r)),overwrite('$'(q),'$'(r))) )). % distri_l | |
| 255 | :- assert_must_fail( test_simp_rule('DISTRI_OVERL_BUNION_L',overwrite('$'(r),union('$'(p),'$'(q))),_) ). | |
| 256 | :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_BUNION_L',domain_subtraction(union('$'(p),'$'(q)),'$'(r)),R), | |
| 257 | R=intersection(domain_subtraction('$'(p),'$'(r)),domain_subtraction('$'(q),'$'(r))) )). | |
| 258 | :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_BUNION',reverse(union(union('$'(r),'$'(b)),'$'(p))),R), | |
| 259 | R=union(union(reverse('$'(r)),reverse('$'(b))),reverse('$'(p))) )). | |
| 260 | :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_FCOMP', | |
| 261 | reverse(composition('$'(r),'$'(b))),R), R=composition(reverse('$'(b)),reverse('$'(r))) )). | |
| 262 | :- assert_must_succeed(( test_simp_rule('DISTRI_RAN_BUNION',range(union(union('$'(r),'$'(b)),'$'(c))),R), | |
| 263 | R=union(union(range('$'(r)),range('$'(b))),range('$'(c))) )). | |
| 264 | :- assert_must_succeed(( test_simp_rule_with_hyps('DERIV_DOM_TOTALREL',[member('$'(r),total_function('$'(a),'$'(b)))], | |
| 265 | equal('$'(f),domain('$'(r))),R), R=equal('$'(f),'$'(a)) )). | |
| 266 | :- assert_must_fail( test_simp_rule_with_hyps('DERIV_DOM_TOTALREL',[member('$'(r),relations('$'(a),'$'(b)))], | |
| 267 | equal('$'(f),domain('$'(r))),_) ). | |
| 268 | :- assert_must_succeed(( test_simp_rule('DERIV_MULTI_IN_BUNION',member('$'(r),union('$'(a),set_extension(['$'(r)]))),R), R=truth )). | |
| 269 | :- assert_must_succeed(( test_simp_rule('SIMP_SETMINUS_EQUAL_EMPTY',equal(empty_set,set_subtraction('$'(r),'$'(a))),R), | |
| 270 | R=subset('$'(r),'$'(a)) )). | |
| 271 | :- assert_must_succeed(( test_simp_rule('SIMP_SETMINUS_EQUAL_EMPTY',equal(set_subtraction('$'(r),'$'(a)),empty_set),R), | |
| 272 | R=subset('$'(r),'$'(a)) )). | |
| 273 | :- assert_must_succeed(( test_simp_rule('SIMP_SETMINUS_EQUAL_EMPTY',subset(set_subtraction('$'(r),'$'(a)),empty_set),R), | |
| 274 | R=subset('$'(r),'$'(a)) )). | |
| 275 | :- assert_must_succeed(( test_simp_rule('SIMP_FCOMP_EQUAL_EMPTY',equal(empty_set,composition('$'(r),'$'(a))),R), | |
| 276 | R=equal(intersection(range('$'(r)),domain('$'(a))),empty_set) )). | |
| 277 | :- assert_must_succeed(( test_simp_rule('SIMP_OVERL_EQUAL_EMPTY',equal(empty_set,overwrite(overwrite('$'(r),'$'(a)),'$'(b))),R), | |
| 278 | R=conjunct(conjunct(equal('$'(r),empty_set),equal('$'(a),empty_set)),equal('$'(b),empty_set)) )). | |
| 279 | :- assert_must_succeed(( test_simp_rule('SIMP_MIN_BUNION_SING',min(union('$'(s),set_extension([min('$'(t))]))),R), | |
| 280 | R=min(union('$'(s),'$'(t))) )). | |
| 281 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_MIN',min(set_extension(['$'(a),'$'(t),3,0,1])),R),R=min(set_extension(['$'(a),'$'(t),0])))). | |
| 282 | :- assert_must_succeed(( test_simp_rule_with_hyps('SIMP_CARD_SETMINUS',[finite('$'(s)),subset('$'(t),'$'(s))], | |
| 283 | not_equal(0,card(set_subtraction('$'(s),'$'(t)))),R), R=not_equal(0,minus(card('$'(s)),card('$'(t)))) )). | |
| 284 | :- assert_must_succeed(( test_simp_rule_with_hyps('SIMP_CARD_SETMINUS_SETENUM', | |
| 285 | [member('$'(e),'$'(s)),member('$'(f),'$'(s)),member('$'(g),'$'(s))], | |
| 286 | not_equal(0,card(set_subtraction('$'(s),set_extension(['$'(e),'$'(f),'$'(g)])))),R), | |
| 287 | R=not_equal(0,minus(card('$'(s)),card(set_extension(['$'(e),'$'(f),'$'(g)])))) )). | |
| 288 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_CARD_UPTO',card(interval(1,2)),R), R=2 )). | |
| 289 | :- assert_must_fail( test_simp_rule('SIMP_LIT_CARD_UPTO',card(interval(2,'$'(drei))),_) ). | |
| 290 | :- assert_must_succeed(( test_simp_rule('DERIV_NOT_EQUAL',not_equal('$'(e),1),R), R=disjunct(greater('$'(e),1),less('$'(e),1)) )). | |
| 291 | :- assert_must_fail( test_simp_rule('DERIV_NOT_EQUAL',not_equal('$'(e),'$'(f)),_) ). | |
| 292 | :- assert_must_succeed(( test_simp_rule_with_types('DERIV_NOT_EQUAL',[member('$'(f),natural_set)],not_equal('$'(e),'$'(f)),R), | |
| 293 | R=disjunct(greater('$'(f),'$'(e)),less('$'(f),'$'(e))) )). | |
| 294 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_0',multiplication(multiplication('$'(i),0),'$'(e)),R), R=0 )). | |
| 295 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_1',multiplication(multiplication('$'(i),1),'$'(e)),R), R=multiplication('$'(i),'$'(e)) )). | |
| 296 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_MINUS_ODD', | |
| 297 | multiplication(multiplication(unary_minus('$'(i)),1),'$'(e)),R), R=unary_minus(multiplication(multiplication('$'(i),1),'$'(e))) )). | |
| 298 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_MINUS_ODD', | |
| 299 | multiplication(multiplication('$'(i),-1),'$'(e)),R), R=unary_minus(multiplication(multiplication('$'(i),1),'$'(e))) )). | |
| 300 | :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_MINUS_EVEN', | |
| 301 | multiplication(multiplication(unary_minus('$'(i)),-1),'$'(e)),R), R=multiplication(multiplication('$'(i),1),'$'(e)) )). | |
| 302 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_MINUS',unary_minus(1),R), R= -1 )). | |
| 303 | :- assert_must_fail( test_simp_rule('SIMP_LIT_MINUS',unary_minus('$'(a)),_) ). | |
| 304 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_GT',greater(1,1),R), R=falsity )). | |
| 305 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_GT',greater(2,1),R), R=truth )). | |
| 306 | :- assert_must_succeed(( test_simp_rule('SIMP_DIV_MINUS',div(-12,unary_minus('$'(x))),R), R=div(12,'$'(x)) )). | |
| 307 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_LT',less(0,multiplication(1000000,0)),R), R=falsity )). | |
| 308 | :- assert_must_succeed(( test_simp_rule('Evaluate tautology',less_equal(0,multiplication(1000,0)),R), R=truth )). % SIMP_MULTI_LE | |
| 309 | :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_DIV_PROD', | |
| 310 | equal(1,div(multiplication(multiplication('$'(y),'$'(e)),'$'(x)),'$'(e))),R), R=equal(1,multiplication('$'(y),'$'(x))) )). | |
| 311 | :- assert_must_succeed(( test_simp_rule('Evaluate tautology',member(0,'NATURAL'),R), R=truth )). % SIMP_LIT_IN_NATURAL | |
| 312 | :- assert_must_fail( test_simp_rule('Evaluate tautology',member(-1,'NATURAL'),_) ). | |
| 313 | :- assert_must_succeed(( test_simp_rule('Evaluate tautology',member(1,'NATURAL1'),R), R=truth )). % SIMP_LIT_IN_NATURAL1 | |
| 314 | :- assert_must_fail( test_simp_rule('Evaluate tautology',member(0,'NATURAL1'),_) ). | |
| 315 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_UPTO',interval(1,0),R),R=empty_set )). | |
| 316 | :- assert_must_fail( test_simp_rule('SIMP_LIT_UPTO',interval(0,0),_) ). | |
| 317 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_IN_MINUS_NATURAL',member(unary_minus(1),natural_set),R),R=falsity )). | |
| 318 | :- assert_must_succeed(( test_simp_rule('SIMP_LIT_IN_MINUS_NATURAL',member(-1,natural_set),R),R=falsity )). | |
| 319 | :- assert_must_succeed(( test_simp_rule('SIMP_MINUS_MINUS',unary_minus(unary_minus('$'(e))),R),R='$'(e) )). | |
| 320 | :- assert_must_succeed(( test_simp_rule('SIMP_MINUS_MINUS',unary_minus(-13),R),R=13 )). | |
| 321 | ||
| 322 | ||
| 323 | :- assert_must_succeed(( test_transition(fun_image_goal, | |
| 324 | sequent([member('$'(f),partial_function(natural_set,bool_set))],equal('$'(t),function('$'(f),'$'(e))),success),R), | |
| 325 | R= sequent([member('$'(f),partial_function(natural_set,bool_set)),member(function('$'(f),'$'(e)),bool_set)], % new Hyp | |
| 326 | equal('$'(t),function('$'(f),'$'(e))),success) )). | |
| 327 | :- assert_must_succeed(( test_transition(subset_inter, | |
| 328 | sequent([subset('$'(x),'$'(u))],equal(intersection('$'(x),'$'(u)),empty_set),success),R), | |
| 329 | R= sequent([subset('$'(x),'$'(u))],equal('$'(x),empty_set),success) )). | |
| 330 | :- assert_must_succeed(( test_transition(in_inter, | |
| 331 | sequent([member('$'(e),'$'(t))],equal(intersection('$'(t),set_extension(['$'(e)])),empty_set),success),R), | |
| 332 | R= sequent([member('$'(e),'$'(t))],equal(set_extension(['$'(e)]),empty_set),success) )). | |
| 333 | :- assert_must_succeed(( test_transition_with_types_r(deriv_equal_card, | |
| 334 | [equal('$'(s),set_extension([1,2])),equal('$'(t),set_extension([3,4]))],equal(card('$'(s)),card('$'(t))),R), | |
| 335 | R= equal('$'(s),'$'(t)) )). | |
| 336 | :- assert_must_fail( test_transition_with_types_r(deriv_equal_card, | |
| 337 | [equal('$'(s),set_extension([1])),equal('$'(t),set_extension([boolean_false]))],equal(card('$'(s)),card('$'(t))),_) ). | |
| 338 | :- assert_must_succeed(( test_transition_with_types_r(deriv_le_card, | |
| 339 | [member('$'(s),pow1_subset(integer_set)),subset('$'(t),natural1_set)],less_equal(card('$'(s)),card('$'(t))),R), | |
| 340 | R= subset('$'(s),'$'(t)) )). | |
| 341 | :- assert_must_fail( test_transition_with_types_r(deriv_le_card, | |
| 342 | [subset('$'(s),bool_set),subset('$'(t),natural1_set)],less_equal(card('$'(s)),card('$'(t))),_) ). | |
| 343 | ||
| 344 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),cartesian_product(integer_set,bool_set)),R), | |
| 345 | R=cartesian_product(domain('$'(r)),bool_set) )). | |
| 346 | :- assert_must_fail( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),pow_subset(integer_set,bool_set)),_) ). | |
| 347 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),cartesian_product(integer_set,bool_set)),R), | |
| 348 | R=cartesian_product(domain('$'(r)),bool_set) )). | |
| 349 | :- assert_must_fail( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),pow_subset(integer_set,bool_set)),_) ). | |
| 350 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_DOM',domain(cartesian_product(integer_set,bool_set)),R), | |
| 351 | R=integer_set )). | |
| 352 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_DOM',domain(cartesian_product(cartesian_product(integer_set,bool_set),bool_set)),R), | |
| 353 | R=cartesian_product(integer_set,bool_set) )). | |
| 354 | :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_RAN',range(cartesian_product(integer_set,bool_set)),R), | |
| 355 | R=bool_set )). | |
| 356 | :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_EQUAL', | |
| 357 | event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),conjunct(member('$'(y),natural_set),equal('$'(x),1))),R), | |
| 358 | R=event_b_comprehension_set(['$'(y)],couple(1,'$'(y)),member('$'(y),natural_set)) )). | |
| 359 | :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_EQUAL', | |
| 360 | event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),conjunct(member('$'(x),natural_set),equal('$'(y),1))),R), | |
| 361 | R=event_b_comprehension_set(['$'(x)],couple('$'(x),1),member('$'(x),natural_set)) )). | |
| 362 | :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_EQUAL', | |
| 363 | event_b_comprehension_set(['$'(x),'$'(y),'$'(z)],couple(couple('$'(x),'$'(z)),'$'(y)), | |
| 364 | conjunct(member('$'(y),natural_set),equal(couple('$'(x),'$'(z)),'$'(e)))),R), | |
| 365 | R=event_b_comprehension_set(['$'(y)],couple('$'(e),'$'(y)),member('$'(y),natural_set)) )). | |
| 366 | :- assert_must_succeed(( test_simp_rule('SIMP_IN_COMPSET', | |
| 367 | member('$'(f),event_b_comprehension_set(['$'(x),'$'(y)],add('$'(x),'$'(y)), | |
| 368 | conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),R), | |
| 369 | R=exists(['$'(x),'$'(y)],conjunct(conjunct(member('$'(x),natural_set),member('$'(y),natural_set)),equal(add('$'(x),'$'(y)),'$'(f)))) )). | |
| 370 | :- assert_must_fail( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT', | |
| 371 | member('$'(a),event_b_comprehension_set(['$'(x)],couple('$'(x),add('$'(x),1)),member('$'(x),set_extension([3,12])))),_) ). | |
| 372 | :- assert_must_succeed(( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT', | |
| 373 | member('$'(a),event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),set_extension([3,12])))),R), | |
| 374 | R=member('$'(a),set_extension([3,12])) )). | |
| 375 | :- assert_must_succeed(( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT', | |
| 376 | member(couple('$'(a),'$'(b)),event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)), | |
| 377 | conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),R), | |
| 378 | R=conjunct(member('$'(a),natural_set),member('$'(b),natural_set)) )). | |
| 379 | :- assert_must_fail( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT',member('$'(a), | |
| 380 | event_b_comprehension_set(['$'(x),'$'(y)],'$'(x),conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),_) ). | |
| 381 | :- assert_must_succeed(( test_simp_rule('SIMP_FUNIMAGE_LAMBDA', | |
| 382 | equal(5,function(event_b_comprehension_set(['$'(x)],couple('$'(x),add('$'(x),1)),member('$'(x),natural_set)),'$'(y))),R), | |
| 383 | R=equal(5,add('$'(y),1)) )). | |
| 384 | :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_LAMBDA', | |
| 385 | finite(event_b_comprehension_set(['$'(x)],couple('$'(x),add('$'(x),1)),member('$'(x),'$'(set)))),R), | |
| 386 | R=finite(event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),'$'(set)))) )). | |
| 387 | :- assert_must_fail( test_simp_rule('SIMP_FINITE_LAMBDA', | |
| 388 | finite(event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)), | |
| 389 | conjunct(member('$'(x),'$'(set)),member('$'(y),'$'(set))))),_) ). | |
| 390 | :- assert_must_fail( test_simp_rule('SIMP_FINITE_LAMBDA', | |
| 391 | finite(event_b_comprehension_set(['$'(x)],couple(1,'$'(x)),member('$'(x),'$'(set)))),_) ). | |
| 392 | :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_LAMBDA', | |
| 393 | finite(event_b_comprehension_set(['$'(x)],couple('$'(x),1),member('$'(x),'$'(set)))),R), | |
| 394 | R=finite(event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),'$'(set)))) )). | |
| 395 | :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_DOMRES', | |
| 396 | composition(domain_restriction('$'(s),'$'(p)),'$'(q)),R),R=domain_restriction('$'(s),composition('$'(p),'$'(q))) )). | |
| 397 | :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_DOMSUB', | |
| 398 | composition('$'(t),composition(domain_subtraction('$'(s),'$'(p)),'$'(q))),R), | |
| 399 | R=composition('$'(t),domain_subtraction('$'(s),composition('$'(p),'$'(q)))) )). | |
| 400 | :- assert_must_fail( test_simp_rule('DERIV_FCOMP_RANRES',composition(range_restriction('$'(s),'$'(p)),'$'(q)),_) ). | |
| 401 | :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_RANRES', | |
| 402 | composition('$'(p),range_restriction('$'(q),'$'(s))),R), | |
| 403 | R=range_restriction(composition('$'(p),'$'(q)),'$'(s)) )). | |
| 404 | :- assert_must_succeed(( test_simp_rule('SIMP_BCOMP_ID', | |
| 405 | ring(ring(ring('$'(r),domain_restriction('$'(s),event_b_identity)),domain_restriction('$'(t),event_b_identity)),'$'(o)),R), | |
| 406 | R=ring(ring('$'(r),domain_restriction(intersection('$'(s),'$'(t)),event_b_identity)),'$'(o)) )). | |
| 407 | :- assert_must_succeed(( test_simp_rule('SIMP_BCOMP_ID', | |
| 408 | ring(ring(domain_restriction('$'(s),event_b_identity),domain_subtraction('$'(t),event_b_identity)),'$'(r)),R), | |
| 409 | R=ring(domain_restriction(set_subtraction('$'(s),'$'(t)),event_b_identity),'$'(r)) )). | |
| 410 | :- assert_must_succeed(( test_simp_rule('SIMP_BCOMP_ID', | |
| 411 | ring(ring(domain_subtraction('$'(s),event_b_identity),domain_subtraction('$'(t),event_b_identity)),'$'(r)),R), | |
| 412 | R=ring(domain_subtraction(union('$'(s),'$'(t)),event_b_identity),'$'(r)) )). | |
| 413 | :- assert_must_succeed(( test_simp_rule('SIMP_FCOMP_ID', | |
| 414 | composition(composition(domain_restriction('$'(s),event_b_identity), | |
| 415 | domain_restriction('$'(t),event_b_identity)),domain_subtraction('$'(q),event_b_identity)),R), | |
| 416 | R=domain_restriction(set_subtraction(intersection('$'(s),'$'(t)),'$'(q)),event_b_identity) )). | |
| 417 | :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BUNION_R', | |
| 418 | range_subtraction('$'(r),union('$'(s),'$'(t))),R), | |
| 419 | R=intersection(range_subtraction('$'(r),'$'(s)),range_subtraction('$'(r),'$'(t))) )). | |
| 420 | :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BUNION_L', | |
| 421 | range_subtraction(union('$'(s),'$'(t)),'$'(r)),R), | |
| 422 | R=union(range_subtraction('$'(s),'$'(r)),range_subtraction('$'(t),'$'(r))) )). | |
| 423 | :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BINTER_R', | |
| 424 | range_subtraction('$'(r),intersection(intersection('$'(s),'$'(t)),'$'(u))),R), | |
| 425 | R=union(union(range_subtraction('$'(r),'$'(s)),range_subtraction('$'(r),'$'(t))),range_subtraction('$'(r),'$'(u))) )). | |
| 426 | ||
| 427 | :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[subset('$'(s),natural_set),subset('$'(t),natural_set)], | |
| 428 | equal('$'(s),'$'(t)),R), R=conjunct(subset('$'(s),'$'(t)),subset('$'(t),'$'(s))) )). | |
| 429 | :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[equal('$'(s),natural_set)],equal('$'(s),set_extension([4])),R), | |
| 430 | R=conjunct(subset('$'(s),set_extension([4])),subset(set_extension([4]),'$'(s))) )). | |
| 431 | :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[member('$'(s),pow_subset(bool_set))], | |
| 432 | equal(set_extension([boolean_true]),'$'(s)),R), | |
| 433 | R=conjunct(subset(set_extension([boolean_true]),'$'(s)),subset('$'(s),set_extension([boolean_true]))) )). | |
| 434 | :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[],equal(set_extension([1]),set_extension([1])),R), | |
| 435 | R=conjunct(subset(set_extension([1]),set_extension([1])),subset(set_extension([1]),set_extension([1]))) )). | |
| 436 | :- assert_must_succeed(( test_simp_rule_with_types('DERIV_SUBSETEQ',[subset('$'(s),natural_set),subset('$'(t),natural_set)], | |
| 437 | subset('$'(s),'$'(t)),R),R=subset(set_subtraction('INTEGER','$'(t)),set_subtraction('INTEGER','$'(s))) )). | |
| 438 | ||
| 439 | :- assert_must_succeed(( test_transition_with_types_r(all_r,[equal('$'(y),0)], | |
| 440 | forall(['$'(x)],member('$'(x),natural_set),greater_equal('$'(x),'$'(y))),R), | |
| 441 | R=implication(member('$'(x),natural_set),greater_equal('$'(x),'$'(y))) )). | |
| 442 | :- assert_must_succeed(( test_transition_with_types_r(all_r,[member('$'(x),bool_set),equal('$'(y),0)], | |
| 443 | forall(['$'(x)],member('$'(x),natural_set),greater_equal('$'(x),'$'(y))),R), | |
| 444 | R=implication(member(NewId,natural_set),greater_equal(NewId,'$'(y))), NewId \= '$'(x), NewId \= '$'(y) )). | |
| 445 | ||
| 446 | :- assert_must_succeed(( test_transition_with_types_l(xst_l,[],exists(['$'(x)],member('$'(x),bool_set)),R), | |
| 447 | R=member('$'(x),bool_set) )). | |
| 448 | :- assert_must_succeed(( test_transition_with_types_l(xst_l,[equal('$'(x),1)],exists(['$'(x)],member('$'(x),bool_set)),R), | |
| 449 | R=member(NewId,bool_set), NewId \= '$'(x) )). | |
| 450 | :- assert_must_succeed(( test_transition_with_types_l(xst_l,[equal('$'(x),1)], | |
| 451 | exists(['$'(x),'$'(y)],conjunct(member('$'(x),bool_set),equal('$'(x),'$'(y)))),R), | |
| 452 | R=conjunct(member(Id1,bool_set),equal(Id1,Id2)), Id1 \= Id2, Id1 \= '$'(x), Id2 \= '$'(y) )). | |
| 453 | ||
| 454 | :- assert_must_fail( sequent_prover:wd_strict_term(conjunct(truth,equal(1,1))) ). | |
| 455 | :- assert_must_succeed(( sequent_prover:wd_strict_term(equivalence(truth,equal(1,1))) )). | |
| 456 | :- assert_must_succeed(( sequent_prover:rewrite_once('$'(x),'$'(y),equal('$'(x),'$'(x)),R), R=equal('$'(y),'$'(x)) )). | |
| 457 | :- assert_must_succeed(( sequent_prover:is_subterm(equal(_,_),conjunct(truth,equal('$'(x),'$'(x)))) )). | |
| 458 | :- assert_must_succeed(( sequent_prover:split_composition(composition('$'(f),'$'(g)),L,R), L='$'(f), R='$'(g) )). | |
| 459 | :- assert_must_succeed(( sequent_prover:split_composition(composition(composition('$'(f),'$'(g)),'$'(h)),composition('$'(f),'$'(g)),'$'(h)) )). | |
| 460 | :- assert_must_succeed(( sequent_prover:split_composition(composition(composition('$'(f),'$'(g)),'$'(h)),'$'(f),composition('$'(g),'$'(h))) )). |