1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Apr 06 11:44:36 2020 +0200
1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Wed Apr 08 12:32:51 2020 +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 e_rls false thm tm)
1.8 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.9 handle _ => error "rewrite.sml diff.behav. in rewriting";
1.10 (*is displayed on _TOP_ of <response> buffer...*)
1.11 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.12 @@ -98,7 +98,7 @@
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 e_rls false thm tm)
1.17 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.18 handle _ => error "rewrite.sml diff.behav. in rew_sub";
1.19
1.20 "----- ordered rewriting";
1.21 @@ -106,13 +106,13 @@
1.22 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
1.23 else error "rewrite.sml diff.behav. in ord.rewr.";
1.24
1.25 -val NONE = (rewrite_ thy tord e_rls false thm tm)
1.26 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
1.27 handle _ => error "rewrite.sml diff.behav. in rewriting";
1.28 (*is displayed on _TOP_ of <response> buffer...*)
1.29 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
1.30
1.31 val tm = @{term "x*y + z::real"};
1.32 -val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
1.33 +val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
1.34 handle _ => error "rewrite.sml diff.behav. in rewriting";
1.35
1.36
1.37 @@ -146,7 +146,7 @@
1.38 "----- conditional rewriting creating an assumption";
1.39 val thm = @{thm nonzero_divide_mult_cancel_right};
1.40 val tm = @{term "x / (2 * x)::real"};
1.41 -val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
1.42 +val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
1.43 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
1.44
1.45 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
1.46 @@ -163,11 +163,11 @@
1.47 "----------- step through 'and rew_sub': ----------------";
1.48 (*and make asms without Trueprop, beginning with the result:*)
1.49 val tm = @{term "x / (2 * x)::real"};
1.50 -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;
1.51 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
1.52 (*show_types := false;*)
1.53 "----- evaluate arguments";
1.54 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.55 - (thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm);
1.56 + (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
1.57 "----- step 1: LHS, RHS of rule";
1.58 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.59 o Logic.strip_imp_concl) r;
1.60 @@ -239,7 +239,7 @@
1.61 (*------------ outcommented WN071210, after inclusion into ROOT.ML
1.62 val SOME (t,_) =
1.63 rewrite_inst_ thy e_rew_ord
1.64 - (append_rls "erls_isolate_bdvs" e_rls
1.65 + (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
1.66 [(Num_Calc ("EqSystem.occur'_exactly'_in",
1.67 eval_occur_exactly_in
1.68 "#eval_occur_exactly_in_"))
1.69 @@ -269,7 +269,7 @@
1.70 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.71 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
1.72 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.73 -##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
1.74 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
1.75 is_polyexp
1.76 ###### try calc: Poly.is'_polyexp'
1.77 ====== calc. to: False
1.78 @@ -288,7 +288,7 @@
1.79 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.80 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
1.81 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.82 -##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.83 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.84 ###### try calc: Poly.is'_polyexp'
1.85 ====== calc. to: False
1.86 ###### try calc: Poly.is'_polyexp'
1.87 @@ -311,7 +311,7 @@
1.88 "----- rewrite_ rat_mult_poly_r--------------------------";
1.89 val thm = @{thm rat_mult_poly_r};
1.90 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.91 -val erls = append_rls "e_rls-is_polyexp" e_rls
1.92 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.93 [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
1.94 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
1.95 (*t' = t''; (*false because of further rewrites in t'*)*)
1.96 @@ -396,7 +396,7 @@
1.97 val pat = parse_patt thy "?p :: real"
1.98 val pres = [parse_patt thy "?p is_multUnordered"];
1.99 val prepat = [(pres, pat)];
1.100 -val erls = append_rls "e_rls-is_multUnordered" e_rls
1.101 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.102 [Num_Calc ("Poly.is'_multUnordered",
1.103 eval_is_multUnordered "")];
1.104
1.105 @@ -537,8 +537,8 @@
1.106 case rul of
1.107 Rule.Thm (thmid, thm) =>
1.108 (trace1 i (" try thm: " ^ thmid);
1.109 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.110 - ((#erls o Rule.rep_rls) rls) put_asm thm ct of
1.111 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.112 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
1.113 NONE => rew_once ruls asm ct apno thms
1.114 | SOME (ct', asm') =>
1.115 (trace1 i (" rewrites to: " ^ Rule.t2str thy ct');
1.116 @@ -551,8 +551,8 @@
1.117 NONE => rew_once ruls asm ct apno thms
1.118 | SOME (_, thm') =>
1.119 let
1.120 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.121 - ((#erls o Rule.rep_rls) rls) put_asm thm' ct;
1.122 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.123 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.124 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.125 Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
1.126 val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt))
1.127 @@ -565,8 +565,8 @@
1.128 NONE => (ct, asm)
1.129 | SOME (_, thm') =>
1.130 let
1.131 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.132 - ((#erls o Rule.rep_rls) rls) put_asm thm' ct;
1.133 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.134 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.135 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.136 Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
1.137 val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt))
1.138 @@ -577,7 +577,7 @@
1.139 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.140 | NONE => rew_once ruls asm ct apno thms)
1.141 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
1.142 - val ruls = (#rules o Rule.rep_rls) rls;
1.143 + val ruls = (#rules o Rule.Rule_Set.rep) rls;
1.144 (* val _ = trace i (" rls: " ^ Rule_Set.id_rls rls ^ " on: " ^ Rule.t2str thy ct)*)
1.145 val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.146 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
1.147 @@ -585,11 +585,11 @@
1.148 val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
1.149
1.150 val SOME (ct', asm') = (*case*)
1.151 - rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
1.152 - ((#erls o Rule.rep_rls) rls) put_asm thm ct (*of*);
1.153 + rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.154 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
1.155 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
1.156 - = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.rep_rls) rls),
1.157 - ((#erls o Rule.rep_rls) rls), put_asm, thm, ct);
1.158 + = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
1.159 + ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
1.160
1.161 val (t', asms, _ (*lrd*), rew) =
1.162 rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.163 @@ -707,7 +707,7 @@
1.164 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.165 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
1.166 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
1.167 - (@{theory}, dummy_ord, e_rls, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
1.168 + (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
1.169 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.170 (thy, 1, [], rew_ord, erls, bool, thm, term);
1.171 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =