1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -171,15 +171,15 @@
1.4 "----- step 1: LHS, RHS of rule";
1.5 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.6 o Logic.strip_imp_concl) r;
1.7 -UnparseC.term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
1.8 -UnparseC.term2str LHS = "?b / (?a * ?b)"; UnparseC.term2str RHS = "(1::?'a) / ?a";
1.9 +UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
1.10 +UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
1.11 "----- step 2: the rule instantiated";
1.12 val r' = Envir.subst_term
1.13 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
1.14 -UnparseC.term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
1.15 +UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
1.16 "----- step 3: get the (instantiated) assumption(s)";
1.17 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
1.18 -UnparseC.term2str (hd p') = "x \<noteq> 0";
1.19 +UnparseC.term (hd p') = "x \<noteq> 0";
1.20 "=====vvv make asms without Trueprop ---vvv";
1.21 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
1.22 (Logic.count_prems r', [], r'));
1.23 @@ -191,7 +191,7 @@
1.24 "----- step 4: get the (instantiated) RHS";
1.25 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.26 o Logic.strip_imp_concl) r';
1.27 -UnparseC.term2str t' = "1 / 2";
1.28 +UnparseC.term t' = "1 / 2";
1.29
1.30 "----------- step through 'fun rewrite_terms_' ---------";
1.31 "----------- step through 'fun rewrite_terms_' ---------";
1.32 @@ -209,21 +209,21 @@
1.33
1.34 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.35 writeln "----------- rewrite_terms_ 1---------------------------";
1.36 -if UnparseC.term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.37 +if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.38 else error "rewrite.sml rewrite_terms_ [x = 0]";
1.39
1.40 val equs = [str2term "M_b 0 = 0"];
1.41 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.42 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.43 writeln "----------- rewrite_terms_ 2---------------------------";
1.44 -if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.45 +if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.46 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.47
1.48 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
1.49 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.50 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
1.51 writeln "----------- rewrite_terms_ 3---------------------------";
1.52 -if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.53 +if UnparseC.term t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.54 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.55
1.56
1.57 @@ -245,8 +245,8 @@
1.58 "#eval_occur_exactly_in_"))
1.59 ])
1.60 false bdvs (num_str @{separate_bdvs_add) t;
1.61 -(writeln o UnparseC.term2str) t;
1.62 -if UnparseC.term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
1.63 +(writeln o UnparseC.term) t;
1.64 +if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
1.65 then () else error "rewrite.sml rewrite_inst_ bdvs";
1.66 > trace_rewrite:=true;
1.67 trace_rewrite:=false;--------------------------------------------*)
1.68 @@ -305,8 +305,8 @@
1.69 val subs = [(@{term "bdv"}, @{term "x"})];
1.70 val rls = norm_Rational_noadd_fractions;
1.71 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
1.72 -if UnparseC.term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
1.73 - UnparseC.terms2str asms = "[]" then {}
1.74 +if UnparseC.term t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
1.75 + UnparseC.terms asms = "[]" then {}
1.76 else error "this was NONE with Isabelle2013-2 ?!?"
1.77 "----- rewrite_ rat_mult_poly_r--------------------------";
1.78 val thm = @{thm rat_mult_poly_r};
1.79 @@ -328,7 +328,7 @@
1.80 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
1.81 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
1.82 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
1.83 -UnparseC.term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
1.84 +UnparseC.term t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
1.85 (*checked visually: trace_rewrite looks like above for 2009*)
1.86
1.87 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
1.88 @@ -354,7 +354,7 @@
1.89
1.90 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.91 val preinst = Envir.subst_term inst precond;
1.92 -UnparseC.term2str preinst;
1.93 +UnparseC.term preinst;
1.94
1.95 "===== Rational.thy: cancel ===";
1.96 (* pat matched with the current term gives an environment
1.97 @@ -370,7 +370,7 @@
1.98
1.99 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.100 val asms = map (Envir.subst_term subst) pres;
1.101 -if UnparseC.terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
1.102 +if UnparseC.terms asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
1.103 then () else error "rewrite.sml: prepat cancel subst";
1.104 if ([], true) = eval__true thy 0 asms [] erls
1.105 then () else error "rewrite.sml: prepat cancel eval__true";
1.106 @@ -402,7 +402,7 @@
1.107
1.108 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
1.109 val asms = map (Envir.subst_term subst) pres;
1.110 -if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
1.111 +if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
1.112 then () else error "rewrite.sml: prepat order_mult_ subst";
1.113 if ([], true) = eval__true thy 0 asms [] erls
1.114 then () else error "rewrite.sml: prepat order_mult_ eval__true";
1.115 @@ -427,7 +427,7 @@
1.116 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
1.117 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.118 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
1.119 -if UnparseC.term2str t' = "x * x ^^^ 2" then ()
1.120 +if UnparseC.term t' = "x * x ^^^ 2" then ()
1.121 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
1.122
1.123 (* for achieving the previous result, the following code was taken apart *)
1.124 @@ -455,7 +455,7 @@
1.125 (*.apply the normal_form of a rev-set.*)
1.126 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.127 if chk_prepat thy erls prepat t
1.128 - then ((*tracing("### app_rev': t = "^(UnparseC.term2str t));*)
1.129 + then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
1.130 normal_form t)
1.131 else NONE;
1.132 (*fixme val NONE = app_rev' thy rrls t;*)
1.133 @@ -490,7 +490,7 @@
1.134 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
1.135 "----- eval__true ---";
1.136 val asms = (map (Envir.subst_term subst) pres);
1.137 -if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
1.138 +if UnparseC.terms asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
1.139 else error "rewrite.sml: diff. is_multUnordered, asms";
1.140 val (thy, i, asms, bdv, rls) =
1.141 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
1.142 @@ -541,7 +541,7 @@
1.143 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
1.144 NONE => rew_once ruls asm ct apno thms
1.145 | SOME (ct', asm') =>
1.146 - (trace1 i (" rewrites to: " ^ UnparseC.t2str thy ct');
1.147 + (trace1 i (" rewrites to: " ^ UnparseC.term_thy thy ct');
1.148 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.149 (* once again try the same rule, e.g. associativity against "()"*)
1.150 | Rule.Num_Calc (cc as (op_, _)) =>
1.151 @@ -554,8 +554,8 @@
1.152 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
1.153 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
1.154 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.155 - Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
1.156 - val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
1.157 + Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
1.158 + val _ = trace1 i (" calc. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
1.159 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.160 end
1.161 | Rule.Cal1 (cc as (op_, _)) =>
1.162 @@ -568,8 +568,8 @@
1.163 val pairopt = 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;
1.165 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.166 - Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
1.167 - val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
1.168 + Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.term_thy thy ct ^ " = NONE")
1.169 + val _ = trace1 i (" cal1. to: " ^ UnparseC.term_thy thy ((fst o the) pairopt))
1.170 in the pairopt end
1.171 end
1.172 | Rule.Rls_ rls' =>
1.173 @@ -578,7 +578,7 @@
1.174 | NONE => rew_once ruls asm ct apno thms)
1.175 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
1.176 val ruls = (#rules o Rule.Rule_Set.rep) rls;
1.177 -(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.t2str thy ct)*)
1.178 +(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_thy thy ct)*)
1.179 val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.180 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
1.181 = (ruls, []:term list, ct, Noap, ruls);
1.182 @@ -600,7 +600,7 @@
1.183 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.184 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
1.185 ;
1.186 -(*+*)if UnparseC.term2str r' =
1.187 +(*+*)if UnparseC.term r' =
1.188 (*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
1.189 (*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
1.190 (*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
1.191 @@ -611,12 +611,12 @@
1.192
1.193 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.194 ;
1.195 -(*+*)if map UnparseC.term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.196 +(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.197 (*+*)then () else error "stored assumptions CHANGED";
1.198
1.199 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.200 ;
1.201 -(*+*)if UnparseC.term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
1.202 +(*+*)if UnparseC.term t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
1.203 (*+*)then () else error "rewritten term (an equality) CHANGED";
1.204
1.205 val (simpl_p', nofalse) =
1.206 @@ -624,7 +624,7 @@
1.207 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
1.208 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
1.209
1.210 -(*+*)if map UnparseC.term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.211 +(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
1.212 (*+*)then () else error "asms before chk CHANGED";
1.213
1.214 fun chk indets [] = (indets, true) (*return asms<>True until false*)
1.215 @@ -663,7 +663,7 @@
1.216 val (* SOME (t, a') *)NONE = (*case*)
1.217 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
1.218
1.219 -(*+*)UnparseC.term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
1.220 +(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
1.221 (*
1.222 :
1.223 #### rls: rateq_erls on: x \<noteq> 0
1.224 @@ -717,10 +717,10 @@
1.225 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.226 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.227 ;
1.228 -if UnparseC.term2str lhss = "?a * (?b + ?c)" andalso UnparseC.term2str t = "x * (y + z)" then ()
1.229 +if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
1.230 else error "ARGS FOR Pattern.match CHANGED";
1.231 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
1.232 -if (Envir.subst_term match r |> UnparseC.term2str) = "x * (y + z) = x * y + x * z" then ()
1.233 +if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
1.234 else error "Pattern.match CHANGED";
1.235
1.236 "----------- fun mk_thm ------------------------------------------------------------------------";
1.237 @@ -742,7 +742,7 @@
1.238 | _ => writeln "parse does NOT take patterns with '?'";
1.239
1.240 val t1 = (#prop o Thm.rep_thm) (num_str thm);
1.241 -if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.242 +if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.243
1.244 val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
1.245 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
1.246 @@ -774,7 +774,7 @@
1.247 | _ => writeln "parse does NOT take patterns with '?'";
1.248
1.249 val t1 = (#prop o Thm.rep_thm) (num_str thm);
1.250 -if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.251 +if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
1.252
1.253 val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
1.254 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
1.255 @@ -798,7 +798,7 @@
1.256 val term = str2term "x + 1 = 2";
1.257
1.258 val SOME (t, asm) = rewrite_set_ thy false rls term;
1.259 -if UnparseC.term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
1.260 +if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
1.261
1.262 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
1.263 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);