1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -34,10 +34,10 @@
1.4 val thy = @{theory Complex_Main};
1.5 val ctxt = @{context};
1.6 val thm = @{thm add.commute};
1.7 -val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
1.8 +val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
1.9 "----- from old: fun rewrite__";
1.10 val bdv = [];
1.11 -val r = inst_bdv bdv (norm (Thm.prop_of thm));
1.12 +val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
1.13 "----- from old: and rew_sub";
1.14 val (LHS,RHS) = (dest_equals o strip_trueprop
1.15 o Logic.strip_imp_concl) r;
1.16 @@ -196,8 +196,8 @@
1.17 "----------- step through 'fun rewrite_terms_' ---------";
1.18 "----- step 0: args for rewrite_terms_, local fun";
1.19 val (thy, ord, erls, equs, t) =
1.20 - (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
1.21 - str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
1.22 + (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
1.23 + TermC.str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
1.24 "----- step 1: args for rew_";
1.25 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
1.26 "----- step 2: rew_sub";
1.27 @@ -210,15 +210,15 @@
1.28 if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.29 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.30
1.31 -val equs = [str2term "M_b 0 = 0"];
1.32 -val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.33 +val equs = [TermC.str2term "M_b 0 = 0"];
1.34 +val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.35 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.36 writeln "----------- rewrite_terms_ 2---------------------------";
1.37 if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.38 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.39
1.40 -val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
1.41 -val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.42 +val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
1.43 +val t = TermC.str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.44 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.45 writeln "----------- rewrite_terms_ 3---------------------------";
1.46 if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.47 @@ -229,11 +229,11 @@
1.48 "----------- rewrite_inst_ bdvs -------------------------";
1.49 "----------- rewrite_inst_ bdvs -------------------------";
1.50 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
1.51 -val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
1.52 -val bdvs = [(str2term"bdv_1",str2term"c"),
1.53 - (str2term"bdv_2",str2term"c_2"),
1.54 - (str2term"bdv_3",str2term"c_3"),
1.55 - (str2term"bdv_4",str2term"c_4")];
1.56 +val t = TermC.str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
1.57 +val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.58 + (TermC.str2term"bdv_2",TermC.str2term"c_2"),
1.59 + (TermC.str2term"bdv_3",TermC.str2term"c_3"),
1.60 + (TermC.str2term"bdv_4",TermC.str2term"c_4")];
1.61 (*------------ outcommented WN071210, after inclusion into ROOT.ML
1.62 val SOME (t,_) =
1.63 rewrite_inst_ thy e_rew_ord
1.64 @@ -346,9 +346,9 @@
1.65 "----------- compare all prepat's existing 2010 ---------";
1.66 val thy = @{theory "Isac_Knowledge"};
1.67 val t = @{term "a + b * x = (0 ::real)"};
1.68 -val pat = parse_patt thy "?l = (?r ::real)";
1.69 -val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
1.70 -val precond = parse_patt thy "(?l::real) is_expanded";
1.71 +val pat = TermC.parse_patt thy "?l = (?r ::real)";
1.72 +val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
1.73 +val precond = TermC.parse_patt thy "(?l::real) is_expanded";
1.74
1.75 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.76 val preinst = Envir.subst_term inst precond;
1.77 @@ -359,9 +359,9 @@
1.78 (or not: hen the Rrls not applied);
1.79 if pre1 and pre2 evaluate to @{term True} in this environment,
1.80 then the Rrls is applied. *)
1.81 -val t = str2term "(a + b) / c ::real";
1.82 -val pat = parse_patt thy "?r / ?s ::real";
1.83 -val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
1.84 +val t = TermC.str2term "(a + b) / c ::real";
1.85 +val pat = TermC.parse_patt thy "?r / ?s ::real";
1.86 +val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
1.87 val prepat = [(pres, pat)];
1.88 val erls = rational_erls;
1.89 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
1.90 @@ -374,10 +374,10 @@
1.91 then () else error "rewrite.sml: prepat cancel eval__true";
1.92
1.93 "===== Rational.thy: add_fractions_p ===";
1.94 -(* if each pat* matches with the current term, the Rrls is applied
1.95 +(* if each pat* TermC.matches with the current term, the Rrls is applied
1.96 (there are no preconditions to be checked, they are @{term True}) *)
1.97 -val t = str2term "a / b + 1 / 2";
1.98 -val pat = parse_patt thy "?r / ?s + ?u / ?v";
1.99 +val t = TermC.str2term "a / b + 1 / 2";
1.100 +val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
1.101 val pres = [@{term True}];
1.102 val prepat = [(pres, pat)];
1.103 val erls = rational_erls;
1.104 @@ -390,9 +390,9 @@
1.105 "===== Poly.thy: order_mult_ ===";
1.106 (* ?p matched with the current term gives an environment,
1.107 which evaluates (the instantiated) "p is_multUnordered" to true*)
1.108 -val t = str2term "x^^^2 * x";
1.109 -val pat = parse_patt thy "?p :: real"
1.110 -val pres = [parse_patt thy "?p is_multUnordered"];
1.111 +val t = TermC.str2term "x^^^2 * x";
1.112 +val pat = TermC.parse_patt thy "?p :: real"
1.113 +val pres = [TermC.parse_patt thy "?p is_multUnordered"];
1.114 val prepat = [(pres, pat)];
1.115 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.116 [Eval ("Poly.is'_multUnordered",
1.117 @@ -409,10 +409,10 @@
1.118 "----------- fun app_rev, Rrls, -------------------------";
1.119 "----------- fun app_rev, Rrls, -------------------------";
1.120 "----------- fun app_rev, Rrls, -------------------------";
1.121 -val t = str2term "x^^^2 * x";
1.122 +val t = TermC.str2term "x^^^2 * x";
1.123
1.124 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.125 -val tm = str2term "(x^^^2 * x) is_multUnordered";
1.126 +val tm = TermC.str2term "(x^^^2 * x) is_multUnordered";
1.127 eval_is_multUnordered "testid" "" tm thy;
1.128
1.129 case eval_is_multUnordered "testid" "" tm thy of
1.130 @@ -479,7 +479,7 @@
1.131 tracing "=== poly.sml: scan_ chk prepat end";
1.132
1.133 "----- chk ---";
1.134 -(*reestablish...*) val t = str2term "x ^^^ 2 * x";
1.135 +(*reestablish...*) val t = TermC.str2term "x ^^^ 2 * x";
1.136 val [(pres, pat)] = prepat;
1.137 val subst: Type.tyenv * Envir.tenv =
1.138 Pattern.match thy (pat, t)
1.139 @@ -491,7 +491,7 @@
1.140 if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
1.141 else error "rewrite.sml: diff. is_multUnordered, asms";
1.142 val (thy, i, asms, bdv, rls) =
1.143 - (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
1.144 + (thy, (i+1), [TermC.str2term "(x^^^2 * x) is_multUnordered"],
1.145 [] : (term * term) list, erls);
1.146 case eval__true thy i asms bdv rls of
1.147 ([], true) => ()
1.148 @@ -502,12 +502,12 @@
1.149 "----------- 2011 thms with axclasses -------------------";
1.150 val thm = ThmC.numerals_to_Free @{thm div_by_1};
1.151 val prop = Thm.prop_of thm;
1.152 -atomty prop; (*Type 'a*)
1.153 -val t = str2term "(2*x)/1"; (*Type real*)
1.154 +TermC.atomty prop; (*Type 'a*)
1.155 +val t = TermC.str2term "(2*x)/1"; (*Type real*)
1.156
1.157 val (thy, ro, er, inst) =
1.158 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
1.159 -val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
1.160 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
1.161
1.162 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.163 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.164 @@ -688,7 +688,7 @@
1.165 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.166 (thy, 1, [], rew_ord, erls, bool, thm, term);
1.167 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.168 - (thy, i, bdv, tless, rls, put_asm, [], inst_bdv bdv (norm (Thm.prop_of thm)), ct)
1.169 + (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
1.170 val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.171 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
1.172 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.173 @@ -706,7 +706,7 @@
1.174 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
1.175 val thy = @{theory};
1.176 val rls = norm_equation;
1.177 -val term = str2term "x + 1 = 2";
1.178 +val term = TermC.str2term "x + 1 = 2";
1.179
1.180 val SOME (t, asm) = rewrite_set_ thy false rls term;
1.181 if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";