1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -88,7 +88,7 @@
1.4 val thm = @{thm add.commute};
1.5 val tm = @{term "x + y*z::real"};
1.6
1.7 -val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.8 +val SOME (r,_) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
1.9 (*is displayed on _TOP_ of <response> buffer...*)
1.10 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.11 if r = @{term "y*z + x::real"}
1.12 @@ -97,19 +97,19 @@
1.13 "----- rewriting a subterm";
1.14 val tm = @{term "w*(x + y*z)::real"};
1.15
1.16 -val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.17 +val SOME (r, _) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
1.18
1.19 "----- ordered rewriting";
1.20 fun tord (_:subst) pp = LibraryC.termless pp;
1.21 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
1.22 else error "rewrite.sml diff.behav. in ord.rewr.";
1.23
1.24 -val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm);
1.25 +val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm);
1.26 (*is displayed on _TOP_ of <response> buffer...*)
1.27 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.28
1.29 val tm = @{term "x*y + z::real"};
1.30 -val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm);
1.31 +val SOME (r, _) = (rewrite_ ctxt tord Rule_Set.empty false thm tm);
1.32
1.33
1.34 "----------- conditional rewriting without Isac's thys -----------------------------------------";
1.35 @@ -150,7 +150,7 @@
1.36 val thm = @{thm nonzero_divide_mult_cancel_right};
1.37 val tm = @{term "x / (2 * x)::real"};
1.38
1.39 -val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.40 +val SOME (rew, asm) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
1.41
1.42 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
1.43 else error "rewrite.sml diff.result in cond.rew.";
1.44 @@ -168,7 +168,7 @@
1.45 val tm = @{term "x / (2 * x)::real"};
1.46 val erls = eval_rls;
1.47
1.48 -(**)val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
1.49 +(**)val SOME (rew, asm) = rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm;
1.50 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
1.51 dest_Trueprop
1.52 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
1.53 @@ -177,7 +177,7 @@
1.54 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.55 (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
1.56
1.57 -(**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.58 +(**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.59 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
1.60 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
1.61 dest_Trueprop
1.62 @@ -195,10 +195,10 @@
1.63 (*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
1.64 (*+*)r';
1.65 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.66 - val _ = trace_in2 i "eval asms" thy r';
1.67 - val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls;
1.68 + val _ = trace_in2 ctxt i "eval asms" r';
1.69 + val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls;
1.70 (*if*) nofalse (*then*);
1.71 - val (t'', p'') = (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'));
1.72 + val (t'', p'') = (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'));
1.73 (*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
1.74
1.75 (*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
1.76 @@ -210,7 +210,7 @@
1.77 "----------- step through 'and rew_sub': ----------------";
1.78 (*and make asms without Trueprop, beginning with the result:*)
1.79 val tm = @{term "x / (2 * x)::real"};
1.80 -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
1.81 +val (t', asm, _, _) = rew_sub ctxt 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
1.82 (*show_types := false;*)
1.83 "----- evaluate arguments";
1.84 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.85 @@ -250,25 +250,25 @@
1.86 "----- step 1: args for rew_";
1.87 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
1.88 "----- step 2: rew_sub";
1.89 -rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
1.90 +rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
1.91 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
1.92
1.93
1.94 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.95 +val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
1.96 writeln "---------- rewrite_terms_ 1---------------------------";
1.97 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.98 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.99
1.100 val equs = [TermC.str2term "M_b 0 = 0"];
1.101 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.102 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.103 +val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
1.104 writeln "---------- rewrite_terms_ 2---------------------------";
1.105 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.106 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.107
1.108 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
1.109 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.110 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.111 +val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
1.112 writeln "---------- rewrite_terms_ 3---------------------------";
1.113 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.114 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.115 @@ -329,7 +329,7 @@
1.116 if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
1.117 then () else error "rewrite.sml: prepat cancel subst";
1.118
1.119 -if ([], true) = eval__true thy 0 asms [] erls
1.120 +if ([], true) = eval__true ctxt 0 asms [] erls
1.121 then () else error "rewrite.sml: prepat cancel eval__true";
1.122
1.123 "===== Rational.thy: add_fractions_p ===";
1.124 @@ -343,7 +343,7 @@
1.125 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.126
1.127 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.128 -if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
1.129 +if ([], true) = eval__true ctxt 0 (map (Envir.subst_term subst) pres) [] erls
1.130 then () else error "rewrite.sml: prepat add_fractions_p";
1.131
1.132 "===== Poly.thy: order_mult_ ===";
1.133 @@ -362,7 +362,7 @@
1.134 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
1.135 then () else error "rewrite.sml: prepat order_mult_ subst";
1.136
1.137 -if ([], true) = eval__true thy 0 asms [] erls
1.138 +if ([], true) = eval__true ctxt 0 asms [] erls
1.139 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.140
1.141
1.142 @@ -396,16 +396,16 @@
1.143 Const (\<^const_name>\<open>True\<close>, _))) => ()
1.144 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
1.145
1.146 -tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
1.147 -val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.148 -tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
1.149 +tracing "----- begin rewrite x \<up> 2 * x ---";
1.150 +val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
1.151 +tracing "----- end rewrite x \<up> 2 * x ---";
1.152 if UnparseC.term t' = "x * x \<up> 2" then ()
1.153 else error "rewrite.sml Poly.is_multUnordered doesn't work";
1.154
1.155 (* for achieving the previous result, the following code was taken apart *)
1.156 "----- rewrite__set_ ---";
1.157 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
1.158 - val (t', asm, rew) = app_rev thy (i+1) rrls t;
1.159 + val (t', asm, rew) = app_rev ctxt (i+1) rrls t;
1.160 "----- app_rev ---";
1.161 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.162 fun chk_prepat thy erls [] t = true
1.163 @@ -414,7 +414,7 @@
1.164 (let val subst: Type.tyenv * Envir.tenv =
1.165 Pattern.match thy (pat, t)
1.166 (Vartab.empty, Vartab.empty)
1.167 - in snd (eval__true thy (i+1)
1.168 + in snd (eval__true ctxt (i+1)
1.169 (map (Envir.subst_term subst) pres)
1.170 [] erls)
1.171 end)
1.172 @@ -440,7 +440,7 @@
1.173 (let val subst: Type.tyenv * Envir.tenv =
1.174 Pattern.match thy (pat, t)
1.175 (Vartab.empty, Vartab.empty)
1.176 - in snd (eval__true thy (i+1)
1.177 + in snd (eval__true ctxt (i+1)
1.178 (map (Envir.subst_term subst) pres)
1.179 [] erls)
1.180 end)
1.181 @@ -467,7 +467,7 @@
1.182 val (thy, i, asms, bdv, rls) =
1.183 (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
1.184 [] : Subst.T, erls);
1.185 -case eval__true thy i asms bdv rls of
1.186 +case eval__true ctxt i asms bdv rls of
1.187 ([], true) => ()
1.188 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
1.189
1.190 @@ -481,7 +481,7 @@
1.191
1.192 val (thy, ro, er, inst) =
1.193 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
1.194 -val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
1.195 +val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
1.196
1.197 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.198 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.199 @@ -492,9 +492,9 @@
1.200 val rls = assoc_rls "RatEq_eliminate"
1.201
1.202 val SOME (t''''', asm''''') =
1.203 - rewrite_set_ thy true rls t;
1.204 + rewrite_set_ ctxt true rls t;
1.205 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
1.206 - rewrite__set_ thy 1 bool [] rls term;
1.207 + rewrite__set_ ctxt 1 bool [] rls term;
1.208 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
1.209 = (thy, 1, bool, []:Subst.T, rls, term);
1.210
1.211 @@ -682,7 +682,7 @@
1.212 val rls = norm_equation;
1.213 val term = TermC.str2term "x + 1 = 2";
1.214
1.215 -(**)val SOME (t, asm) = rewrite_set_ thy false rls term;
1.216 +(**)val SOME (t, asm) = rewrite_set_ ctxt false rls term;
1.217 (** )##### try thm: "root_ge0"
1.218 exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
1.219 dest_eq