walther@60347: (* Title: Knowledge/eqsystem-2.sml
walther@60347:    author: Walther Neuper 050826,
walther@60347:    (c) due to copyright terms
walther@60347: *)
walther@60347: 
walther@60347: "-----------------------------------------------------------------";
walther@60347: "table of contents -----------------------------------------------";
walther@60347: "-----------------------------------------------------------------";
walther@60347: "----------- occur_exactly_in ------------------------------------";
walther@60347: "----------- problems --------------------------------------------";
walther@60347: "----------- rewrite-order ord_simplify_System -------------------";
walther@60347: "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
walther@60347: "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
walther@60347: "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
walther@60347: "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
walther@60347: "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
walther@60347: "----------- refine [linear,system]-------------------------------";
walther@60347: "----------- refine [2x2,linear,system] search error--------------";
walther@60347: "----------- me [EqSystem,normalise,2x2] -------------------------";
walther@60347: (*^^^--- eqsystem-1.sml ######### together exceed resources here, but not in Test_Isac.thy #####
walther@60347:   vvv--- eqsystem-2.sml ######### together exceed resources here, but not in Test_Isac.thy #####*)
walther@60347: "----------- me [linear,system] ..normalise..top_down_sub..-------";
walther@60347: "----------- all systems from Biegelinie -------------------------";
walther@60347: "----------- 4x4 systems from Biegelinie -------------------------";
walther@60347: "-----------------------------------------------------------------";
walther@60347: "-----------------------------------------------------------------";
walther@60347: "-----------------------------------------------------------------";
walther@60347: 
walther@60347: val thy = @{theory "EqSystem"};
walther@60347: val ctxt = Proof_Context.init_global thy;
walther@60347: 
walther@60347: "----------- me [linear,system] ..normalise..top_down_sub..-------";
walther@60347: "----------- me [linear,system] ..normalise..top_down_sub..-------";
walther@60347: "----------- me [linear,system] ..normalise..top_down_sub..-------";
walther@60347: val fmz = 
walther@60347:     ["equalities\
walther@60347:      \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +                \
walther@60347:      \                                            - 1 * q_0 / 24 * 0 \<up> 4),\
walther@60347:      \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +                \
walther@60347:      \                                            - 1 * q_0 / 24 * L \<up> 4)]",
walther@60347:      "solveForVars [c, c_2]", "solution LL"];
walther@60347: val (dI',pI',mI') =
walther@60347:   ("Biegelinie",["LINEAR", "system"], ["no_met"]);
walther@60347: val p = e_pos'; val c = []; 
walther@60347: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
walther@60347: 	  | _ => error "eqsystem.sml [linear,system] specify b";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
walther@60347:   "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
walther@60347:   "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
walther@60347: then () else error "eqsystem.sml me simpl. before SubProblem b";
walther@60347: case nxt of
walther@60347:     (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
walther@60347:   | _ => error "eqsystem.sml me [linear,system] SubProblem b";
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: case nxt of
walther@60347:     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
walther@60347:   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val PblObj {probl,...} = get_obj I pt [5];
walther@60360:     (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
walther@60347: (*[
walther@60347: (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]])),
walther@60347: (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
walther@60347: (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
walther@60347: *)
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: case nxt of
walther@60347:     (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
walther@60347:   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: 
walther@60347: if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
walther@60347:   "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
walther@60347:   "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
walther@60347: then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
walther@60347: case nxt of
walther@60347:     (End_Proof') => ()
walther@60347:   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
walther@60347: 
walther@60347: 
walther@60347: "----------- all systems from Biegelinie -------------------------";
walther@60347: "----------- all systems from Biegelinie -------------------------";
walther@60347: "----------- all systems from Biegelinie -------------------------";
walther@60347: val thy = @{theory Isac_Knowledge}
walther@60347: val subst = 
walther@60347:   [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
walther@60347: 	(TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")]; 
walther@60347: 
walther@60347: "------- Bsp 7.27";
walther@60347: reset_states ();
walther@60347: CalcTree [(
walther@60347:   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
walther@60347: 	  "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
walther@60347: 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: ##7.27##          ordered           substs
walther@60347:           c_4       c_2           
walther@60347: c c_2 c_3 c_4     c c_2             1->2: c
walther@60347:   c_2                       c_4	  
walther@60347: c c_2             c c_2 c_3 c_4     [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
walther@60347: val t = TermC.str2term
walther@60347:   ("[0 = c_4, " ^
walther@60347:   "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), " ^
walther@60347:   "0 = c_2, " ^
walther@60347:   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;
walther@60347: if UnparseC.term t =
walther@60347: "[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]"
walther@60347: then () else error "Bsp 7.27";
walther@60347: 
walther@60347: "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
walther@60347: val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
Walther@60500: val NONE = rewrite_set_ ctxt false norm_Rational t;
walther@60347: val SOME (t,_) = 
Walther@60500:     rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
walther@60347: if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
walther@60347: then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
walther@60347: 
walther@60347: "--- isolate_bdvs_4x4";
walther@60347: (*
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
walther@60347: UnparseC.term t;
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;
walther@60347: UnparseC.term t;
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt false order_system t;
walther@60347: UnparseC.term t;
walther@60347: *)
walther@60347: 
walther@60347: "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
walther@60347: reset_states ();
walther@60347: CalcTree [((*WN130908  <ERROR> error in kernel </ERROR>*)
walther@60347:   ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
walther@60347: 	    "Biegelinie y",
walther@60347: 	    "Randbedingungen [y L = 0, y' L = 0]",
walther@60347: 	    "FunktionsVariable x"],
walther@60347: 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
walther@60347: 	    ["Biegelinien", "AusMomentenlinie"]))];
walther@60347: (*
walther@60347: moveActiveRoot 1;
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: *)
walther@60347: 
walther@60347: "------- Bsp 7.69";
walther@60347: reset_states ();
walther@60347: CalcTree [(
walther@60347:   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
walther@60347: 	  "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
walther@60347: 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: ##7.69##          ordered           subst                   2x2
walther@60347:           c_4           c_3         
walther@60347: c c_2 c_3 c_4     c c_2 c_3	    1:c_3 -> 2:c c_2        2:         c c_2
walther@60347:       c_3                   c_4	 			   
walther@60347: 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*)
walther@60347: val t = TermC.str2term 
walther@60347:   ("[0 = c_4 + 0 / (- 1 * EI), " ^
walther@60347:   "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), " ^
walther@60347:   "0 = c_3 + 0 / (- 1 * EI), " ^
walther@60347:   "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
walther@60347: 
walther@60347: "------- Bsp 7.70";
walther@60347: reset_states ();
walther@60347: CalcTree [(
walther@60347:   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
walther@60347: 	  "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
walther@60347: 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: ##7.70##        |subst
walther@60347: c		|
walther@60347: c c_2           |1:c -> 2:c_2
walther@60347:       c_3	|
walther@60347:           c_4   |            STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
walther@60347: 
walther@60347: "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
walther@60347: val t = TermC.str2term
walther@60347:   ("[L * q_0 = c, " ^
walther@60347:   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
walther@60347:   "0 = c_4, " ^
walther@60347:   "0 = c_3]");
Walther@60509: val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
Walther@60509: val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
Walther@60509: val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
walther@60347: if UnparseC.term t = 
walther@60347:   "[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]"
walther@60347: then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
walther@60347: 
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
walther@60347: 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]"
walther@60347: then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
walther@60347: 
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
walther@60347: if UnparseC.term t =
walther@60347:    "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^ 
walther@60347:    " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
walther@60347: then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
walther@60347: 
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
walther@60395: if UnparseC.term t =
walther@60395:   "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
walther@60347: then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
walther@60347: 
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt false order_system t;
walther@60395: if UnparseC.term t =
walther@60395:   "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
walther@60347: then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
walther@60347: 
walther@60347: "----- 7.70 with met normalise: ";
walther@60347: val fmz = ["equalities" ^
walther@60347:   "[L * q_0 = c, " ^
walther@60347:   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
walther@60347:   "0 = c_4, " ^
walther@60347:   "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
walther@60347: val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
walther@60347: val p = e_pos'; val c = [];
walther@60347: 
walther@60347: (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
walther@60347:   in next but one test below the same type error.
walther@60347: /-------------------------------------------------------\
walther@60347: Type unification failed
walther@60347: Type error in application: incompatible operand type
walther@60347: 
walther@60347: Operator:  op # c_3 :: 'a list \<Rightarrow> 'a list
walther@60347: Operand:   [c_4] :: 'b list
walther@60347: \-------------------------------------------------------/
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
walther@60347: 	  | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: 
walther@60347: "----- outcommented before Isabelle2002 --> 2011 -------------------------";
walther@60347: (*-----------------------------------vvvWN080102 Exception- Match raised 
walther@60347:   since associate Rewrite .. Rewrite_Set
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]" 
walther@60347: then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
walther@60347: --------------------------------------------------------------------------*)
walther@60347: ============ inhibit exn WN120314 ==============================================*)
walther@60347: 
walther@60347: "----- 7.70 with met top_down_: me";
walther@60347: val fmz = [
walther@60347:   "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]",
walther@60347: 	"solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
walther@60347: val (dI',pI',mI') =
walther@60347:   ("Biegelinie",["LINEAR", "system"],["no_met"]);
walther@60347: val p = e_pos'; val c = []; 
walther@60347: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
walther@60347: 	  | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: if p = ([], Res) andalso
walther@60347: (*           "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
walther@60347:    f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
walther@60347: then () else error "eqsystem.sml: 7.70 with met top_down_: me";
walther@60347: 
walther@60347: "------- Bsp 7.71";
walther@60347: reset_states ();
walther@60347: CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
walther@60347: 	     "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
walther@60347: 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
walther@60347: 	     "AbleitungBiegelinie dy"],
walther@60347: 	    ("Biegelinie", ["Biegelinien"],
walther@60347: 	     ["IntegrierenUndKonstanteBestimmen2"] ))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: ##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal
walther@60347: c c_2          |c c_2	      |1'		      |1': c c_2 |
walther@60347:           c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |
walther@60347: c c_2 c_3 c_4  |          c_4 |3'                     |	         |
walther@60347:       c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)
walther@60347: val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
walther@60347: \ 0 = c_4 + 0 / (- 1 * EI),                            \
walther@60347: \ 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),\
walther@60347: \ 0 = c_3 + 0 / (- 1 * EI)]";
walther@60347: 
walther@60347: "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
walther@60347: reset_states ();
walther@60347: CalcTree [(["Traegerlaenge L",
walther@60347: 	    "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
walther@60347: 	    "Biegelinie y",
walther@60347: 	    "Randbedingungen [y 0 = (0::real), y L = 0]",
walther@60347: 	    "FunktionsVariable x"],
walther@60347: 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
walther@60347: 	    ["Biegelinien", "AusMomentenlinie"]))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: *)
walther@60347: 
walther@60347: "------- Bsp 7.72b";
walther@60347: reset_states ();
walther@60347: CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
walther@60347: 	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
walther@60347: 	    "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
walther@60347: 	    "AbleitungBiegelinie dy"],
walther@60347: 	   ("Biegelinie", ["Biegelinien"],
walther@60347: 	    ["IntegrierenUndKonstanteBestimmen2"] ))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: ##7.72b##      |ord. |subst.singles         |ord.triang.
walther@60347:   c_2          |     |			    |c_2  
walther@60347: c c_2	       |     |1:c_2 -> 2':c	    |c_2 c
walther@60347:           c_4  |     |			    |
walther@60347: c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
walther@60347: val t = TermC.str2term"[0 = c_2,                                            \
walther@60347: \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
walther@60347: \ 0 = c_4 + 0 / (- 1 * EI),                            \
walther@60347: \ 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)]";
walther@60347: 
walther@60347: "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
walther@60347: reset_states ();
walther@60347: CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
walther@60347: 	    "Biegelinie y",
walther@60347: 	    "Randbedingungen [y L = 0, y' L = 0]",
walther@60347: 	    "FunktionsVariable x"],
walther@60347: 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
walther@60347: 	    ["Biegelinien", "AusMomentenlinie"]))];
walther@60347: moveActiveRoot 1;
walther@60347: (*
walther@60347: LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
walther@60347: *)
walther@60347: 
walther@60347: "----------- 4x4 systems from Biegelinie -------------------------";
walther@60347: "----------- 4x4 systems from Biegelinie -------------------------";
walther@60347: "----------- 4x4 systems from Biegelinie -------------------------";
walther@60347: (*STOPPED.WN08?? replace this test with 7.70 *)
walther@60347: "----- Bsp 7.27";
walther@60347: val fmz = ["equalities \
walther@60347: 	   \[0 = c_4,                           \
walther@60347: 	   \ 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),                                       \
walther@60347: 	   \ 0 = c_2,                                           \
walther@60347: 	   \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]", 
walther@60347: 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
walther@60347: val (dI',pI',mI') =
walther@60347:   ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
walther@60347:    ["EqSystem", "normalise", "4x4"]);
walther@60347: val p = e_pos'; val c = []; 
walther@60347: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: "------------------------------------------- Apply_Method...";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: "[0 = c_4,                                          \
walther@60347: \ 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),                                   \
walther@60347: \ 0 = c_2,                                          \
walther@60347: \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
walther@60347: (*vvvWN080102 Exception- Match raised 
walther@60347:   since associate Rewrite .. Rewrite_Set
walther@60347: "------------------------------------------- simplify_System_parenthesized...";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: "[0 = c_4,                                  \
walther@60347: \ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) +     \
walther@60347: \     (4 * L \<up> 3 * c / (- 24 * EI) +       \
walther@60347: \     (12 * L \<up> 2 * c_2 / (- 24 * EI) +    \
walther@60347: \     (L * c_3 + c_4))),                    \
walther@60347: \ 0 = c_2,                                  \
walther@60347: \ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
walther@60347: (*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
walther@60347: "------------------------------------------- isolate_bdvs...";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: "[c_4 = 0,\
walther@60347: \ 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),\
walther@60347: \ c_2 = 0, \
walther@60347: \ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
walther@60347: 
walther@60347: ---------------------------------------------------------------------*)