1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -158,7 +158,7 @@
1.4 if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
1.5 then () else error "rewrite.sml diff.asm in cond.rew.";
1.6 "----- conditional rewriting immediately: can only be done with ";
1.7 -"------Isabelle numerals, because erls cannot handle them yet.";
1.8 +"------Isabelle numerals, because asm_rls cannot handle them yet.";
1.9
1.10
1.11 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
1.12 @@ -166,16 +166,16 @@
1.13 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
1.14 val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
1.15 val tm = @{term "x / (2 * x)::real"};
1.16 -val erls = eval_rls;
1.17 +val asm_rls = eval_rls;
1.18
1.19 (**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
1.20 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
1.21 dest_Trueprop
1.22 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
1.23 -"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
1.24 - (thy, Rewrite_Ord.function_empty, erls, false, thm, tm);
1.25 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, asm_rls, bool, thm, term) =
1.26 + (thy, Rewrite_Ord.function_empty, asm_rls, false, thm, tm);
1.27 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.28 - (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
1.29 + (thy, 1, []: Subst.T, rew_ord, asm_rls, bool, thm, term);
1.30
1.31 (**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.32 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
1.33 @@ -244,13 +244,13 @@
1.34 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.35 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
1.36 "----- step 0: args for rewrite_terms_, local fun";
1.37 -val (thy, ord, erls, equs, t) =
1.38 +val (thy, ord, asm_rls, equs, t) =
1.39 (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.parse_test @{context} "x = 0"],
1.40 TermC.parse_test @{context} "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
1.41 "----- step 1: args for rew_";
1.42 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
1.43 "----- step 2: rew_sub";
1.44 -rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
1.45 +rew_sub ctxt 1 [] ord asm_rls false [] (HOLogic.Trueprop $ r) t;
1.46 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
1.47
1.48
1.49 @@ -321,15 +321,15 @@
1.50 val pat = TermC.parse_patt thy "?r / ?s ::real";
1.51 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
1.52 val prepat = [(pres, pat)];
1.53 -val erls = rational_erls;
1.54 -(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.55 +val asm_rls = rational_erls;
1.56 +(* asm_rls got from Rrls {asm_rls, prepat, program = Rfuns {normal_form, ...}, ...} *)
1.57
1.58 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.59 val asms = map (Envir.subst_term subst) pres;
1.60 if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
1.61 then () else error "rewrite.sml: prepat cancel subst";
1.62
1.63 -if ([], true) = eval__true ctxt 0 asms [] erls
1.64 +if ([], true) = eval__true ctxt 0 asms [] asm_rls
1.65 then () else error "rewrite.sml: prepat cancel eval__true";
1.66
1.67 "===== Rational.thy: add_fractions_p ===";
1.68 @@ -339,11 +339,11 @@
1.69 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
1.70 val pres = [@{term True}];
1.71 val prepat = [(pres, pat)];
1.72 -val erls = rational_erls;
1.73 -(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.74 +val asm_rls = rational_erls;
1.75 +(* asm_rls got from Rrls {asm_rls, prepat, program = Rfuns {normal_form, ...}, ...} *)
1.76
1.77 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.78 -if ([], true) = eval__true ctxt 0 (map (Envir.subst_term subst) pres) [] erls
1.79 +if ([], true) = eval__true ctxt 0 (map (Envir.subst_term subst) pres) [] asm_rls
1.80 then () else error "rewrite.sml: prepat add_fractions_p";
1.81
1.82 "===== Poly.thy: order_mult_ ===";
1.83 @@ -353,7 +353,7 @@
1.84 val pat = TermC.parse_patt thy "?p :: real"
1.85 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
1.86 val prepat = [(pres, pat)];
1.87 -val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.88 +val asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.89 [Eval ("Poly.is_multUnordered",
1.90 eval_is_multUnordered "")];
1.91
1.92 @@ -362,7 +362,7 @@
1.93 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
1.94 then () else error "rewrite.sml: prepat order_mult_ subst";
1.95
1.96 -if ([], true) = eval__true ctxt 0 asms [] erls
1.97 +if ([], true) = eval__true ctxt 0 asms [] asm_rls
1.98 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.99
1.100
1.101 @@ -408,15 +408,15 @@
1.102 val (t', asm, rew) = app_rev ctxt (i+1) rrls t;
1.103 "----- app_rev ---";
1.104 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.105 - fun chk_prepat thy erls [] t = true
1.106 - | chk_prepat thy erls prepat t =
1.107 + fun chk_prepat thy asm_rls [] t = true
1.108 + | chk_prepat thy asm_rls prepat t =
1.109 let fun chk (pres, pat) =
1.110 (let val subst: Type.tyenv * Envir.tenv =
1.111 Pattern.match thy (pat, t)
1.112 (Vartab.empty, Vartab.empty)
1.113 in snd (eval__true ctxt (i+1)
1.114 (map (Envir.subst_term subst) pres)
1.115 - [] erls)
1.116 + [] asm_rls)
1.117 end)
1.118 handle Pattern.MATCH => false
1.119 fun scan_ f [] = false (*scan_ NEVER called by []*)
1.120 @@ -425,24 +425,24 @@
1.121 in scan_ chk prepat end;
1.122
1.123 (*.apply the normal_form of a rev-set.*)
1.124 - fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.125 - if chk_prepat thy erls prepat t
1.126 + fun app_rev' thy (Rrls{asm_rls,prepat,program=Rfuns{normal_form,...},...}) t =
1.127 + if chk_prepat thy asm_rls prepat t
1.128 then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
1.129 normal_form t)
1.130 else NONE;
1.131 (*fixme val NONE = app_rev' thy rrls t;*)
1.132 "----- app_rev' ---";
1.133 -val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
1.134 -(*fixme false*) chk_prepat thy erls prepat t;
1.135 +val (thy, Rrls{asm_rls,prepat,program=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
1.136 +(*fixme false*) chk_prepat thy asm_rls prepat t;
1.137 "----- chk_prepat ---";
1.138 -val (thy, erls, prepat, t) = (thy, erls, prepat, t);
1.139 +val (thy, asm_rls, prepat, t) = (thy, asm_rls, prepat, t);
1.140 fun chk (pres, pat) =
1.141 (let val subst: Type.tyenv * Envir.tenv =
1.142 Pattern.match thy (pat, t)
1.143 (Vartab.empty, Vartab.empty)
1.144 in snd (eval__true ctxt (i+1)
1.145 (map (Envir.subst_term subst) pres)
1.146 - [] erls)
1.147 + [] asm_rls)
1.148 end)
1.149 handle Pattern.MATCH => false;
1.150 fun scan_ _ [] = false (*scan_ NEVER called by []*)
1.151 @@ -466,7 +466,7 @@
1.152 else error "rewrite.sml: diff. is_multUnordered, asms";
1.153 val (thy, i, asms, bdv, rls) =
1.154 (thy, (i+1), [TermC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered"],
1.155 - [] : Subst.T, erls);
1.156 + [] : Subst.T, asm_rls);
1.157 case eval__true ctxt i asms bdv rls of
1.158 ([], true) => ()
1.159 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
1.160 @@ -510,7 +510,7 @@
1.161 Rule.Thm (thmid, thm) =>
1.162 (trace1 i (" try thm: " ^ thmid);
1.163 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.164 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
1.165 + ((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm ct of
1.166 NONE => rew_once ruls asm ct apno thms
1.167 | SOME (ct', asm') =>
1.168 (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
1.169 @@ -524,7 +524,7 @@
1.170 | SOME (_, thm') =>
1.171 let
1.172 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.173 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.174 + ((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.175 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.176 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.177 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
1.178 @@ -538,7 +538,7 @@
1.179 | SOME (_, thm') =>
1.180 let
1.181 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.182 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.183 + ((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.184 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.185 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
1.186 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
1.187 @@ -558,10 +558,10 @@
1.188
1.189 val SOME (ct', asm') = (*case*)
1.190 rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.191 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
1.192 + ((#asm_rls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
1.193 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
1.194 = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
1.195 - ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
1.196 + ((#asm_rls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
1.197
1.198 val (t', asms, _ (*lrd*), rew) =
1.199 rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.200 @@ -657,10 +657,10 @@
1.201 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.202 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.203 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.204 -"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
1.205 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, asm_rls, bool, thm, term) =
1.206 (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
1.207 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.208 - (thy, 1, [], rew_ord, erls, bool, thm, term);
1.209 + (thy, 1, [], rew_ord, asm_rls, bool, thm, term);
1.210 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.211 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
1.212 val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r