1.1 --- a/test/Tools/isac/Test_Some.thy Fri Sep 16 12:13:23 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Mon Sep 26 10:57:53 2022 +0200
1.3 @@ -111,6 +111,584 @@
1.4 section \<open>===================================================================================\<close>
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 +(* Title: Knowledge/eqsystem-1.sml
1.8 + author: Walther Neuper 050826,
1.9 + (c) due to copyright terms
1.10 +*)
1.11 +
1.12 +"-----------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------";
1.14 +"-----------------------------------------------------------------";
1.15 +"----------- occur_exactly_in ------------------------------------";
1.16 +"----------- problems --------------------------------------------";
1.17 +"----------- rewrite-order ord_simplify_System -------------------";
1.18 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.19 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.20 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.21 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.22 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.23 +"----------- refine [linear,system]-------------------------------";
1.24 +"----------- refine [2x2,linear,system] search error--------------";
1.25 +(*^^^--- eqsystem-1.sml #####################################################################*)
1.26 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.27 +(*^^^--- eqsystem-1a.sml #####################################################################
1.28 + vvv--- eqsystem-2.sml #####################################################################*)
1.29 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
1.30 +"----------- all systems from Biegelinie -------------------------";
1.31 +"----------- 4x4 systems from Biegelinie -------------------------";
1.32 +"-----------------------------------------------------------------";
1.33 +"-----------------------------------------------------------------";
1.34 +"-----------------------------------------------------------------";
1.35 +
1.36 +val thy = @{theory "EqSystem"};
1.37 +val ctxt = Proof_Context.init_global thy;
1.38 +
1.39 +"----------- occur_exactly_in ------------------------------------";
1.40 +"----------- occur_exactly_in ------------------------------------";
1.41 +"----------- occur_exactly_in ------------------------------------";
1.42 +val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
1.43 +val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.44 +
1.45 +if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
1.46 +then () else error "eqsystem.sml occur_exactly_in 1";
1.47 +
1.48 +if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
1.49 +then () else error "eqsystem.sml occur_exactly_in 2";
1.50 +
1.51 +if not (occur_exactly_in [TermC.str2term"c_2"] all t)
1.52 +then () else error "eqsystem.sml occur_exactly_in 3";
1.53 +
1.54 +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.55 +eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.56 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.57 +if str = "[c, c_2] from [c, c_2,\n" ^
1.58 + " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
1.59 +then () else error "eval_occur_exactly_in [c, c_2]";
1.60 +
1.61 +val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
1.62 + "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
1.63 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.64 +if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
1.65 +" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
1.66 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
1.67 +
1.68 +val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
1.69 + \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
1.70 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.71 +if str = "[c_2] from [c, c_2,\n" ^
1.72 + " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
1.73 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
1.74 +
1.75 +val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
1.76 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.77 +if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
1.78 +else error "eval_occur_exactly_in [c, c_2, c_3]";
1.79 +
1.80 +val t =
1.81 + TermC.str2term
1.82 + "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
1.83 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
1.84 +if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
1.85 + \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
1.86 +else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
1.87 +
1.88 +"----------- problems --------------------------------------------";
1.89 +"----------- problems --------------------------------------------";
1.90 +"----------- problems --------------------------------------------";
1.91 +val t = TermC.str2term "Length [x+y=1,y=2] = 2";
1.92 +TermC.atomty t;
1.93 +val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
1.94 + [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
1.95 + (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
1.96 + Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
1.97 + Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
1.98 + ];
1.99 +val SOME (t',_) = rewrite_set_ ctxt false testrls t;
1.100 +if UnparseC.term t' = "True" then ()
1.101 +else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
1.102 +
1.103 +val SOME t = TermC.parseNEW ctxt "solution LL";
1.104 +TermC.atomty t;
1.105 +val SOME t = TermC.parseNEW ctxt "solution LL";
1.106 +TermC.atomty t;
1.107 +
1.108 +val t = TermC.str2term
1.109 +"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
1.110 +TermC.atomty t;
1.111 +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.112 + "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
1.113 +(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
1.114 + assume flawed test setup hidden by "handle _ => ..."
1.115 + ERROR rewrite__set_ called with 'Erls' for '1 < 1'
1.116 +val SOME (t,_) =
1.117 + rewrite_set_ ctxt true
1.118 + (Rule_Set.append_rules "prls_" Rule_Set.empty
1.119 + [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.120 + Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.121 + Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
1.122 + Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
1.123 + Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
1.124 + ]) t;
1.125 +if t = @{term True} then ()
1.126 +else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
1.127 + broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
1.128 +
1.129 +
1.130 +"----------- rewrite-order ord_simplify_System -------------------";
1.131 +"----------- rewrite-order ord_simplify_System -------------------";
1.132 +"----------- rewrite-order ord_simplify_System -------------------";
1.133 +"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
1.134 +"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
1.135 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
1.136 + TermC.str2term"c * x") then ()
1.137 +else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
1.138 +
1.139 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
1.140 + TermC.str2term"c_2") then ()
1.141 +else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
1.142 +
1.143 +if ord_simplify_System false thy [] (TermC.str2term"c * x",
1.144 + TermC.str2term"c_2") then ()
1.145 +else error "integrate.sml, (c * x) < (c_2) not#3";
1.146 +
1.147 +"--- mult.commute ---";
1.148 +if ord_simplify_System false thy [] (TermC.str2term"x * c",
1.149 + TermC.str2term"c * x") then ()
1.150 +else error "integrate.sml, (x * c) < (c * x) not#4";
1.151 +
1.152 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
1.153 + TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
1.154 +then () else error "integrate.sml, (. * .) < (. * .) not#5";
1.155 +
1.156 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
1.157 + TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
1.158 +then () else error "integrate.sml, (. * .) < (. * .) not#6";
1.159 +
1.160 +
1.161 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.162 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.163 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.164 +val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
1.165 + \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
1.166 +val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.167 + (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.168 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.169 +if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
1.170 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
1.171 +
1.172 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
1.173 +if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
1.174 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
1.175 +
1.176 +val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
1.177 +if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
1.178 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
1.179 +
1.180 +"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
1.181 +val SOME (t,_) = rewrite_set_ ctxt true order_system t;
1.182 +if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
1.183 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
1.184 +
1.185 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.186 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.187 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.188 +val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
1.189 +val ctxt = Proof_Context.init_global thy;
1.190 +val t =
1.191 + TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
1.192 + \ - 1 * q_0 / 24 * 0 \<up> 4),\
1.193 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
1.194 + \ - 1 * q_0 / 24 * L \<up> 4)]";
1.195 +val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
1.196 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.197 + "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
1.198 + "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
1.199 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
1.200 +
1.201 +val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.202 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.203 + "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
1.204 + "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
1.205 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
1.206 +
1.207 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
1.208 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.209 + "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
1.210 + "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
1.211 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
1.212 +
1.213 +val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
1.214 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
1.215 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
1.216 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
1.217 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
1.218 +
1.219 +val xxx = rewrite_set_ ctxt true order_system t;
1.220 +if is_none xxx
1.221 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
1.222 +
1.223 +
1.224 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.225 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.226 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.227 +val e1__ = TermC.str2term "c_2 = 77";
1.228 +val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
1.229 +val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.230 + (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.231 +val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
1.232 +if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
1.233 +else error "eqsystem.sml top_down_substitution,2x2] subst";
1.234 +
1.235 +val SOME (e2__,_) =
1.236 + rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
1.237 +if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
1.238 +else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
1.239 +
1.240 +val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
1.241 +if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
1.242 +else error "eqsystem.sml top_down_substitution,2x2] isolate";
1.243 +
1.244 +val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
1.245 +val SOME (t,_) = rewrite_set_ ctxt true order_system t;
1.246 +if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
1.247 +else error "eqsystem.sml top_down_substitution,2x2] order_system";
1.248 +
1.249 +if not (ord_simplify_System
1.250 + false thy []
1.251 + (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
1.252 + TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
1.253 +then () else error "eqsystem.sml, order_result rew_ord";
1.254 +
1.255 +
1.256 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.257 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.258 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.259 +(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
1.260 +val t = TermC.str2term (
1.261 + "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
1.262 + "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
1.263 + "c + c_2 + c_3 + c_4 = 0, " ^
1.264 + "c_2 + c_3 + c_4 = 0]");
1.265 +val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
1.266 + (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
1.267 + (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
1.268 + (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
1.269 +val SOME (t, _) =
1.270 + rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.271 +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.272 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
1.273 +
1.274 +val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
1.275 +if UnparseC.term t = "[c_4 = 0, \
1.276 + \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
1.277 + \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
1.278 +then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
1.279 +
1.280 +val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.281 +if UnparseC.term t = "[c_4 = 0,\
1.282 + \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
1.283 + \ c + (c_2 + (c_3 + c_4)) = 0,\n\
1.284 + \ c_2 + (c_3 + c_4) = 0]"
1.285 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
1.286 +
1.287 +val SOME (t, _) = rewrite_set_ ctxt true order_system t;
1.288 +if UnparseC.term t = "[c_4 = 0,\
1.289 + \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
1.290 + \ c_2 + (c_3 + c_4) = 0,\n\
1.291 + \ c + (c_2 + (c_3 + c_4)) = 0]"
1.292 +then () else error "eqsystem.sml rewrite in 4x4 order_system";
1.293 +
1.294 +\<close> ML \<open>
1.295 +"----------- refine [linear,system]-------------------------------";
1.296 +"----------- refine [linear,system]-------------------------------";
1.297 +"----------- refine [linear,system]-------------------------------";
1.298 +val fmz =
1.299 + ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
1.300 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
1.301 + "solveForVars [c, c_2]", "solution LL"];
1.302 +
1.303 +(*WN120313 in "solution L" above "Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]" caused an error...*)
1.304 +"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
1.305 +"~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
1.306 + ((rev o tl) pblID, fmz, [(*match list*)],
1.307 + ((Store.Node ("LINEAR", [Problem.from_store_PIDE ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
1.308 + val {thy, ppc, where_, prls, ...} = py ;
1.309 +"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
1.310 + val ctxt = Proof_Context.init_global thy;
1.311 +"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
1.312 + fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
1.313 + (_, _::_) => (Free (v,T)::get_vars vs)
1.314 + | (_, [] ) => get_vars vs) (*filter out nums as long as
1.315 + we have Free ("123",_)*)
1.316 + | get_vars [] = [];
1.317 + t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
1.318 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
1.319 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
1.320 +val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
1.321 +val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
1.322 +val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
1.323 +val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
1.324 + val t = nth 2 fmz; t = "solveForVars [c, c_2]";
1.325 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
1.326 +val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
1.327 + val t = nth 3 fmz; t = "solution LL";
1.328 + (*(Syntax.read_term ctxt t);
1.329 +Type unification failed: Clash of types "real" and "_ list"
1.330 +Type error in application: incompatible operand type
1.331 +
1.332 +Operator: solution :: bool list \<Rightarrow> toreall
1.333 +Operand: L :: real ========== L was already present in equalities ========== *)
1.334 +
1.335 +"===== case 1 =====";
1.336 +val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
1.337 +case matches of
1.338 + [M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
1.339 + M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch ! GOON !*)
1.340 + M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
1.341 + M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
1.342 + {Find = [Correct "solution LL"], With = [], (**)
1.343 + Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.344 + Correct "solveForVars [c, c_2]"],
1.345 + Where = [],
1.346 + Relate = []})] => ()
1.347 +| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
1.348 +
1.349 +"===== case 2 =====";
1.350 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
1.351 + "solveForVars [c, c_2]", "solution LL"];
1.352 +val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
1.353 +case matches of [_,_,
1.354 + M_Match.Matches
1.355 + (["triangular", "2x2", "LINEAR", "system"],
1.356 + {Find = [Correct "solution LL"],
1.357 + With = [],
1.358 + Given =
1.359 + [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
1.360 + Correct "solveForVars [c, c_2]"],
1.361 + Where = [Correct
1.362 + "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
1.363 + Correct
1.364 + "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
1.365 + Relate = []})] => ()
1.366 +| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
1.367 +
1.368 +(*WN051014-----------------------------------------------------------------------------------\\
1.369 + the above 'val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]'
1.370 + didn't work anymore; we investigated in these steps:*)
1.371 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
1.372 + "solveForVars [c, c_2]", "solution LL"];
1.373 +val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
1.374 +(*... resulted in
1.375 + False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
1.376 + [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
1.377 +val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
1.378 + "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
1.379 +
1.380 +val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
1.381 +(*found:...
1.382 +## try thm: NTH_CONS
1.383 +### eval asms: 1 < 2 + - 1
1.384 +==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
1.385 + nth_ (2 + - 1 + - 1) []
1.386 +#### rls: erls_prls_triangular on: 1 < 2 + - 1
1.387 +##### try calc: op <'
1.388 +### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
1.389 +
1.390 +... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
1.391 +(*--------------------------------------------------------------------------------------------//*)
1.392 +
1.393 +
1.394 +"===== case 3: relaxed preconditions for triangular system =====";
1.395 +val fmz = ["equalities [L * q_0 = c, \
1.396 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
1.397 + \ 0 = c_4, \
1.398 + \ 0 = c_3]",
1.399 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
1.400 +(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
1.401 +probably exn thrown by fun declare_constraints
1.402 +/-------------------------------------------------------\
1.403 +Type unification failed
1.404 +Type error in application: incompatible operand type
1.405 +
1.406 +Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
1.407 +Operand: [c_4] :: 'b list
1.408 +\-------------------------------------------------------/
1.409 +val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
1.410 +case TermC.matches of
1.411 + [M_Match.Matches (["LINEAR", "system"], _),
1.412 + M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
1.413 + M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
1.414 + M_Match.Matches (["4x4", "LINEAR", "system"], _),
1.415 + M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
1.416 + M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
1.417 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
1.418 +(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
1.419 +
1.420 +"===== case 4 =====";
1.421 +val fmz = ["equalities [L * q_0 = c, \
1.422 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
1.423 + \ 0 = c_3, \
1.424 + \ 0 = c_4]",
1.425 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
1.426 +val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
1.427 +case TermC.matches of
1.428 + [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
1.429 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
1.430 +val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
1.431 +============ inhibit exn WN120314 ==============================================*)
1.432 +
1.433 +\<close> ML \<open>
1.434 +"----------- Refine.refine [2x2,linear,system] search error--------------";
1.435 +"----------- Refine.refine [2x2,linear,system] search error--------------";
1.436 +"----------- Refine.refine [2x2,linear,system] search error--------------";
1.437 +(*didn't go into ["2x2", "LINEAR", "system"];
1.438 + we investigated in these steps:*)
1.439 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.440 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.441 + "solveForVars [c, c_2]", "solution LL"];
1.442 +val matches = Refine.refine_PIDE @{context} fmz ["2x2", "LINEAR", "system"];
1.443 +(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
1.444 +(*brought: 'False "length_ es_ = 2"'*)
1.445 +
1.446 +(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
1.447 +(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
1.448 + (rev ["LINEAR", "system"], fmz, [(*match list*)],
1.449 + ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
1.450 + *)
1.451 +> show_types:=true; UnparseC.term (hd where_); show_types:=false;
1.452 +val it = "length_ (es_::real list) = (2::real)" : string
1.453 +
1.454 +=========================================================================\
1.455 +-------fun Problem.prep_input
1.456 +(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
1.457 + ev:rls, ca: string option, metIDs:metID list)) =
1.458 + (EqSystem.thy, (["system"],
1.459 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.460 + ("#Find" ,["solution ss___"](*___ is copy-named*))
1.461 + ],
1.462 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.463 + SOME "solveSystem es_ v_s",
1.464 + []));
1.465 + *)
1.466 +> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
1.467 +val equalities_es_ = "equalities es_" : string
1.468 +> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
1.469 +> show_types:=true; UnparseC.term ii; show_types:=false;
1.470 +val it = "es_::bool list" : string
1.471 +~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.472 +
1.473 +> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
1.474 +> show_types:=true; UnparseC.term (hd where_); show_types:=false;
1.475 +
1.476 +=========================================================================/
1.477 +
1.478 +-----fun refin' ff:
1.479 +> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
1.480 +[
1.481 +(1 ,[1] ,true ,#Given ,Cor equalities
1.482 + [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
1.483 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
1.484 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
1.485 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.486 +(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
1.487 +
1.488 +> (writeln o pres2str) pre';
1.489 +[
1.490 +(false, length_ es_ = 2),
1.491 +(true, length_ [c, c_2] = 2)]
1.492 +
1.493 +----- fun match_oris':
1.494 +> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
1.495 +> (writeln o pres2str) pre';
1.496 +..as in refin'
1.497 +
1.498 +----- fun check in Pre_Conds.
1.499 +> (writeln o env2str) env;
1.500 +["
1.501 +(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
1.502 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
1.503 +(v_s, [c, c_2])", "
1.504 +(ss___, L)"]
1.505 +
1.506 +> val es_ = (fst o hd) env;
1.507 +val es_ = Free ("es_", "bool List.list") : Term.term
1.508 +
1.509 +> val pre1 = hd pres;
1.510 +TermC.atomty pre1;
1.511 +***
1.512 +*** Const (op =, [real, real] => bool)
1.513 +*** . Const (ListG.length_, real list => real)
1.514 +*** . . Free (es_, real list)
1.515 +~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
1.516 +*** . Free (2, real)
1.517 +***
1.518 +
1.519 +THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
1.520 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.521 +*)
1.522 +
1.523 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.524 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.525 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.526 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.527 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.528 + "solveForVars [c, c_2]", "solution LL"];
1.529 +val (dI',pI',mI') =
1.530 + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
1.531 + ["EqSystem", "normalise", "2x2"]);
1.532 +val p = e_pos'; val c = [];
1.533 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.534 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.535 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.536 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.537 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.538 +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
1.539 + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
1.540 +
1.541 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.542 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.543 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
1.544 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.545 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.546 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.547 +case nxt of
1.548 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
1.549 + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
1.550 +
1.551 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.552 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.553 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.554 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.555 +case nxt of
1.556 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
1.557 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
1.558 +
1.559 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.560 +val PblObj {probl,...} = get_obj I pt [5];
1.561 + (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
1.562 +(*[
1.563 +(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
1.564 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.565 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
1.566 +*)
1.567 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.568 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.569 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.570 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.571 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.572 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.573 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.574 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.575 +case nxt of
1.576 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
1.577 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
1.578 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.579 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.580 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
1.581 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
1.582 +case nxt of
1.583 + (End_Proof') => ()
1.584 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
1.585 \<close> ML \<open>
1.586 \<close> ML \<open>
1.587 \<close>