1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Sun Apr 25 12:49:37 2021 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 26 14:16:35 2021 +0200
1.3 @@ -58,7 +58,7 @@
1.4 val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.5 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
1.6 in if rew then SOME (t', distinct op = asms) else NONE end
1.7 - (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
1.8 + (* one rewrite (possibly conditional, ordered) EXOR exn Pattern.MATCH EXOR go into subterms *)
1.9 and rew_sub thy i bdv tless rls put_asm lrd r t =
1.10 (let
1.11 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
2.1 --- a/test/Tools/isac/Test_Some.thy Sun Apr 25 12:49:37 2021 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Mon Apr 26 14:16:35 2021 +0200
2.3 @@ -98,10 +98,433 @@
2.4 \<close> ML \<open>
2.5 \<close>
2.6
2.7 -section \<open>===================================================================================\<close>
2.8 +section \<open>============ prep.eliminate "handle _ => ..." from Rewrite.rewrite ================\<close>
2.9 ML \<open>
2.10 \<close> ML \<open>
2.11 \<close> ML \<open>
2.12 +exception NO_REWRITE;
2.13 +exception STOP_REW_SUB; (*WN050820 quick and dirty*)
2.14 +
2.15 +val trace_on = Unsynchronized.ref false;
2.16 +(* depth of recursion in traces of the rewriter, if trace_on:=true *)
2.17 +val depth = Unsynchronized.ref 99999;
2.18 +(* no of rewrites exceeding this int -> NO rewrite *)
2.19 +val lim_deriv = Unsynchronized.ref 100;
2.20 +
2.21 +fun trace i str =
2.22 + if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
2.23 +fun trace_eq1 i str rrls thy t =
2.24 + trace i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
2.25 +fun trace_eq2 i str thy t t' =
2.26 + trace i (" " ^ str ^ ": \"" ^
2.27 + UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
2.28 +(*/----- sig*)
2.29 +trace_eq1 : int -> string -> Rule_Def.rule_set -> theory -> term -> unit;
2.30 +trace_eq2 : int -> string -> theory -> term -> term -> unit;
2.31 +(*\----- sig*)
2.32 +
2.33 +fun trace1 i str =
2.34 + if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
2.35 +fun trace_in1 i str thmid =
2.36 + trace1 i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
2.37 +fun trace_in2 i str thy t =
2.38 + trace1 i (" " ^ str ^ ": \"" ^ UnparseC.term_in_thy thy t ^ "\"");
2.39 +fun trace_in3 i str thy pairopt =
2.40 + trace1 i (" " ^ str ^ ": " ^ UnparseC.term_in_thy thy ((fst o the) pairopt));
2.41 +fun trace_in4 i str thy ts ts' =
2.42 + if ! trace_on andalso i < ! depth andalso ts <> []
2.43 + then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy ts ^
2.44 + " stored: " ^ UnparseC.terms_in_thy thy ts')
2.45 + else ();
2.46 +fun trace_in5 i str thy p' =
2.47 + if ! trace_on andalso i < ! depth
2.48 + then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
2.49 + else();
2.50 +(*/----- sig*)
2.51 +trace_in1 : int -> string -> string -> unit;
2.52 +trace_in2 : int -> string -> theory -> term -> unit;
2.53 +trace_in3 : int -> string -> theory -> (term * 'a) option -> unit;
2.54 +trace_in4 : int -> string -> theory -> term list -> term list -> unit;
2.55 +trace_in5 : int -> string -> theory -> term list -> unit;
2.56 +(*\----- sig*)
2.57 +
2.58 +\<close> ML \<open>
2.59 +(*=== unify: trace trac1 trace_eq1 trace_eq2 trace_in1 trace_in2 trace_in3 trace_in4 trace_in5 *)
2.60 +fun rewrite__ thy i bdv tless rls put_asm thm ct =
2.61 + let
2.62 + val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
2.63 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
2.64 + in if rew then SOME (t', distinct op = asms) else NONE end
2.65 + (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
2.66 +and rew_sub thy i bdv tless rls put_asm lrd r t =
2.67 + (let
2.68 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
2.69 + (*?alternative Unify.matchers:
2.70 + http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
2.71 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
2.72 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
2.73 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
2.74 + val _ = trace_in2 i "eval asms" thy r';
2.75 + val (t'', p'') = (*conditional rewriting*)
2.76 + let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
2.77 + in
2.78 + if nofalse
2.79 + then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
2.80 + else (trace_in5 i "asms false" thy p'; raise STOP_REW_SUB) (* don't go into subtm.of cond*)
2.81 + end
2.82 + in
2.83 + if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
2.84 + then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
2.85 + else (t'', p'', [], true)
2.86 + end
2.87 + ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
2.88 + (case t of
2.89 + Const(s,T) => (Const(s,T),[],lrd,false)
2.90 + | Free(s,T) => (Free(s,T),[],lrd,false)
2.91 + | Var(n,T) => (Var(n,T),[],lrd,false)
2.92 + | Bound i => (Bound i,[],lrd,false)
2.93 + | Abs(s,T,body) =>
2.94 + let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
2.95 + in (Abs(s, T, t'), asms, [], rew) end
2.96 + | t1 $ t2 =>
2.97 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
2.98 + in
2.99 + if rew2 then (t1 $ t2', asm2, lrd, true)
2.100 + else
2.101 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
2.102 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
2.103 + end)
2.104 +and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false*)
2.105 + if asms = [@{term True}] orelse asms = [] then ([], true)
2.106 + else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
2.107 + if asms = [@{term False}] then ([], false)
2.108 + else
2.109 + let
2.110 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
2.111 + | chk indets (a :: asms) =
2.112 + (case rewrite__set_ thy (i + 1) false bdv rls a of
2.113 + NONE => (chk (indets @ [a]) asms)
2.114 + | SOME (t, a') =>
2.115 + if t = @{term True} then (chk (indets @ a') asms)
2.116 + else if t = @{term False} then ([], false)
2.117 + (*asm false .. thm not applied ^^^; continue until False vvv*)
2.118 + else chk (indets @ [t] @ a') asms);
2.119 + in chk [] asms end
2.120 +and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set*)
2.121 + raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
2.122 + | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
2.123 + let
2.124 + val _= trace_eq1 i "rls" rrls thy t;
2.125 + val (t', asm, rew) = app_rev thy (i + 1) rrls t
2.126 + in if rew then SOME (t', distinct op = asm) else NONE end
2.127 + | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
2.128 + let
2.129 + (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
2.130 + datatype switch = Appl | Noap;
2.131 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
2.132 + | rew_once ruls asm ct Appl [] =
2.133 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
2.134 + | Rule_Set.Sequence _ => (ct, asm)
2.135 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
2.136 + | rew_once ruls asm ct apno (rul :: thms) =
2.137 + case rul of
2.138 + Rule.Thm (thmid, thm) =>
2.139 + (trace_in1 i "try thm" thmid;
2.140 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
2.141 + ((#erls o Rule_Set.rep) rls) put_asm thm ct of
2.142 + NONE => rew_once ruls asm ct apno thms
2.143 + | SOME (ct', asm') =>
2.144 + (trace_in2 i "rewrites to" thy ct';
2.145 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
2.146 + (* once again try the same rule, e.g. associativity against "()"*)
2.147 + | Rule.Eval (cc as (op_, _)) =>
2.148 + let val _= trace_in1 i "try calc" op_;
2.149 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
2.150 + in case Eval.adhoc_thm thy cc ct of
2.151 + NONE => rew_once ruls asm ct apno thms
2.152 + | SOME (_, thm') =>
2.153 + let
2.154 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
2.155 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
2.156 + val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
2.157 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
2.158 + val _ = trace_in3 i "calc. to" thy pairopt;
2.159 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
2.160 + end
2.161 + | Rule.Cal1 (cc as (op_, _)) =>
2.162 + let val _= trace_in1 i "try cal1" op_;
2.163 + val ct = TermC.uminus_to_string ct
2.164 + in case Eval.adhoc_thm1_ thy cc ct of
2.165 + NONE => (ct, asm)
2.166 + | SOME (_, thm') =>
2.167 + let
2.168 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
2.169 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
2.170 + val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
2.171 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
2.172 + val _ = trace_in3 i "cal1. to" thy pairopt;
2.173 + in the pairopt end
2.174 + end
2.175 + | Rule.Rls_ rls' =>
2.176 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
2.177 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
2.178 + | NONE => rew_once ruls asm ct apno thms)
2.179 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
2.180 + val ruls = (#rules o Rule_Set.rep) rls;
2.181 + val _ = trace_eq1 i "rls" rls thy ct
2.182 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
2.183 + in if ct = ct' then NONE else SOME (ct', distinct op = asm') end
2.184 +(*-------------------------------------------------------------*)
2.185 +and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
2.186 + let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
2.187 + fun chk_prepat _ _ [] _ = true
2.188 + | chk_prepat thy erls prepat t =
2.189 + let
2.190 + fun chk (pres, pat) =
2.191 + (let
2.192 + val subst: Type.tyenv * Envir.tenv =
2.193 + Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
2.194 + in
2.195 + snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
2.196 + end) handle _ (*TODO Pattern.MATCH*) => false
2.197 + fun scan_ _ [] = false
2.198 + | scan_ f (pp :: pps) =
2.199 + if f pp then true else scan_ f pps;
2.200 + in scan_ chk prepat end;
2.201 + (* apply the normal_form of a rev-set *)
2.202 + fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
2.203 + if chk_prepat thy erls prepat t then normal_form t else NONE
2.204 + | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
2.205 + val opt = app_rev' thy rrls t
2.206 + in
2.207 + case opt of
2.208 + SOME (t', asm) => (t', asm, true)
2.209 + | NONE => app_sub thy i rrls t
2.210 + end
2.211 +and app_sub thy i rrls t = (* apply an Rrls to subterms*)
2.212 + case t of
2.213 + Const (s, T) => (Const(s, T), [], false)
2.214 + | Free (s, T) => (Free(s, T), [], false)
2.215 + | Var (n, T) => (Var(n, T), [], false)
2.216 + | Bound i => (Bound i, [], false)
2.217 + | Abs (s, T, body) =>
2.218 + let val (t', asm, rew) = app_rev thy i rrls body
2.219 + in (Abs(s, T, t'), asm, rew) end
2.220 + | t1 $ t2 =>
2.221 + let val (t2', asm2, rew2) = app_rev thy i rrls t2
2.222 + in
2.223 + if rew2 then (t1 $ t2', asm2, true)
2.224 + else
2.225 + let val (t1', asm1, rew1) = app_rev thy i rrls t1
2.226 + in if rew1 then (t1' $ t2, asm1, true)
2.227 + else (t1 $ t2, [], false)
2.228 + end
2.229 + end;
2.230 +
2.231 +\<close> ML \<open>
2.232 +\<close>
2.233 +
2.234 +section \<open>========== unify and shorten trace ================================================\<close>
2.235 +ML \<open>
2.236 +(*=== unify: trace trac1 trace_eq1 trace_eq2 trace_in1 trace_in2 trace_in3 trace_in4 trace_in5 *)
2.237 +trace_on := true;
2.238 +\<close> ML \<open> (*original, shift new above ! *)
2.239 +fun trace i str = (*<-------------------------------------------------------------------------*)
2.240 + if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ();
2.241 +trace : int -> string -> unit;
2.242 +\<close> ML \<open>
2.243 +val (str, thy, i, rrls, t) = ("xxxxx", @{theory}, 2, Rule_Set.empty, @{term "x + y*z::real"});
2.244 +trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t);
2.245 +(*## rls: empty on: x + y * z *)
2.246 +\<close> ML \<open> (*----- new ----- *)
2.247 +trace_eq1 i "rls" rrls thy t;
2.248 +(*## rls: empty on: x + y * z *)
2.249 +\<close> ML \<open>
2.250 +fun trace1 i str = (*<------------------------------------------------------------------------*)
2.251 + if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
2.252 +\<close> ML \<open>
2.253 +val (str, i, thmid) = ("try thm", 2, "commute");
2.254 +trace1 i (" try thm: \"" ^ thmid ^ "\"");
2.255 +(*### try thm: "commute" *)
2.256 +\<close> ML \<open> (*----- new ----- *)
2.257 +trace_in1 i str thmid;
2.258 +(*### try thm: "commute" *)
2.259 +\<close> ML \<open>
2.260 +\<close> ML \<open>
2.261 +val (str, thy, i, ct') = ("rewrites to", @{theory}, 2, @{term "x + y*z::real"});
2.262 +trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
2.263 +(*### rewrites to: "x + y * z" *)
2.264 +\<close> ML \<open> (*----- new ----- *)
2.265 +trace_in2 i str thy ct';
2.266 +(*### rewrites to: "x + y * z" *)
2.267 +\<close> ML \<open>
2.268 +\<close> ML \<open>
2.269 +val (str, i, op_) = ("try thm", 2, "+");
2.270 +trace1 i (" try calc: \"" ^ op_ ^ "\"");
2.271 +(*### try calc: "+" *)
2.272 +\<close> ML \<open>
2.273 +trace_in1 i str op_;
2.274 +(*### try thm: "+" *)
2.275 +\<close> ML \<open>
2.276 +\<close> ML \<open>
2.277 +val (str, thy, i, pairopt) = ("calc. to", @{theory}, 2, SOME (@{term "x + y*z::real"}, []));
2.278 +trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt));
2.279 +(*### calc. to: x + y * z *)
2.280 +\<close> ML \<open> (*----- new ----- *)
2.281 +trace_in3 i str thy pairopt;
2.282 +(*### calc. to: x + y * z *)
2.283 +\<close> ML \<open>
2.284 +\<close> ML \<open>
2.285 +val (str, thy, i, r') = ("eval asms", @{theory}, 2, @{term "x + y*z::real"});
2.286 +tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r');
2.287 +(*### eval asms: x + y * z *)
2.288 +\<close> ML \<open>
2.289 +trace_in2 i str thy r';
2.290 +(*### eval asms: "x + y * z" *)
2.291 +\<close> ML \<open>
2.292 +\<close> ML \<open>
2.293 +val (str, thy, i, t, t') = ("not >", @{theory}, 2, @{term "y*z::real"}, @{term "x + y*z::real"});
2.294 +tracing (idt"#"i ^ " not >: \"" ^
2.295 + UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
2.296 +(*## not >: "y * z" > "x + y * z" *)
2.297 +\<close> ML \<open> (*----- new ----- *)
2.298 +trace_eq2 i str thy t t';
2.299 +(*## not >: "y * z" > "x + y * z" *)
2.300 +\<close> ML \<open>
2.301 +\<close> ML \<open>
2.302 +val (str, thy, i, p', simpl_p') = ("asms accepted", @{theory}, 2, [@{term "x + y*z::real"}], [@{term "y*z::real"}]);
2.303 +if ! trace_on andalso i < ! depth andalso p' <> []
2.304 +then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
2.305 + " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
2.306 +else();
2.307 +(*### asms accepted: [x + y * z] stored: [y * z] *)
2.308 +\<close> ML \<open> (*----- new ----- *)
2.309 +trace_in4 i str thy p' simpl_p';
2.310 +(*### asms accepted: [x + y * z] stored: [y * z] *)
2.311 +\<close> ML \<open>
2.312 +\<close> ML \<open>
2.313 +val (str, thy, i, p') = ("asms false", @{theory}, 2, [@{term "x + y*z::real"}]);
2.314 +if ! trace_on andalso i < ! depth
2.315 +then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
2.316 +else();
2.317 +(*### asms false: [x + y * z] *)
2.318 +\<close> ML \<open> (*----- new ----- *)
2.319 +trace_in5 i str thy p';
2.320 +(*### asms false: [x + y * z] *)
2.321 +\<close> ML \<open>
2.322 +\<close> ML \<open>
2.323 +val (str, i, thmid) = ("try thm", 2, "commute");
2.324 +trace1 i (" try thm: \"" ^ thmid ^ "\"");
2.325 +(*### try thm: "commute" *)
2.326 +trace_in1 i str thmid
2.327 +(*### try thm: "commute" *)
2.328 +\<close> ML \<open>
2.329 +\<close> ML \<open>
2.330 +val (i, str, thy, ct') = (2, "rewrites to", @{theory}, @{term "x + y*z::real"});
2.331 +trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
2.332 +(*### rewrites to: "x + y * z" *)
2.333 +trace_in2 i str thy ct';
2.334 +(*### rewrites to: "x + y * z" *)
2.335 +\<close> ML \<open>
2.336 +\<close> ML \<open>
2.337 +\<close>
2.338 +
2.339 +section \<open>==========--- test rewriting without Isac's thys ---===============================\<close>
2.340 +ML \<open>
2.341 +\<close> ML \<open>
2.342 +Rewrite.trace_on := true
2.343 +\<close> ML \<open>
2.344 +"----------- test rewriting without Isac's thys ---------";
2.345 +"----------- test rewriting without Isac's thys ---------";
2.346 +"----------- test rewriting without Isac's thys ---------";
2.347 +
2.348 +"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
2.349 +val thy = @{theory Complex_Main};
2.350 +val ctxt = @{context};
2.351 +val thm = @{thm add.commute};
2.352 +val tm = @{term "x + y*z::real"};
2.353 +
2.354 +val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
2.355 + handle _ => error "rewrite.sml diff.behav. in rewriting 1";
2.356 +(*is displayed on _TOP_ of <response> buffer...*)
2.357 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
2.358 +if r = @{term "y*z + x::real"}
2.359 +then () else error "rewrite.sml diff.result in rewriting 2";
2.360 +
2.361 +\<close> ML \<open>
2.362 +"----- rewriting a subterm";
2.363 +val tm = @{term "w*(x + y*z)::real"};
2.364 +
2.365 +\<close> ML \<open>
2.366 +val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
2.367 + handle _ => error "rewrite.sml diff.behav. in rew_sub";
2.368 +
2.369 +"----- ordered rewriting";
2.370 +fun tord (_:subst) pp = LibraryC.termless pp;
2.371 +if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
2.372 +else error "rewrite.sml diff.behav. in ord.rewr.";
2.373 +
2.374 +\<close> text \<open>
2.375 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
2.376 + handle _ => error "rewrite.sml diff.behav. in rewriting 3";
2.377 +\<close> ML \<open>
2.378 +(** )
2.379 + rewrite_ thy tord Rule_Set.empty false thm tm;
2.380 +(**)# not: "x + y * z" > "y * z + x"
2.381 +exception NO_REWRITE raised (line 94 of "~/repos/isa/src/Tools/isac/MathEngBasic/rewrite.sml")( **)
2.382 +\<close> ML \<open>
2.383 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) = (thy, tord, Rule_Set.empty, false, thm, tm);
2.384 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) = (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
2.385 +\<close> ML \<open>
2.386 +(**)
2.387 + val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
2.388 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
2.389 +(*WAS* )exception NO_REWRITE raised (line 94 of "~/repos/isa/src/Tools/isac/MathEngBasic/rewrite.sml")( **)
2.390 +\<close> ML \<open>
2.391 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
2.392 + (thy, i, bdv, tless, rls, put_asm ,([(*root of the term*)]: TermC.path),
2.393 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
2.394 +\<close> ML \<open>
2.395 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
2.396 +\<close> ML \<open>
2.397 +(** )
2.398 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
2.399 +(**)exception MATCH raised (line 351 of "pattern.ML")( **)
2.400 +\<close> ML \<open>
2.401 +val t1 $ t2 = (*case*) t (*of*);
2.402 +\<close> ML \<open>
2.403 +(*+*)if UnparseC.term t = "w * (x + y * z)" then () else error "input to rew_sub CHANGED"
2.404 +\<close> ML \<open>
2.405 +rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
2.406 + handle NO_REWRITE => (t2, [], [], false)
2.407 +\<close> ML \<open>
2.408 +\<close> ML \<open>
2.409 +(** )
2.410 +val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
2.411 +(*WAS*)exception NO_REWRITE raised (line 94 of "~/repos/isa/src/Tools/isac/MathEngBasic/rewrite.sml")( **)
2.412 +\<close> ML \<open>
2.413 +\<close> ML \<open>
2.414 +\<close> ML \<open>
2.415 +\<close> ML \<open>
2.416 +\<close> ML \<open>
2.417 +\<close> ML \<open>
2.418 +\<close> ML \<open>
2.419 +\<close> ML \<open>
2.420 +\<close> ML \<open>
2.421 +\<close> ML \<open>
2.422 +\<close> ML \<open>
2.423 +\<close> text \<open>
2.424 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
2.425 + handle _ => error "rewrite.sml diff.behav. in rewriting 3";
2.426 +(*is displayed on _TOP_ of <response> buffer...*)
2.427 +Pretty.writeln (Proof_Context.pretty_term_abbrev @ {context} r);
2.428 +
2.429 +val tm = @{term "x*y + z::real"};
2.430 +val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
2.431 + handle _ => error "rewrite.sml diff.behav. in rewriting 4";
2.432 +
2.433 +
2.434 +\<close> ML \<open>
2.435 \<close> ML \<open>
2.436 \<close>
2.437