1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -185,7 +185,7 @@
1.4 [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
1.5 $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
1.6 | _ => error "rewrite.sml assumption changed";
1.7 -"=====^^^ make asms without Trueprop ---^^^";
1.8 +"===== \<up> make asms without Trueprop --- \<up> ";
1.9 "----- step 4: get the (instantiated) RHS";
1.10 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.11 o Logic.strip_imp_concl) r';
1.12 @@ -197,7 +197,7 @@
1.13 "----- step 0: args for rewrite_terms_, local fun";
1.14 val (thy, ord, erls, equs, t) =
1.15 (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
1.16 - TermC.str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
1.17 + TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
1.18 "----- step 1: args for rew_";
1.19 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
1.20 "----- step 2: rew_sub";
1.21 @@ -207,21 +207,21 @@
1.22
1.23 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.24 writeln "----------- rewrite_terms_ 1---------------------------";
1.25 -if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.26 +if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.27 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.28
1.29 val equs = [TermC.str2term "M_b 0 = 0"];
1.30 -val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.31 +val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
1.32 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.33 writeln "----------- rewrite_terms_ 2---------------------------";
1.34 -if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.35 +if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.36 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.37
1.38 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
1.39 -val t = TermC.str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.40 +val t = TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
1.41 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.42 writeln "----------- rewrite_terms_ 3---------------------------";
1.43 -if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.44 +if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
1.45 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.46
1.47
1.48 @@ -229,7 +229,7 @@
1.49 "----------- rewrite_inst_ bdvs -------------------------";
1.50 "----------- rewrite_inst_ bdvs -------------------------";
1.51 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
1.52 -val t = TermC.str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
1.53 +val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
1.54 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.55 (TermC.str2term"bdv_2",TermC.str2term"c_2"),
1.56 (TermC.str2term"bdv_3",TermC.str2term"c_3"),
1.57 @@ -244,7 +244,7 @@
1.58 ])
1.59 false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
1.60 (writeln o UnparseC.term) t;
1.61 -if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
1.62 +if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
1.63 then () else error "rewrite.sml rewrite_inst_ bdvs";
1.64 > Rewrite.trace_on:=true;
1.65 Rewrite.trace_on:=false;--------------------------------------------*)
1.66 @@ -255,55 +255,55 @@
1.67 "----------- check diff 2002--2009-3 --------------------";
1.68 (*----- 2002 -------------------------------------------------------------------
1.69 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
1.70 -q_0 * x ^^^ 2 / 2)
1.71 -## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
1.72 +q_0 * x \<up> 2 / 2)
1.73 +## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2
1.74 / 2)
1.75 ### try thm: real_diff_minus
1.76 ### try thm: sym_real_mult_minus1
1.77 -## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
1.78 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2
1.79 / 2)
1.80 ### try thm: rat_mult_poly_l
1.81 ### try thm: rat_mult_poly_r
1.82 -#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.83 -==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
1.84 - 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.85 -##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
1.86 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp
1.87 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) =
1.88 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
1.89 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2
1.90 is_polyexp
1.91 ###### try calc: Poly.is'_polyexp'
1.92 ====== calc. to: False
1.93 ###### try calc: Poly.is'_polyexp'
1.94 ###### try calc: Poly.is'_polyexp'
1.95 -#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
1.96 +#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp"]
1.97 ----- 2002 NONE rewrite --------------------------------------------------------
1.98 ----- 2009 should maintain this behaviour, but: --------------------------------
1.99 -# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
1.100 -## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
1.101 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)
1.102 +## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)
1.103 ### try thm: real_diff_minus
1.104 ### try thm: sym_real_mult_minus1
1.105 -## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
1.106 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)
1.107 ### try thm: rat_mult_poly_l
1.108 ### try thm: rat_mult_poly_r
1.109 -#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.110 -==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
1.111 - 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.112 -##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
1.113 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp
1.114 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) =
1.115 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
1.116 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp
1.117 ###### try calc: Poly.is'_polyexp'
1.118 ====== calc. to: False
1.119 ###### try calc: Poly.is'_polyexp'
1.120 ###### try calc: Poly.is'_polyexp'
1.121 -#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
1.122 -=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
1.123 +#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2 is_polyexp"] stored: ["False"]
1.124 +=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
1.125 ----- 2009 -------------------------------------------------------------------*)
1.126
1.127 (*the situation as was before repair (asm without Trueprop) is outcommented*)
1.128 val thy = @{theory "Isac_Knowledge"};
1.129 "===== example which raised the problem =================";
1.130 -val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
1.131 +val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)"};
1.132 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.133 val subs = [(@{term "bdv"}, @{term "x"})];
1.134 val rls = norm_Rational_noadd_fractions;
1.135 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
1.136 -if UnparseC.term t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
1.137 +if UnparseC.term t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x \<up> 2 / 2)" andalso
1.138 UnparseC.terms asms = "[]" then {}
1.139 else error "this was NONE with Isabelle2013-2 ?!?"
1.140 "----- rewrite_ rat_mult_poly_r--------------------------";
1.141 @@ -317,16 +317,16 @@
1.142 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
1.143 (*t'' = t'''; (*true*)*)
1.144 "----- rewrite_set_ erls --------------------------------";
1.145 -val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
1.146 +val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)"};
1.147 val NONE = rewrite_set_ thy true erls cond;
1.148 -(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
1.149 +(* \<up> ^^ goes with '====== calc. to: False' above from beginning*)
1.150
1.151 writeln "===== maximally simplified example =====================";
1.152 -val t = @{term "a / b * (x / x ^^^ 2)"};
1.153 +val t = @{term "a / b * (x / x \<up> 2)"};
1.154 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.155 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.156 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
1.157 -UnparseC.term t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
1.158 +UnparseC.term t' = "a * x / (b * x \<up> 2)"; (*rew. by thm outside test case*)
1.159 (*checked visually: Rewrite.trace_on looks like above for 2009*)
1.160
1.161 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
1.162 @@ -336,9 +336,9 @@
1.163 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
1.164 (*t'' = t'''; (*true*)*)
1.165 writeln "----- rewrite_set_ erls --------------------------------";
1.166 -val cond = @{term "(x / x ^^^ 2)"};
1.167 +val cond = @{term "(x / x \<up> 2)"};
1.168 val NONE = rewrite_set_ thy true erls cond;
1.169 -(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
1.170 +(* \<up> ^^ goes with '====== calc. to: False' above from beginning*)
1.171
1.172
1.173 "----------- compare all prepat's existing 2010 ---------";
1.174 @@ -390,7 +390,7 @@
1.175 "===== Poly.thy: order_mult_ ===";
1.176 (* ?p matched with the current term gives an environment,
1.177 which evaluates (the instantiated) "p is_multUnordered" to true*)
1.178 -val t = TermC.str2term "x^^^2 * x";
1.179 +val t = TermC.str2term "x \<up> 2 * x";
1.180 val pat = TermC.parse_patt thy "?p :: real"
1.181 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
1.182 val prepat = [(pres, pat)];
1.183 @@ -400,7 +400,7 @@
1.184
1.185 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.186 val asms = map (Envir.subst_term subst) pres;
1.187 -if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
1.188 +if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
1.189 then () else error "rewrite.sml: prepat order_mult_ subst";
1.190 if ([], true) = eval__true thy 0 asms [] erls
1.191 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.192 @@ -409,10 +409,10 @@
1.193 "----------- fun app_rev, Rrls, -------------------------";
1.194 "----------- fun app_rev, Rrls, -------------------------";
1.195 "----------- fun app_rev, Rrls, -------------------------";
1.196 -val t = TermC.str2term "x^^^2 * x";
1.197 +val t = TermC.str2term "x \<up> 2 * x";
1.198
1.199 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
1.200 -val tm = TermC.str2term "(x^^^2 * x) is_multUnordered";
1.201 +val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
1.202 eval_is_multUnordered "testid" "" tm thy;
1.203
1.204 case eval_is_multUnordered "testid" "" tm thy of
1.205 @@ -422,10 +422,10 @@
1.206 Const ("HOL.True", _))) => ()
1.207 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
1.208
1.209 -tracing "----- begin rewrite x^^^2 * x ---"; Rewrite.trace_on := false;
1.210 +tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
1.211 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.212 -tracing "----- end rewrite x^^^2 * x ---"; Rewrite.trace_on := false;
1.213 -if UnparseC.term t' = "x * x ^^^ 2" then ()
1.214 +tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
1.215 +if UnparseC.term t' = "x * x \<up> 2" then ()
1.216 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
1.217
1.218 (* for achieving the previous result, the following code was taken apart *)
1.219 @@ -479,7 +479,7 @@
1.220 tracing "=== poly.sml: scan_ chk prepat end";
1.221
1.222 "----- chk ---";
1.223 -(*reestablish...*) val t = TermC.str2term "x ^^^ 2 * x";
1.224 +(*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
1.225 val [(pres, pat)] = prepat;
1.226 val subst: Type.tyenv * Envir.tenv =
1.227 Pattern.match thy (pat, t)
1.228 @@ -488,10 +488,10 @@
1.229 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
1.230 "----- eval__true ---";
1.231 val asms = (map (Envir.subst_term subst) pres);
1.232 -if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
1.233 +if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
1.234 else error "rewrite.sml: diff. is_multUnordered, asms";
1.235 val (thy, i, asms, bdv, rls) =
1.236 - (thy, (i+1), [TermC.str2term "(x^^^2 * x) is_multUnordered"],
1.237 + (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
1.238 [] : (term * term) list, erls);
1.239 case eval__true thy i asms bdv rls of
1.240 ([], true) => ()
1.241 @@ -514,7 +514,7 @@
1.242 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
1.243 val thy = @{theory RatEq};
1.244 val ctxt = Proof_Context.init_global thy;
1.245 -val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
1.246 +val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
1.247 val rls = assoc_rls "RatEq_eliminate"
1.248
1.249 val SOME (t''''', asm''''') =
1.250 @@ -599,22 +599,22 @@
1.251 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
1.252 ;
1.253 (*+*)if UnparseC.term r' =
1.254 -(*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
1.255 -(*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
1.256 -(*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
1.257 +(*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
1.258 +(*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
1.259 +(*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
1.260 (*+*) " 1 / x) =\n" ^
1.261 -(*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
1.262 -(*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
1.263 +(*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
1.264 +(*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
1.265 (*+*)then () else error "instantiated rule CHANGED";
1.266
1.267 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.268 ;
1.269 -(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.270 +(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
1.271 (*+*)then () else error "stored assumptions CHANGED";
1.272
1.273 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.274 ;
1.275 -(*+*)if UnparseC.term t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
1.276 +(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
1.277 (*+*)then () else error "rewritten term (an equality) CHANGED";
1.278
1.279 val (simpl_p', nofalse) =
1.280 @@ -622,7 +622,7 @@
1.281 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
1.282 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
1.283
1.284 -(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.285 +(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
1.286 (*+*)then () else error "asms before chk CHANGED";
1.287
1.288 fun chk indets [] = (indets, true) (*return asms<>True until false*)
1.289 @@ -632,7 +632,7 @@
1.290 | SOME (t, a') =>
1.291 if t = @{term True} then (chk (indets @ a') asms)
1.292 else if t = @{term False} then ([], false)
1.293 - (*asm false .. thm not applied ^^^; continue until False vvv*)
1.294 + (*asm false .. thm not applied \<up> ; continue until False vvv*)
1.295 else chk (indets @ [t] @ a') asms);
1.296
1.297 val (xxx, true) =