1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 26 14:16:35 2021 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 27 18:09:22 2021 +0200
1.3 @@ -3,31 +3,33 @@
1.4 (c) copyright due to lincense terms.
1.5 *)
1.6
1.7 -"--------------------------------------------------------";
1.8 -"table of contents --------------------------------------";
1.9 -"--------------------------------------------------------";
1.10 -"----------- assemble rewrite ---------------------------";
1.11 -"----------- test rewriting without Isac session --------";
1.12 -"----------- conditional rewriting without Isac session -";
1.13 -"----------- step through 'and rew_sub': ----------------";
1.14 -"----------- step through 'fun rewrite_terms_' ---------";
1.15 -"----------- rewrite_inst_ bdvs -------------------------";
1.16 -"----------- check diff 2002--2009-3 --------------------";
1.17 -"----------- compare all prepat's existing 2010 ---------";
1.18 -"----------- fun app_rev, Rrls, -------------------------";
1.19 -"----------- 2011 thms with axclasses -------------------";
1.20 +"-----------------------------------------------------------------------------------------------";
1.21 +"table of contents -----------------------------------------------------------------------------";
1.22 +"-----------------------------------------------------------------------------------------------";
1.23 +"----------- assemble rewrite ------------------------------------------------------------------";
1.24 +"----------- test rewriting without Isac's thys ------------------------------------------------";
1.25 +"----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------";
1.26 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
1.27 +"----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------";
1.28 +"----------- conditional rewriting creating an assumption---------------------------------------";
1.29 +"----------- step through 'and rew_sub': -------------------------------------------------------";
1.30 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.31 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
1.32 +"----------- check diff 2002--2009-3 -----------------------------------------------------------";
1.33 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
1.34 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.35 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
1.36 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.37 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.38 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.39 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.40 -"--------------------------------------------------------";
1.41 -"--------------------------------------------------------";
1.42 -"--------------------------------------------------------";
1.43 +"-----------------------------------------------------------------------------------------------";
1.44 +"-----------------------------------------------------------------------------------------------";
1.45 +"-----------------------------------------------------------------------------------------------";
1.46
1.47
1.48 -"----------- assemble rewrite ---------------------------";
1.49 -"----------- assemble rewrite ---------------------------";
1.50 -"----------- assemble rewrite ---------------------------";
1.51 +"----------- assemble rewrite ------------------------------------------------------------------";
1.52 +"----------- assemble rewrite ------------------------------------------------------------------";
1.53 +"----------- assemble rewrite ------------------------------------------------------------------";
1.54 "===== rewriting by thm with 'a";
1.55 (*show_types := true;*)
1.56
1.57 @@ -76,9 +78,9 @@
1.58 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
1.59 (**)
1.60
1.61 -"----------- test rewriting without Isac's thys ---------";
1.62 -"----------- test rewriting without Isac's thys ---------";
1.63 -"----------- test rewriting without Isac's thys ---------";
1.64 +"----------- test rewriting without Isac's thys ------------------------------------------------";
1.65 +"----------- test rewriting without Isac's thys ------------------------------------------------";
1.66 +"----------- test rewriting without Isac's thys ------------------------------------------------";
1.67
1.68 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
1.69 val thy = @{theory Complex_Main};
1.70 @@ -86,8 +88,7 @@
1.71 val thm = @{thm add.commute};
1.72 val tm = @{term "x + y*z::real"};
1.73
1.74 -val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.75 - handle _ => error "rewrite.sml diff.behav. in rewriting";
1.76 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.77 (*is displayed on _TOP_ of <response> buffer...*)
1.78 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.79 if r = @{term "y*z + x::real"}
1.80 @@ -96,35 +97,30 @@
1.81 "----- rewriting a subterm";
1.82 val tm = @{term "w*(x + y*z)::real"};
1.83
1.84 -val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.85 - handle _ => error "rewrite.sml diff.behav. in rew_sub";
1.86 +val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.87
1.88 "----- ordered rewriting";
1.89 fun tord (_:subst) pp = LibraryC.termless pp;
1.90 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
1.91 else error "rewrite.sml diff.behav. in ord.rewr.";
1.92
1.93 -val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
1.94 - handle _ => error "rewrite.sml diff.behav. in rewriting";
1.95 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm);
1.96 (*is displayed on _TOP_ of <response> buffer...*)
1.97 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.98
1.99 val tm = @{term "x*y + z::real"};
1.100 -val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
1.101 - handle _ => error "rewrite.sml diff.behav. in rewriting";
1.102 +val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm);
1.103
1.104
1.105 -"----------- conditional rewriting without Isac's thys --";
1.106 -"----------- conditional rewriting without Isac's thys --";
1.107 -"----------- conditional rewriting without Isac's thys --";
1.108 -
1.109 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
1.110 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
1.111 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
1.112 "===== prepr cond.rew. with Pattern.match";
1.113 val thy = @{theory Complex_Main};
1.114 val ctxt = @{context};
1.115 -val thm = @{thm nonzero_divide_mult_cancel_right};
1.116 +val thm = @{thm nonzero_divide_mult_cancel_right}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)
1.117 val rule = Thm.prop_of thm;
1.118 val tm = @{term "x / (2 * x)::real"};
1.119 -
1.120 val prem = Logic.strip_imp_prems rule;
1.121 val nps = Logic.count_prems rule;
1.122 val prems = Logic.strip_prems (nps, [], rule);
1.123 @@ -135,17 +131,26 @@
1.124 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
1.125 val rule' = Envir.subst_term mtcs rule;
1.126
1.127 -val prems' = (fst o Logic.strip_prems)
1.128 - (Logic.count_prems rule', [], rule');
1.129 -val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.130 - o Logic.strip_imp_concl) rule';
1.131 +val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');
1.132 +val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';
1.133
1.134 -"----- conditional rewriting creating an assumption";
1.135 -"----- conditional rewriting creating an assumption";
1.136 +(rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
1.137 + rule';
1.138 +
1.139 +(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
1.140 + rule' |> Logic.strip_imp_concl;
1.141 +
1.142 +(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
1.143 + rule' |> Logic.strip_imp_concl;
1.144 +
1.145 +
1.146 +"----------- conditional rewriting creating an assumption---------------------------------------";
1.147 +"----------- conditional rewriting creating an assumption---------------------------------------";
1.148 +"----------- conditional rewriting creating an assumption---------------------------------------";
1.149 val thm = @{thm nonzero_divide_mult_cancel_right};
1.150 val tm = @{term "x / (2 * x)::real"};
1.151 -val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.152 - handle _ => error "rewrite.sml diff.behav. in cond.rew.";
1.153 +
1.154 +val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.155
1.156 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
1.157 else error "rewrite.sml diff.result in cond.rew.";
1.158 @@ -156,6 +161,50 @@
1.159 "------Isabelle numerals, because erls cannot handle them yet.";
1.160
1.161
1.162 +"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
1.163 +"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
1.164 +"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
1.165 +val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
1.166 +val tm = @{term "x / (2 * x)::real"};
1.167 +val erls = eval_rls;
1.168 +
1.169 +(**)val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.170 +(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
1.171 + dest_Trueprop
1.172 + ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
1.173 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
1.174 + (thy, dummy_ord, erls, false, thm, tm);
1.175 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.176 + (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
1.177 +
1.178 +(**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.179 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
1.180 +(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
1.181 + dest_Trueprop
1.182 + ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
1.183 +"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.184 + (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
1.185 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
1.186 +(*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
1.187 +
1.188 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
1.189 +(*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");
1.190 + val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
1.191 + handle Pattern.MATCH => raise NO_REWRITE;
1.192 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
1.193 +(*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
1.194 +(*+*)r';
1.195 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.196 + val _ = trace_in2 i "eval asms" thy r';
1.197 + val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls;
1.198 + (*if*) nofalse (*then*);
1.199 + val (t'', p'') = (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'));
1.200 +(*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
1.201 +
1.202 +(*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
1.203 +(*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";
1.204 +
1.205 +
1.206 "----------- step through 'and rew_sub': ----------------";
1.207 "----------- step through 'and rew_sub': ----------------";
1.208 "----------- step through 'and rew_sub': ----------------";
1.209 @@ -191,9 +240,9 @@
1.210 o Logic.strip_imp_concl) r';
1.211 UnparseC.term t' = "1 / 2";
1.212
1.213 -"----------- step through 'fun rewrite_terms_' ---------";
1.214 -"----------- step through 'fun rewrite_terms_' ---------";
1.215 -"----------- step through 'fun rewrite_terms_' ---------";
1.216 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.217 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.218 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.219 "----- step 0: args for rewrite_terms_, local fun";
1.220 val (thy, ord, erls, equs, t) =
1.221 (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
1.222 @@ -206,28 +255,28 @@
1.223
1.224
1.225 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.226 -writeln "----------- rewrite_terms_ 1---------------------------";
1.227 +writeln "---------- rewrite_terms_ 1---------------------------";
1.228 if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.229 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.230
1.231 val equs = [TermC.str2term "M_b 0 = 0"];
1.232 val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.233 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.234 -writeln "----------- rewrite_terms_ 2---------------------------";
1.235 +writeln "---------- rewrite_terms_ 2---------------------------";
1.236 if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.237 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.238
1.239 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
1.240 val t = TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.241 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.242 -writeln "----------- rewrite_terms_ 3---------------------------";
1.243 +writeln "---------- rewrite_terms_ 3---------------------------";
1.244 if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.245 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.246
1.247
1.248 -"----------- rewrite_inst_ bdvs -------------------------";
1.249 -"----------- rewrite_inst_ bdvs -------------------------";
1.250 -"----------- rewrite_inst_ bdvs -------------------------";
1.251 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
1.252 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
1.253 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
1.254 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
1.255 val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
1.256 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.257 @@ -250,100 +299,9 @@
1.258 Rewrite.trace_on:=false;--------------------------------------------*)
1.259
1.260
1.261 -"----------- check diff 2002--2009-3 --------------------";
1.262 -"----------- check diff 2002--2009-3 --------------------";
1.263 -"----------- check diff 2002--2009-3 --------------------";
1.264 -(*----- 2002 -------------------------------------------------------------------
1.265 -# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
1.266 -q_0 * x \<up> 2 / 2)
1.267 -## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2
1.268 -/ 2)
1.269 -### try thm: real_diff_minus
1.270 -### try thm: sym_real_mult_minus1
1.271 -## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2
1.272 -/ 2)
1.273 -### try thm: rat_mult_poly_l
1.274 -### try thm: rat_mult_poly_r
1.275 -#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp
1.276 -==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) =
1.277 - 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
1.278 -##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2
1.279 -is_polyexp
1.280 -###### try calc: Poly.is'_polyexp'
1.281 -====== calc. to: False
1.282 -###### try calc: Poly.is'_polyexp'
1.283 -###### try calc: Poly.is'_polyexp'
1.284 -#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp"]
1.285 ------ 2002 NONE rewrite --------------------------------------------------------
1.286 ------ 2009 should maintain this behaviour, but: --------------------------------
1.287 -# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)
1.288 -## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)
1.289 -### try thm: real_diff_minus
1.290 -### try thm: sym_real_mult_minus1
1.291 -## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)
1.292 -### try thm: rat_mult_poly_l
1.293 -### try thm: rat_mult_poly_r
1.294 -#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp
1.295 -==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) =
1.296 - 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
1.297 -##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp
1.298 -###### try calc: Poly.is'_polyexp'
1.299 -====== calc. to: False
1.300 -###### try calc: Poly.is'_polyexp'
1.301 -###### try calc: Poly.is'_polyexp'
1.302 -#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp"] stored: ["False"]
1.303 -=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
1.304 ------ 2009 -------------------------------------------------------------------*)
1.305 -
1.306 -(*the situation as was before repair (asm without Trueprop) is outcommented*)
1.307 -val thy = @{theory "Isac_Knowledge"};
1.308 -"===== example which raised the problem =================";
1.309 -val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)"};
1.310 -"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.311 -val subs = [(@{term "bdv"}, @{term "x"})];
1.312 -val rls = norm_Rational_noadd_fractions;
1.313 -val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
1.314 -if UnparseC.term t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x \<up> 2 / 2)" andalso
1.315 - UnparseC.terms asms = "[]" then {}
1.316 -else error "this was NONE with Isabelle2013-2 ?!?"
1.317 -"----- rewrite_ rat_mult_poly_r--------------------------";
1.318 -val thm = @{thm rat_mult_poly_r};
1.319 - "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.320 -val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.321 - [Eval ("Poly.is'_polyexp", eval_is_polyexp "")];
1.322 -val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
1.323 -(*t' = t''; (*false because of further rewrites in t'*)*)
1.324 -"----- rew_sub --------------------------------";
1.325 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
1.326 -(*t'' = t'''; (*true*)*)
1.327 -"----- rewrite_set_ erls --------------------------------";
1.328 -val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)"};
1.329 -val NONE = rewrite_set_ thy true erls cond;
1.330 -(* \<up> ^^ goes with '====== calc. to: False' above from beginning*)
1.331 -
1.332 -writeln "===== maximally simplified example =====================";
1.333 -val t = @{term "a / b * (x / x \<up> 2)"};
1.334 - "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.335 -writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.336 -val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
1.337 -UnparseC.term t' = "a * x / (b * x \<up> 2)"; (*rew. by thm outside test case*)
1.338 -(*checked visually: Rewrite.trace_on looks like above for 2009*)
1.339 -
1.340 -writeln "----- rewrite_ rat_mult_poly_r--------------------------";
1.341 -val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
1.342 -(*t' = t''; (*false because of further rewrites in t'*)*)
1.343 -writeln "----- rew_sub --------------------------------";
1.344 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
1.345 -(*t'' = t'''; (*true*)*)
1.346 -writeln "----- rewrite_set_ erls --------------------------------";
1.347 -val cond = @{term "(x / x \<up> 2)"};
1.348 -val NONE = rewrite_set_ thy true erls cond;
1.349 -(* \<up> ^^ goes with '====== calc. to: False' above from beginning*)
1.350 -
1.351 -
1.352 -"----------- compare all prepat's existing 2010 ---------";
1.353 -"----------- compare all prepat's existing 2010 ---------";
1.354 -"----------- compare all prepat's existing 2010 ---------";
1.355 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
1.356 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
1.357 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
1.358 val thy = @{theory "Isac_Knowledge"};
1.359 val t = @{term "a + b * x = (0 ::real)"};
1.360 val pat = TermC.parse_patt thy "?l = (?r ::real)";
1.361 @@ -406,9 +364,9 @@
1.362 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.363
1.364
1.365 -"----------- fun app_rev, Rrls, -------------------------";
1.366 -"----------- fun app_rev, Rrls, -------------------------";
1.367 -"----------- fun app_rev, Rrls, -------------------------";
1.368 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.369 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.370 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
1.371 val t = TermC.str2term "x \<up> 2 * x";
1.372
1.373 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.374 @@ -497,9 +455,9 @@
1.375 ([], true) => ()
1.376 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
1.377
1.378 -"----------- 2011 thms with axclasses -------------------";
1.379 -"----------- 2011 thms with axclasses -------------------";
1.380 -"----------- 2011 thms with axclasses -------------------";
1.381 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
1.382 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
1.383 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
1.384 val thm = ThmC.numerals_to_Free @{thm div_by_1};
1.385 val prop = Thm.prop_of thm;
1.386 TermC.atomty prop; (*Type 'a*)
1.387 @@ -689,10 +647,10 @@
1.388 (thy, 1, [], rew_ord, erls, bool, thm, term);
1.389 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.390 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
1.391 - val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.392 + val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
1.393 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
1.394 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.395 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.396 + val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
1.397 ;
1.398 if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
1.399 else error "ARGS FOR Pattern.match CHANGED";
1.400 @@ -700,17 +658,23 @@
1.401 if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
1.402 else error "Pattern.match CHANGED";
1.403
1.404 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.405 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.406 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
1.407 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
1.408 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
1.409 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
1.410 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
1.411 val thy = @{theory};
1.412 val rls = norm_equation;
1.413 val term = TermC.str2term "x + 1 = 2";
1.414
1.415 -val SOME (t, asm) = rewrite_set_ thy false rls term;
1.416 +(**)val SOME (t, asm) = rewrite_set_ thy false rls term;
1.417 +(** )##### try thm: "root_ge0"
1.418 +exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
1.419 + dest_eq
1.420 + 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
1.421 if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
1.422
1.423 -"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
1.424 -"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
1.425 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
1.426 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
1.427 + (thy, 1, bool, []: (term * term) list, rls, term);
1.428 +(*deleted after error detection*)
1.429