1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Tue Aug 03 19:16:27 2021 +0200
1.3 @@ -0,0 +1,425 @@
1.4 +(* Title: Knowledge/eqsystem-2.sml
1.5 + author: Walther Neuper 050826,
1.6 + (c) due to copyright terms
1.7 +*)
1.8 +
1.9 +Rewrite.trace_on := false; (*true false*)
1.10 +"-----------------------------------------------------------------";
1.11 +"table of contents -----------------------------------------------";
1.12 +"-----------------------------------------------------------------";
1.13 +"----------- occur_exactly_in ------------------------------------";
1.14 +"----------- problems --------------------------------------------";
1.15 +"----------- rewrite-order ord_simplify_System -------------------";
1.16 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
1.17 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
1.18 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.19 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
1.20 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.21 +"----------- refine [linear,system]-------------------------------";
1.22 +"----------- refine [2x2,linear,system] search error--------------";
1.23 +"----------- me [EqSystem,normalise,2x2] -------------------------";
1.24 +(*^^^--- eqsystem-1.sml ######### together exceed resources here, but not in Test_Isac.thy #####
1.25 + vvv--- eqsystem-2.sml ######### together exceed resources here, but not in Test_Isac.thy #####*)
1.26 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
1.27 +"----------- all systems from Biegelinie -------------------------";
1.28 +"----------- 4x4 systems from Biegelinie -------------------------";
1.29 +"-----------------------------------------------------------------";
1.30 +"-----------------------------------------------------------------";
1.31 +"-----------------------------------------------------------------";
1.32 +
1.33 +val thy = @{theory "EqSystem"};
1.34 +val ctxt = Proof_Context.init_global thy;
1.35 +
1.36 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
1.37 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
1.38 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
1.39 +val fmz =
1.40 + ["equalities\
1.41 + \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
1.42 + \ - 1 * q_0 / 24 * 0 \<up> 4),\
1.43 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
1.44 + \ - 1 * q_0 / 24 * L \<up> 4)]",
1.45 + "solveForVars [c, c_2]", "solution LL"];
1.46 +val (dI',pI',mI') =
1.47 + ("Biegelinie",["LINEAR", "system"], ["no_met"]);
1.48 +val p = e_pos'; val c = [];
1.49 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.50 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.51 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.52 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.53 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.54 +case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
1.55 + | _ => error "eqsystem.sml [linear,system] specify b";
1.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.62 +if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
1.63 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
1.64 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
1.65 +then () else error "eqsystem.sml me simpl. before SubProblem b";
1.66 +case nxt of
1.67 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
1.68 + | _ => error "eqsystem.sml me [linear,system] SubProblem b";
1.69 +
1.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.72 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.73 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.74 +case nxt of
1.75 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
1.76 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
1.77 +
1.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.79 +val PblObj {probl,...} = get_obj I pt [5];
1.80 + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
1.81 +(*[
1.82 +(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.83 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.84 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
1.85 +*)
1.86 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.88 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.90 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.92 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.94 +case nxt of
1.95 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
1.96 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
1.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.99 +
1.100 +if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
1.101 + "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
1.102 + "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
1.103 +then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
1.104 +case nxt of
1.105 + (End_Proof') => ()
1.106 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
1.107 +
1.108 +
1.109 +"----------- all systems from Biegelinie -------------------------";
1.110 +"----------- all systems from Biegelinie -------------------------";
1.111 +"----------- all systems from Biegelinie -------------------------";
1.112 +val thy = @{theory Isac_Knowledge}
1.113 +val subst =
1.114 + [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
1.115 + (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
1.116 +
1.117 +"------- Bsp 7.27";
1.118 +reset_states ();
1.119 +CalcTree [(
1.120 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.121 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
1.122 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
1.123 +moveActiveRoot 1;
1.124 +(*
1.125 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.126 +##7.27## ordered substs
1.127 + c_4 c_2
1.128 +c c_2 c_3 c_4 c c_2 1->2: c
1.129 + c_2 c_4
1.130 +c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
1.131 +val t = TermC.str2term
1.132 + ("[0 = c_4, " ^
1.133 + "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
1.134 + "0 = c_2, " ^
1.135 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
1.136 +val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
1.137 +if UnparseC.term t =
1.138 +"[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
1.139 +then () else error "Bsp 7.27";
1.140 +
1.141 +"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
1.142 +val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
1.143 +val NONE = rewrite_set_ thy false norm_Rational t;
1.144 +val SOME (t,_) =
1.145 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.146 +if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
1.147 +then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
1.148 +
1.149 +"--- isolate_bdvs_4x4";
1.150 +(*
1.151 +val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
1.152 +UnparseC.term t;
1.153 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
1.154 +UnparseC.term t;
1.155 +val SOME (t,_) = rewrite_set_ thy false order_system t;
1.156 +UnparseC.term t;
1.157 +*)
1.158 +
1.159 +"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1.160 +reset_states ();
1.161 +CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
1.162 + ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
1.163 + "Biegelinie y",
1.164 + "Randbedingungen [y L = 0, y' L = 0]",
1.165 + "FunktionsVariable x"],
1.166 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
1.167 + ["Biegelinien", "AusMomentenlinie"]))];
1.168 +(*
1.169 +moveActiveRoot 1;
1.170 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.171 +*)
1.172 +
1.173 +"------- Bsp 7.69";
1.174 +reset_states ();
1.175 +CalcTree [(
1.176 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.177 + "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
1.178 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
1.179 +moveActiveRoot 1;
1.180 +(*
1.181 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.182 +##7.69## ordered subst 2x2
1.183 + c_4 c_3
1.184 +c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
1.185 + c_3 c_4
1.186 +c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
1.187 +val t = TermC.str2term
1.188 + ("[0 = c_4 + 0 / (- 1 * EI), " ^
1.189 + "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
1.190 + "0 = c_3 + 0 / (- 1 * EI), " ^
1.191 + "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
1.192 +
1.193 +"------- Bsp 7.70";
1.194 +reset_states ();
1.195 +CalcTree [(
1.196 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.197 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
1.198 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
1.199 +moveActiveRoot 1;
1.200 +(*
1.201 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.202 +##7.70## |subst
1.203 +c |
1.204 +c c_2 |1:c -> 2:c_2
1.205 + c_3 |
1.206 + c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
1.207 +
1.208 +"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
1.209 +val t = TermC.str2term
1.210 + ("[L * q_0 = c, " ^
1.211 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
1.212 + "0 = c_4, " ^
1.213 + "0 = c_3]");
1.214 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
1.215 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
1.216 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
1.217 +if UnparseC.term t =
1.218 + "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
1.219 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
1.220 +
1.221 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.222 +if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
1.223 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
1.224 +
1.225 +val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
1.226 +if UnparseC.term t =
1.227 + "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
1.228 + " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
1.229 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
1.230 +
1.231 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.232 +if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
1.233 + "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"*)
1.234 + "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
1.235 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
1.236 +
1.237 +val SOME (t, _) = rewrite_set_ thy false order_system t;
1.238 +if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
1.239 + "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"*)
1.240 + "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
1.241 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
1.242 +
1.243 +"----- 7.70 with met normalise: ";
1.244 +val fmz = ["equalities" ^
1.245 + "[L * q_0 = c, " ^
1.246 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
1.247 + "0 = c_4, " ^
1.248 + "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
1.249 +val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
1.250 +val p = e_pos'; val c = [];
1.251 +
1.252 +(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
1.253 + in next but one test below the same type error.
1.254 +/-------------------------------------------------------\
1.255 +Type unification failed
1.256 +Type error in application: incompatible operand type
1.257 +
1.258 +Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
1.259 +Operand: [c_4] :: 'b list
1.260 +\-------------------------------------------------------/
1.261 +
1.262 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.263 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.264 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.265 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.266 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.267 +case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
1.268 + | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
1.269 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.270 +
1.271 +"----- outcommented before Isabelle2002 --> 2011 -------------------------";
1.272 +(*-----------------------------------vvvWN080102 Exception- Match raised
1.273 + since associate Rewrite .. Rewrite_Set
1.274 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.275 +
1.276 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.277 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.278 +
1.279 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.280 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.281 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.282 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.283 +if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
1.284 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
1.285 +--------------------------------------------------------------------------*)
1.286 +============ inhibit exn WN120314 ==============================================*)
1.287 +
1.288 +"----- 7.70 with met top_down_: me";
1.289 +val fmz = [
1.290 + "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
1.291 + "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
1.292 +val (dI',pI',mI') =
1.293 + ("Biegelinie",["LINEAR", "system"],["no_met"]);
1.294 +val p = e_pos'; val c = [];
1.295 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.296 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.297 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.298 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.299 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.300 +case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
1.301 + | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
1.302 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.303 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.304 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.305 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.306 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.307 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.308 +if p = ([], Res) andalso
1.309 +(* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
1.310 + f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
1.311 +then () else error "eqsystem.sml: 7.70 with met top_down_: me";
1.312 +
1.313 +"------- Bsp 7.71";
1.314 +reset_states ();
1.315 +CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.316 + "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
1.317 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
1.318 + "AbleitungBiegelinie dy"],
1.319 + ("Biegelinie", ["Biegelinien"],
1.320 + ["IntegrierenUndKonstanteBestimmen2"] ))];
1.321 +moveActiveRoot 1;
1.322 +(*
1.323 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.324 +##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
1.325 +c c_2 |c c_2 |1' |1': c c_2 |
1.326 + c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
1.327 +c c_2 c_3 c_4 | c_4 |3' | |
1.328 + c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
1.329 +val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
1.330 +\ 0 = c_4 + 0 / (- 1 * EI), \
1.331 +\ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
1.332 +\ 0 = c_3 + 0 / (- 1 * EI)]";
1.333 +
1.334 +"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1.335 +reset_states ();
1.336 +CalcTree [(["Traegerlaenge L",
1.337 + "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
1.338 + "Biegelinie y",
1.339 + "Randbedingungen [y 0 = (0::real), y L = 0]",
1.340 + "FunktionsVariable x"],
1.341 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
1.342 + ["Biegelinien", "AusMomentenlinie"]))];
1.343 +moveActiveRoot 1;
1.344 +(*
1.345 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.346 +*)
1.347 +
1.348 +"------- Bsp 7.72b";
1.349 +reset_states ();
1.350 +CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
1.351 + "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
1.352 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
1.353 + "AbleitungBiegelinie dy"],
1.354 + ("Biegelinie", ["Biegelinien"],
1.355 + ["IntegrierenUndKonstanteBestimmen2"] ))];
1.356 +moveActiveRoot 1;
1.357 +(*
1.358 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.359 +##7.72b## |ord. |subst.singles |ord.triang.
1.360 + c_2 | | |c_2
1.361 +c c_2 | |1:c_2 -> 2':c |c_2 c
1.362 + c_4 | | |
1.363 +c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
1.364 +val t = TermC.str2term"[0 = c_2, \
1.365 +\ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
1.366 +\ 0 = c_4 + 0 / (- 1 * EI), \
1.367 +\ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
1.368 +
1.369 +"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1.370 +reset_states ();
1.371 +CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
1.372 + "Biegelinie y",
1.373 + "Randbedingungen [y L = 0, y' L = 0]",
1.374 + "FunktionsVariable x"],
1.375 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
1.376 + ["Biegelinien", "AusMomentenlinie"]))];
1.377 +moveActiveRoot 1;
1.378 +(*
1.379 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
1.380 +*)
1.381 +
1.382 +"----------- 4x4 systems from Biegelinie -------------------------";
1.383 +"----------- 4x4 systems from Biegelinie -------------------------";
1.384 +"----------- 4x4 systems from Biegelinie -------------------------";
1.385 +(*STOPPED.WN08?? replace this test with 7.70 *)
1.386 +"----- Bsp 7.27";
1.387 +val fmz = ["equalities \
1.388 + \[0 = c_4, \
1.389 + \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
1.390 + \ 0 = c_2, \
1.391 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
1.392 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
1.393 +val (dI',pI',mI') =
1.394 + ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
1.395 + ["EqSystem", "normalise", "4x4"]);
1.396 +val p = e_pos'; val c = [];
1.397 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.398 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.399 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.400 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.401 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.402 +"------------------------------------------- Apply_Method...";
1.403 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.404 +"[0 = c_4, \
1.405 +\ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
1.406 +\ 0 = c_2, \
1.407 +\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
1.408 +(*vvvWN080102 Exception- Match raised
1.409 + since associate Rewrite .. Rewrite_Set
1.410 +"------------------------------------------- simplify_System_parenthesized...";
1.411 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.412 +"[0 = c_4, \
1.413 +\ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
1.414 +\ (4 * L \<up> 3 * c / (- 24 * EI) + \
1.415 +\ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
1.416 +\ (L * c_3 + c_4))), \
1.417 +\ 0 = c_2, \
1.418 +\ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
1.419 +(*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
1.420 +"------------------------------------------- isolate_bdvs...";
1.421 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.422 +"[c_4 = 0,\
1.423 +\ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
1.424 +\ c_2 = 0, \
1.425 +\ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
1.426 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.427 +
1.428 +---------------------------------------------------------------------*)