1.1 --- a/src/sml/IsacKnowledge/EqSystem.ML Fri Sep 08 09:02:48 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML Fri Sep 08 20:33:59 2006 +0200
1.3 @@ -267,6 +267,29 @@
1.4 Thm ("", num_str )*)
1.5 ],
1.6 scr = EmptyScr};
1.7 +val isolate_bdvs_4x4 =
1.8 + Rls {id="isolate_bdvs_4x4", preconds = [],
1.9 + rew_ord = ("e_rew_ord", e_rew_ord),
1.10 + erls = append_rls "erls_isolate_bdvs_4x4" e_rls
1.11 + [(Calc ("EqSystem.occur'_exactly'_in",
1.12 + eval_occur_exactly_in
1.13 + "#eval_occur_exactly_in_"))
1.14 + ],
1.15 + srls = Erls, calc = [],
1.16 + rules = [Thm ("commute_0_equality",
1.17 + num_str commute_0_equality),
1.18 + Thm ("separate_bdvs_add", num_str separate_bdvs_add),
1.19 + Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
1.20 + Thm ("separate_bdvs_add2", num_str separate_bdvs_add2),
1.21 + Thm ("separate_bdvs_add3", num_str separate_bdvs_add3),
1.22 + Thm ("separate_bdvs_add4", num_str separate_bdvs_add4),
1.23 + (*GOON*)
1.24 + Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)(*,
1.25 + Thm ("", num_str ),
1.26 + Thm ("", num_str ),
1.27 + Thm ("", num_str )*)
1.28 + ],
1.29 + scr = EmptyScr};
1.30
1.31 (*.order the equations in a system such, that a triangular system (if any)
1.32 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.33 @@ -310,6 +333,7 @@
1.34 [("simplify_System_parenthesized", prep_rls simplify_System_parenthesized),
1.35 ("simplify_System", prep_rls simplify_System),
1.36 ("isolate_bdvs", prep_rls isolate_bdvs),
1.37 + ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4),
1.38 ("order_system", prep_rls order_system),
1.39 ("order_add_mult_System", prep_rls order_add_mult_System),
1.40 ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions),
1.41 @@ -422,6 +446,18 @@
1.42 prls_triangular,
1.43 Some "solveSystem es_ vs_",
1.44 [(*["EqSystem","triangular","4x4"]*)]));
1.45 +store_pbt
1.46 + (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_norm" [] e_pblID
1.47 + (["normalize", "4x4", "linear", "system"],
1.48 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.49 + (*length_ is checked 1 level above*)
1.50 + ("#Find" ,["solution ss___"])
1.51 + ],
1.52 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.53 + Some "solveSystem es_ vs_",
1.54 + [["EqSystem","normalize","4x4"]]));
1.55 +
1.56 +
1.57 show_ptyps();
1.58
1.59
1.60 @@ -525,6 +561,54 @@
1.61 \ in (SubProblem (EqSystem_,[linear,system],[no_met]) \
1.62 \ [bool_list_ es__, real_list_ vs_]))"
1.63 ));
1.64 +
1.65 +(*this is for nth_ only*)
1.66 +val srls = Rls {id="srls_normalize_4x4",
1.67 + preconds = [],
1.68 + rew_ord = ("termlessI",termlessI),
1.69 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.70 + [(*for asm in nth_Cons_ ...*)
1.71 + Calc ("op <",eval_equ "#less_"),
1.72 + (*2nd nth_Cons_ pushes n+-1 into asms*)
1.73 + Calc("op +", eval_binop "#add_")
1.74 + ],
1.75 + srls = Erls, calc = [],
1.76 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.77 + Calc("op +", eval_binop "#add_"),
1.78 + Thm ("nth_Nil_",num_str nth_Nil_)],
1.79 + scr = EmptyScr};
1.80 +store_met
1.81 + (prep_met EqSystem.thy "met_eqsys_norm_4x4" [] e_metID
1.82 + (["EqSystem","normalize","4x4"],
1.83 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.84 + ("#Find" ,["solution ss___"])],
1.85 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.86 + srls = append_rls "srls_normalize_4x4" e_rls
1.87 + [Thm ("hd_thm",num_str hd_thm),
1.88 + Thm ("tl_Cons",num_str tl_Cons),
1.89 + Thm ("tl_Nil",num_str tl_Nil)
1.90 + ],
1.91 + prls = Erls, crls = Erls, nrls = Erls},
1.92 +(*@@@@@@ TODO, vvv just copied from 2x2 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.93 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.94 +\ (let es__ = \
1.95 +\ ((Try (Rewrite_Set norm_Rational False)) @@ \
1.96 +\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.97 +\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.98 +\ simplify_System_parenthesized False)) @@ \
1.99 +\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.100 +\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.101 +\ isolate_bdvs_4x4 False)) @@ \
1.102 +\ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
1.103 +\ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
1.104 +\ simplify_System_parenthesized False)) @@ \
1.105 +\ (Try (Rewrite_Set order_system False))) es_ \
1.106 +\ in (SubProblem (EqSystem_,[linear,system],[no_met]) \
1.107 +\ [bool_list_ es__, real_list_ vs_]))"
1.108 +));
1.109 +
1.110 +
1.111 +
1.112 show_mets();
1.113
1.114 (*
2.1 --- a/src/sml/IsacKnowledge/EqSystem.thy Fri Sep 08 09:02:48 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/EqSystem.thy Fri Sep 08 20:33:59 2006 +0200
2.3 @@ -42,11 +42,24 @@
2.4 separate_bdvs_add
2.5 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.6 \ ==> (a + b = c) = (b = c + -1*a)"
2.7 + separate_bdvs_add1
2.8 + "[| [bdv_1] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.9 + \ ==> (a + b = c) = (b = c + -1*a)"
2.10 + separate_bdvs_add2
2.11 + "[| [bdv_2] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.12 + \ ==> (a + b = c) = (b = c + -1*a)"
2.13 + separate_bdvs_add3
2.14 + "[| [bdv_3] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.15 + \ ==> (a + b = c) = (b = c + -1*a)"
2.16 + separate_bdvs_add4
2.17 + "[| [bdv_4] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
2.18 + \ ==> (a + b = c) = (b = c + -1*a)"
2.19 +
2.20 separate_bdvs_mult
2.21 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\
2.22 \ ==>(a * b = c) = (b = c / a)"
2.23
2.24 - (*require rew_ord for termination, eg. ord_simplify_Integral;
2.25 + (*requires rew_ord for termination, eg. ord_simplify_Integral;
2.26 works for lists of any length, interestingly !?!*)
2.27 order_system_NxN "[a,b] = [b,a]"
2.28
3.1 --- a/src/sml/ME/solve.sml Fri Sep 08 09:02:48 2006 +0200
3.2 +++ b/src/sml/ME/solve.sml Fri Sep 08 20:33:59 2006 +0200
3.3 @@ -421,8 +421,8 @@
3.4 (* val (ptp as (pt,pos as (p,p_))) = ptp';
3.5 val (ptp as (pt, pos as (p,p_))) = ptp'';
3.6 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
3.7 + val (ptp as (pt, pos as (p,p_))) = (pt, pos);
3.8 val (ptp as (pt, pos as (p,p_))) = ptp;
3.9 - val (ptp as (pt, pos as (p,p_))) = (pt, pos);
3.10 *)
3.11 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
3.12 if e_metID = get_obj g_metID pt (par_pblobj pt p)
3.13 @@ -457,12 +457,8 @@
3.14 | autoord CompleteToSubpbl = 4
3.15 | autoord CompleteSubpbl = 5
3.16 | autoord CompleteCalc = 6;
3.17 -(* val ptp as (_, p) = ptp;
3.18 - val ptp as (_, p) = (pt, pos); val auto = CompleteSubpbl;
3.19 - val (auto, ptp as (_, p)) = (CompleteSubpbl, (pt', pos'));
3.20
3.21 - val (c, (ptp as (_, p))) = ((c@c'), ptp);
3.22 - val (auto, c, (ptp as (_, p))) = (CompleteSubpbl, [], (pt', pos'));
3.23 +(* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);
3.24 *)
3.25 fun complete_solve auto c (ptp as (_, p): ptree * pos') =
3.26 if p = ([], Res) then ("end-of-calculation", [], ptp) else
3.27 @@ -496,6 +492,31 @@
3.28 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate))
3.29 e_istate ptp;
3.30 in complete_solve auto (c@c') ptp end;
3.31 +(*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.32 +fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
3.33 + if p = ([], Res) then ("end-of-calculation", [], ptp) else
3.34 + if p_ mem [Pbl, Met]
3.35 + then let val ptp = all_modspec ptp
3.36 + val (_, c', ptp) = all_solve auto c ptp
3.37 + in complete_solve auto (c@c') ptp end
3.38 + else case nxt_solve_ ptp of
3.39 + ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
3.40 + if autoord auto < 5 then ("ok", c@c', ptp)
3.41 + else let val ptp = all_modspec ptp'
3.42 + val (_, c'', ptp) = all_solve auto (c@c') ptp
3.43 + in complete_solve auto (c@c'@c'') ptp end
3.44 + | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
3.45 + if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
3.46 + else complete_solve auto (c@c') ptp'
3.47 + | ((End_Detail, _, _)::_, c', ptp') =>
3.48 + if autoord auto < 6 then ("ok", c@c', ptp')
3.49 + else complete_solve auto (c@c') ptp'
3.50 + | (_, c', ptp') => complete_solve auto (c@c') ptp'
3.51 +and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
3.52 + let val (_,_,mI) = get_obj g_spec pt p
3.53 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate))
3.54 + e_istate ptp
3.55 + in complete_solve auto (c@c') ptp end;
3.56
3.57 (*.aux.fun for detailrls with Rrls, reverse rewriting.*)
3.58 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
4.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Fri Sep 08 09:02:48 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Fri Sep 08 20:33:59 2006 +0200
4.3 @@ -877,7 +877,7 @@
4.4 (*---vvv-NOTok--------------------------------------------------------------*)
4.5
4.6
4.7 -"----- met [Biegelinien,ausBelastung] in IntegrierenUndKonstanteBestimmen2";
4.8 +"----- Bsp 7.27 with me";
4.9 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.10 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
4.11 "FunktionsVariable x"];
4.12 @@ -911,6 +911,20 @@
4.13 "further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
4.14 \ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
4.15
4.16 +"----- Bsp 7.27 with autoCalculate";
4.17 +states:=[];
4.18 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.19 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
4.20 + "FunktionsVariable x"],
4.21 + ("Biegelinie.thy", ["Biegelinien"],
4.22 + ["IntegrierenUndKonstanteBestimmen2"]))];
4.23 +moveActiveRoot 1;
4.24 +trace_script := true;
4.25 +autoCalculate 1 CompleteCalcHead;val ((pt,_),_) = get_calc 1;show_pt pt;
4.26 +(*
4.27 +autoCalculate 1 CompleteCalc;
4.28 +*)
4.29 +trace_script := false;
4.30
4.31
4.32 "----------- investigate normalforms in biegelinien --------------";
5.1 --- a/src/smltest/IsacKnowledge/diffapp.sml Fri Sep 08 09:02:48 2006 +0200
5.2 +++ b/src/smltest/IsacKnowledge/diffapp.sml Fri Sep 08 20:33:59 2006 +0200
5.3 @@ -371,7 +371,7 @@
5.4 Error' (Error_ "Refine_Tacitly [\"univariate\",\"equation\"] not applicable")*)
5.5
5.6
5.7 -(*----GOON.15.5.03 run scripts for maximum-example: univariate equation ?!?
5.8 +(*----postponed.15.5.03 run scripts for maximum-example: univariate equation
5.9
5.10 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
5.11
6.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml Fri Sep 08 09:02:48 2006 +0200
6.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Fri Sep 08 20:33:59 2006 +0200
6.3 @@ -26,6 +26,7 @@
6.4 "----------- me [EqSystem,normalize,2x2] -------------------------";
6.5 "----------- me [linear,system] ..normalize..top_down_sub..-------";
6.6 "----------- all systems from Biegelinie -------------------------";
6.7 +"----------- 4x4 systems from Biegelinie -------------------------";
6.8 "-----------------------------------------------------------------";
6.9 "-----------------------------------------------------------------";
6.10 "-----------------------------------------------------------------";
6.11 @@ -243,6 +244,7 @@
6.12 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
6.13 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
6.14 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
6.15 +(*GOON: revise... from before 0609*)
6.16 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
6.17 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
6.18 \c + c_2 + c_3 + c_4 = 0,\
6.19 @@ -965,13 +967,162 @@
6.20 ("Biegelinie.thy", ["Biegelinien"],
6.21 ["IntegrierenUndKonstanteBestimmen2"]))];
6.22 moveActiveRoot 1;
6.23 -trace_script := true;
6.24 -trace_script := false;
6.25 (*
6.26 -autoCalculate 1 CompleteCalc;
6.27 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.28 +*)
6.29 +"[0 = c_4, \
6.30 +\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
6.31 +\ 0 = c_2, \
6.32 +\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
6.33 +
6.34 +"----- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.35 +states:=[];
6.36 +CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",
6.37 + "Biegelinie y",
6.38 + "Randbedingungen [y L = 0, y' L = 0]",
6.39 + "FunktionsVariable x"],
6.40 + ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
6.41 + ["Biegelinien", "AusMomentenlinie"]))];
6.42 +moveActiveRoot 1;
6.43 +(*
6.44 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.45 *)
6.46
6.47 +"----- Bsp 7.69";
6.48 +states:=[];
6.49 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
6.50 + "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
6.51 + "FunktionsVariable x"],
6.52 + ("Biegelinie.thy", ["Biegelinien"],
6.53 + ["IntegrierenUndKonstanteBestimmen2"] ))];
6.54 +moveActiveRoot 1;
6.55 +(*
6.56 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.57 +*)
6.58 +"[0 = c_4 + 0 / (-1 * EI), \
6.59 +\ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
6.60 +\ 0 = c_3 + 0 / (-1 * EI), \
6.61 +\ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
6.62
6.63 +"----- Bsp 7.70";
6.64 +states:=[];
6.65 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
6.66 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
6.67 + "FunktionsVariable x"],
6.68 + ("Biegelinie.thy", ["Biegelinien"],
6.69 + ["IntegrierenUndKonstanteBestimmen2"] ))];
6.70 +moveActiveRoot 1;
6.71 +(*
6.72 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.73 +*)
6.74 +"[L * q_0 = c, \
6.75 +\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
6.76 +\ 0 = c_4 + 0 / (-1 * EI), \
6.77 +\ 0 = c_3 + 0 / (-1 * EI)]";
6.78 +
6.79 +"----- Bsp 7.71";
6.80 +states:=[];
6.81 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
6.82 + "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
6.83 + "FunktionsVariable x"],
6.84 + ("Biegelinie.thy", ["Biegelinien"],
6.85 + ["IntegrierenUndKonstanteBestimmen2"] ))];
6.86 +moveActiveRoot 1;
6.87 +(*
6.88 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.89 +*)
6.90 +"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
6.91 +\ 0 = c_4 + 0 / (-1 * EI), \
6.92 +\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
6.93 +\ 0 = c_3 + 0 / (-1 * EI)]";
6.94 +
6.95 +"----- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.96 +states:=[];
6.97 +CalcTree [(["Traegerlaenge L",
6.98 + "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",
6.99 + "Biegelinie y",
6.100 + "Randbedingungen [y 0 = 0, y L = 0]",
6.101 + "FunktionsVariable x"],
6.102 + ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
6.103 + ["Biegelinien", "AusMomentenlinie"]))];
6.104 +moveActiveRoot 1;
6.105 +(*
6.106 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.107 +*)
6.108 +
6.109 +"----- Bsp 7.72b";
6.110 +states:=[];
6.111 +CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
6.112 + "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
6.113 + "FunktionsVariable x"],
6.114 + ("Biegelinie.thy", ["Biegelinien"],
6.115 + ["IntegrierenUndKonstanteBestimmen2"] ))];
6.116 +moveActiveRoot 1;
6.117 +(*
6.118 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.119 +*)
6.120 +"[0 = c_2, \
6.121 +\ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
6.122 +\ 0 = c_4 + 0 / (-1 * EI), \
6.123 +\ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";
6.124 +
6.125 +"----- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.126 +states:=[];
6.127 +CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)
6.128 + "Biegelinie y",
6.129 + "Randbedingungen [y L = 0, y' L = 0]",
6.130 + "FunktionsVariable x"],
6.131 + ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
6.132 + ["Biegelinien", "AusMomentenlinie"]))];
6.133 +moveActiveRoot 1;
6.134 +(*
6.135 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.136 +*)
6.137 +
6.138 +
6.139 +"----------- 4x4 systems from Biegelinie -------------------------";
6.140 +"----------- 4x4 systems from Biegelinie -------------------------";
6.141 +"----------- 4x4 systems from Biegelinie -------------------------";
6.142 +"----- Bsp 7.27";
6.143 +val fmz = ["equalities \
6.144 + \[0 = c_4, \
6.145 + \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
6.146 + \ 0 = c_2, \
6.147 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
6.148 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
6.149 +val (dI',pI',mI') =
6.150 + ("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
6.151 + ["EqSystem","normalize","4x4"]);
6.152 +val p = e_pos'; val c = [];
6.153 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.154 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.155 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.156 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.157 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.158 +"------------------------------------------- Apply_Method...";
6.159 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.160 +"[0 = c_4, \
6.161 +\ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
6.162 +\ 0 = c_2, \
6.163 +\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
6.164 +"------------------------------------------- simplify_System_parenthesized...";
6.165 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.166 +"[0 = c_4, \
6.167 +\ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) + \
6.168 +\ (4 * L ^^^ 3 * c / (-24 * EI) + \
6.169 +\ (12 * L ^^^ 2 * c_2 / (-24 * EI) + \
6.170 +\ (L * c_3 + c_4))), \
6.171 +\ 0 = c_2, \
6.172 +\ 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)]";
6.173 +(*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)
6.174 +"------------------------------------------- isolate_bdvs...";
6.175 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.176 +"[c_4 = 0,\
6.177 +\ c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 4 / (-24 * EI)) + -1 * (4 * L ^^^ 3 * c / (-24 * EI)) + -1 * (12 * L ^^^ 2 * c_2 / (-24 * EI)) + -1 * (L * c_3),\
6.178 +\ c_2 = 0, \
6.179 +\ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
6.180 +(*GOON ^^^^^*)
6.181 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.182
6.183
6.184