1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -169,25 +169,23 @@
1.4 "----------- watch order_add_mult -------------------------------";
1.5 "----------- watch order_add_mult -------------------------------";
1.6 "----- with these simple variables it works...";
1.7 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.8 -Rewrite.trace_on:=false; (*true false*)
1.9 +val ctxt = @{context};
1.10 val t = TermC.str2term "((a + d) + c) + b";
1.11 -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.12 +val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
1.13 if UnparseC.term t = "a + (b + (c + d))" then ()
1.14 else error "polyminus.sml 1 watch order_add_mult";
1.15 -Rewrite.trace_on:=false; (*true false*)
1.16
1.17 "----- the same stepwise...";
1.18 val od = ord_make_polynomial true (@{theory "Poly"});
1.19 val t = TermC.str2term "((a + d) + c) + b";
1.20 "((a + d) + c) + b";
1.21 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.22 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.23 "b + ((a + d) + c)";
1.24 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.25 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.26 "b + (c + (a + d))";
1.27 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.28 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.29 "b + (a + (c + d))";
1.30 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.31 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.32 "a + (b + (c + d))";
1.33 if UnparseC.term t = "a + (b + (c + d))" then ()
1.34 else error "polyminus.sml 2 watch order_add_mult";
1.35 @@ -195,25 +193,25 @@
1.36 "----- if parentheses are right, left_commute is (almost) sufficient...";
1.37 val t = TermC.str2term "a + (d + (c + b))";
1.38 "a + (d + (c + b))";
1.39 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.40 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.41 "a + (c + (d + b))";
1.42 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
1.43 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
1.44 "a + (c + (b + d))";
1.45 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.46 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.47 "a + (b + (c + d))";
1.48
1.49 "----- but we do not want the parentheses at right; thus: cond.rew.";
1.50 "WN0712707 complicated monomials do not yet work ...";
1.51 val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b";
1.52 -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.53 +val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
1.54 if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
1.55 else error "polyminus.sml: order_add_mult changed";
1.56
1.57 "----- here we see rew_sub going into subterm with ord.rew....";
1.58 val od = ord_make_polynomial false (@{theory "Poly"});
1.59 val t = TermC.str2term "b + a + c + d";
1.60 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.61 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.62 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.63 +val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.64 (*@@@ rew_sub gosub: t = d + (b + a + c)
1.65 @@@ rew_sub begin: t = b + a + c*)
1.66
1.67 @@ -263,53 +261,53 @@
1.68
1.69 val erls = erls_ordne_alphabetisch;
1.70 val t = TermC.str2term "b + a";
1.71 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
1.72 +val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
1.73 if UnparseC.term t = "a + b" then ()
1.74 else error "polyminus.sml: ordne_alphabetisch1 b + a";
1.75
1.76 val erls = Atools_erls;
1.77 val t = TermC.str2term "2*a + 3*a";
1.78 -val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
1.79 +val SOME (t,_) = rewrite_ ctxt od erls false @{thm real_num_collect} t; UnparseC.term t;
1.80
1.81 "======= test rewrite_, rewrite_set_";
1.82 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.83 val erls = erls_ordne_alphabetisch;
1.84 val t = TermC.str2term "b + a";
1.85 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.86 +val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.87 if UnparseC.term t = "a + b" then ()
1.88 else error "polyminus.sml: ordne_alphabetisch a + b";
1.89
1.90 val t = TermC.str2term "2*b + a";
1.91 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.92 +val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.93 if UnparseC.term t = "a + 2 * b" then ()
1.94 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
1.95
1.96 val t = TermC.str2term "a + c + b";
1.97 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.98 +val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.99 if UnparseC.term t = "a + b + c" then ()
1.100 else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.101
1.102 "======= rewrite goes into subterms";
1.103 val t = TermC.str2term "a + c + b + d ::real";
1.104 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
1.105 +val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
1.106 if UnparseC.term t = "a + b + c + d" then ()
1.107 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.108
1.109 val t = TermC.str2term "a + c + d + b";
1.110 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.111 +val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.112 if UnparseC.term t = "a + b + c + d" then ()
1.113 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.114
1.115 "======= here we see rew_sub going into subterm with cond.rew....";
1.116 val t = TermC.str2term "b + a + c + d";
1.117 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
1.118 +val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
1.119 if UnparseC.term t = "a + b + c + d" then ()
1.120 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.121
1.122 "======= compile rls for the most complicated terms";
1.123 val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.124 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
1.125 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
1.126 +val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t;
1.127 if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
1.128 then () else error "polyminus.sml: ordne_alphabetisch finished";
1.129
1.130 @@ -319,7 +317,7 @@
1.131 "----------- build fasse_zusammen --------------------------------";
1.132 "----------- build fasse_zusammen --------------------------------";
1.133 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.134 -val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
1.135 +val SOME (t,_) = rewrite_set_ ctxt false fasse_zusammen t;
1.136 if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
1.137 else error "polyminus.sml: fasse_zusammen finished";
1.138
1.139 @@ -327,12 +325,10 @@
1.140 "----------- build verschoenere ----------------------------------";
1.141 "----------- build verschoenere ----------------------------------";
1.142 val t = TermC.str2term "3 + - 2 * e + 2 * f + 2 * g";
1.143 -val SOME (t,_) = rewrite_set_ thy false verschoenere t;
1.144 +val SOME (t,_) = rewrite_set_ ctxt false verschoenere t;
1.145 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.146 else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
1.147
1.148 -(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.149 -Rewrite.trace_on:=false; (*true false*)
1.150
1.151 "----------- met simplification for_polynomials with_minus -------";
1.152 "----------- met simplification for_polynomials with_minus -------";
1.153 @@ -530,18 +526,17 @@
1.154 val erls = erls_ordne_alphabetisch;
1.155 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.156 val SOME (t',_) =
1.157 - rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
1.158 + rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus} t;
1.159 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
1.160
1.161 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.162 val NONE =
1.163 - rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
1.164 + rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus_plus} t;
1.165
1.166 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.167 val SOME (t',_) =
1.168 - rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
1.169 + rewrite_set_ ctxt false ordne_alphabetisch t;
1.170 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
1.171 -Rewrite.trace_on := false; (*true false*)
1.172
1.173
1.174 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
1.175 @@ -604,31 +599,31 @@
1.176 val thy = @{theory};
1.177 val rls = klammern_ausmultiplizieren;
1.178 val t = TermC.str2term "(3 * a + 2) * (4 * a - 1::real)";
1.179 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.180 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.181 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
1.182 val rls = discard_parentheses;
1.183 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.184 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.185 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
1.186 val rls = ordne_monome;
1.187 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.188 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.189 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
1.190 (*
1.191 val t = TermC.str2term "3 * a * 4 * a";
1.192 val rls = ordne_monome;
1.193 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.194 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.195 *)
1.196 val rls = klammern_aufloesen;
1.197 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.198 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.199 "3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2";
1.200 val rls = ordne_alphabetisch;
1.201 (*TODO: make is_monom more general, a*a=a^2, ...*)
1.202 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.203 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.204 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";
1.205 (*STOPPED.WN080104
1.206 val rls = fasse_zusammen;
1.207 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.208 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.209 val rls = verschoenere;
1.210 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.211 +val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.212 *)
1.213
1.214 (*@@@@@@@*)
1.215 @@ -690,8 +685,7 @@
1.216 Thm ("not_false", @{thm not_false})
1.217 (*"(~ False) = True"*)];
1.218 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.219 -val SOME (t', _) = rewrite_set_ thy false prls t;
1.220 -Rewrite.trace_on := false; (*true false*)
1.221 +val SOME (t', _) = rewrite_set_ ctxt false prls t;
1.222
1.223 "--- does the respective prls rewrite the whole predicate ?";
1.224 val t = TermC.str2term
1.225 @@ -700,8 +694,7 @@
1.226 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
1.227 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
1.228 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.229 -val SOME (t', _) = rewrite_set_ thy false prls t;
1.230 -Rewrite.trace_on := false; (*true false*)
1.231 +val SOME (t', _) = rewrite_set_ ctxt false prls t;
1.232 if UnparseC.term t' = "False" then ()
1.233 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
1.234