1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Sun Oct 09 09:01:29 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Oct 19 10:43:04 2022 +0200
1.3 @@ -3,29 +3,27 @@
1.4 (c) due to copyright terms
1.5 *)
1.6
1.7 -"-----------------------------------------------------------------";
1.8 -"table of contents -----------------------------------------------";
1.9 -"-----------------------------------------------------------------";
1.10 -"----------- occur_exactly_in ------------------------------------";
1.11 -"----------- problems --------------------------------------------";
1.12 -"----------- rewrite-order ord_simplify_System -------------------";
1.13 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.14 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.15 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.16 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.17 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.18 -"----------- refine [linear,system]-------------------------------";
1.19 -"----------- refine [2x2,linear,system] search error--------------";
1.20 -(*^^^--- eqsystem-1.sml #####################################################################*)
1.21 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.22 -(*^^^--- eqsystem-1a.sml #####################################################################
1.23 - vvv--- eqsystem-2.sml #####################################################################*)
1.24 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
1.25 -"----------- all systems from Biegelinie -------------------------";
1.26 -"----------- 4x4 systems from Biegelinie -------------------------";
1.27 -"-----------------------------------------------------------------";
1.28 -"-----------------------------------------------------------------";
1.29 -"-----------------------------------------------------------------";
1.30 +"-----------------------------------------------------------------------------------------------";
1.31 +"table of contents -----------------------------------------------------------------------------";
1.32 +"-----------------------------------------------------------------------------------------------";
1.33 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
1.34 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
1.35 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
1.36 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
1.37 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
1.38 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
1.39 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
1.40 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
1.41 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
1.42 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
1.43 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
1.44 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
1.45 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
1.46 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
1.47 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
1.48 +"-----------------------------------------------------------------------------------------------";
1.49 +"-----------------------------------------------------------------------------------------------";
1.50 +"-----------------------------------------------------------------------------------------------";
1.51
1.52 val thy = @{theory "EqSystem"};
1.53 val ctxt = Proof_Context.init_global thy;
1.54 @@ -176,6 +174,7 @@
1.55 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
1.56 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
1.57
1.58 +
1.59 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.60 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.61 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.62 @@ -285,6 +284,8 @@
1.63 \ c + (c_2 + (c_3 + c_4)) = 0]"
1.64 then () else error "eqsystem.sml rewrite in 4x4 order_system";
1.65
1.66 +
1.67 +
1.68 "----------- refine [linear,system]-------------------------------";
1.69 "----------- refine [linear,system]-------------------------------";
1.70 "----------- refine [linear,system]-------------------------------";
1.71 @@ -423,6 +424,8 @@
1.72 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
1.73 ============ inhibit exn WN120314 ==============================================*)
1.74
1.75 +
1.76 +
1.77 "----------- Refine.refine [2x2,linear,system] search error--------------";
1.78 "----------- Refine.refine [2x2,linear,system] search error--------------";
1.79 "----------- Refine.refine [2x2,linear,system] search error--------------";
1.80 @@ -512,11 +515,12 @@
1.81 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.82 *)
1.83
1.84 +
1.85 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.86 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.87 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.88 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.89 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.90 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
1.91 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.92 "solveForVars [c, c_2]", "solution LL"];
1.93 val (dI',pI',mI') =
1.94 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
1.95 @@ -532,7 +536,7 @@
1.96
1.97 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.98 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.99 -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.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.101 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.102 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.103 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.104 @@ -549,13 +553,6 @@
1.105 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
1.106
1.107 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.108 -val PblObj {probl,...} = get_obj I pt [5];
1.109 - (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
1.110 -(*[
1.111 -(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.112 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.113 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
1.114 -*)
1.115 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.116 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.117 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.118 @@ -569,8 +566,33 @@
1.119 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
1.120 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.121 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.122 +(* final test ... ----------------------------------------------------------------------------*)
1.123 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
1.124 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
1.125 +
1.126 case nxt of
1.127 (End_Proof') => ()
1.128 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
1.129 +
1.130 +Test_Tool.show_pt pt (*[
1.131 +(([], Frm), solveSystem
1.132 + [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
1.133 + [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
1.134 + [[c], [c_2]]),
1.135 +(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
1.136 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
1.137 +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
1.138 +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
1.139 +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
1.140 +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
1.141 +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
1.142 +(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
1.143 +(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
1.144 +(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
1.145 +(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
1.146 +(([5, 4], Res), c = L * q_0 / 2),
1.147 +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
1.148 +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.149 +(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.150 +(([], Res), [c = L * q_0 / 2, c_2 = 0])]
1.151 +*)