1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -33,46 +33,46 @@
1.4 "----------- occur_exactly_in ------------------------------------";
1.5 "----------- occur_exactly_in ------------------------------------";
1.6 "----------- occur_exactly_in ------------------------------------";
1.7 -val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
1.8 -val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.9 +val all = [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"];
1.10 +val t = TermC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.11
1.12 -if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
1.13 +if occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2"] all t
1.14 then () else error "eqsystem.sml occur_exactly_in 1";
1.15
1.16 -if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
1.17 +if not (occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"] all t)
1.18 then () else error "eqsystem.sml occur_exactly_in 2";
1.19
1.20 -if not (occur_exactly_in [TermC.str2term"c_2"] all t)
1.21 +if not (occur_exactly_in [TermC.parse_test @{context}"c_2"] all t)
1.22 then () else error "eqsystem.sml occur_exactly_in 3";
1.23
1.24 -val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.25 +val t = TermC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.26 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.27 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.28 if str = "[c, c_2] from [c, c_2,\n" ^
1.29 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
1.30 then () else error "eval_occur_exactly_in [c, c_2]";
1.31
1.32 -val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
1.33 +val t = TermC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
1.34 "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
1.35 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.36 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
1.37 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
1.38 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
1.39
1.40 -val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
1.41 +val t = TermC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
1.42 \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.43 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.44 if str = "[c_2] from [c, c_2,\n" ^
1.45 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
1.46 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
1.47
1.48 -val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
1.49 +val t = TermC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
1.50 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.51 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
1.52 else error "eval_occur_exactly_in [c, c_2, c_3]";
1.53
1.54 val t =
1.55 - TermC.str2term
1.56 + TermC.parse_test @{context}
1.57 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
1.58 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.59 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
1.60 @@ -82,7 +82,7 @@
1.61 "----------- problems --------------------------------------------";
1.62 "----------- problems --------------------------------------------";
1.63 "----------- problems --------------------------------------------";
1.64 -val t = TermC.str2term "Length [x+y=1,y=2] = 2";
1.65 +val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";
1.66 TermC.atomty t;
1.67 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
1.68 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
1.69 @@ -99,10 +99,10 @@
1.70 val SOME t = TermC.parseNEW ctxt "solution LL";
1.71 TermC.atomty t;
1.72
1.73 -val t = TermC.str2term
1.74 +val t = TermC.parse_test @{context}
1.75 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
1.76 TermC.atomty t;
1.77 -val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
1.78 +val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
1.79 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
1.80 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
1.81 assume flawed test setup hidden by "handle _ => ..."
1.82 @@ -126,39 +126,39 @@
1.83 "----------- rewrite-order ord_simplify_System -------------------";
1.84 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
1.85 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
1.86 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
1.87 - TermC.str2term"c * x") then ()
1.88 +if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
1.89 + TermC.parse_test @{context}"c * x") then ()
1.90 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
1.91
1.92 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
1.93 - TermC.str2term"c_2") then ()
1.94 +if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
1.95 + TermC.parse_test @{context}"c_2") then ()
1.96 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
1.97
1.98 -if ord_simplify_System false thy [] (TermC.str2term"c * x",
1.99 - TermC.str2term"c_2") then ()
1.100 +if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x",
1.101 + TermC.parse_test @{context}"c_2") then ()
1.102 else error "integrate.sml, (c * x) < (c_2) not#3";
1.103
1.104 "--- mult.commute ---";
1.105 -if ord_simplify_System false thy [] (TermC.str2term"x * c",
1.106 - TermC.str2term"c * x") then ()
1.107 +if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c",
1.108 + TermC.parse_test @{context}"c * x") then ()
1.109 else error "integrate.sml, (x * c) < (c * x) not#4";
1.110
1.111 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
1.112 - TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
1.113 +if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
1.114 + TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")
1.115 then () else error "integrate.sml, (. * .) < (. * .) not#5";
1.116
1.117 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
1.118 - TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
1.119 +if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
1.120 + TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")
1.121 then () else error "integrate.sml, (. * .) < (. * .) not#6";
1.122
1.123
1.124 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.125 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.126 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.127 -val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
1.128 +val t = TermC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
1.129 \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
1.130 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.131 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.132 +val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
1.133 + (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
1.134 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.135 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
1.136 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
1.137 @@ -182,7 +182,7 @@
1.138 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
1.139 val ctxt = Proof_Context.init_global thy;
1.140 val t =
1.141 - TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
1.142 + TermC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
1.143 \ - 1 * q_0 / 24 * 0 \<up> 4),\
1.144 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
1.145 \ - 1 * q_0 / 24 * L \<up> 4)]";
1.146 @@ -218,10 +218,10 @@
1.147 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.148 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.149 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.150 -val e1__ = TermC.str2term "c_2 = 77";
1.151 -val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
1.152 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.153 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.154 +val e1__ = TermC.parse_test @{context} "c_2 = 77";
1.155 +val e2__ = TermC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
1.156 +val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
1.157 + (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
1.158 val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
1.159 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
1.160 else error "eqsystem.sml top_down_substitution,2x2] subst";
1.161 @@ -235,15 +235,15 @@
1.162 if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
1.163 else error "eqsystem.sml top_down_substitution,2x2] isolate";
1.164
1.165 -val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
1.166 +val t = TermC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
1.167 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
1.168 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
1.169 else error "eqsystem.sml top_down_substitution,2x2] order_system";
1.170
1.171 if not (ord_simplify_System
1.172 false thy []
1.173 - (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
1.174 - TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
1.175 + (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
1.176 + TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
1.177 then () else error "eqsystem.sml, order_result rew_ord";
1.178
1.179
1.180 @@ -251,15 +251,15 @@
1.181 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.182 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.183 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
1.184 -val t = TermC.str2term (
1.185 +val t = TermC.parse_test @{context} (
1.186 "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
1.187 "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
1.188 "c + c_2 + c_3 + c_4 = 0, " ^
1.189 "c_2 + c_3 + c_4 = 0]");
1.190 -val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
1.191 - (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
1.192 - (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
1.193 - (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
1.194 +val bdvs = [(TermC.parse_test @{context}"bdv_1::real",TermC.parse_test @{context}"c::real"),
1.195 + (TermC.parse_test @{context}"bdv_2::real",TermC.parse_test @{context}"c_2::real"),
1.196 + (TermC.parse_test @{context}"bdv_3::real",TermC.parse_test @{context}"c_3::real"),
1.197 + (TermC.parse_test @{context}"bdv_4::real",TermC.parse_test @{context}"c_4::real")];
1.198 val SOME (t, _) =
1.199 rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.200 if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
1.201 @@ -367,7 +367,7 @@
1.202 (*... resulted in
1.203 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
1.204 [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
1.205 -val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
1.206 +val t = TermC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
1.207 "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
1.208
1.209 val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;