Biegelinie2, intermediate state until SubProblem (_,[setzeRandbedingungen,Biegelinien] (excl.)
1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Thu Aug 31 13:38:22 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Fri Sep 01 09:25:35 2006 +0200
1.3 @@ -91,7 +91,7 @@
1.4 (prep_pbt Biegelinie.thy "pbl_bieg_vonq" [] e_pblID
1.5 (["vonBelastungZu","Biegelinien"],
1.6 [("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),
1.7 - ("#Find" ,["Funktionen funs_"])],
1.8 + ("#Find" ,["Funktionen funs___"])],
1.9 append_rls "e_rls" e_rls [],
1.10 None,
1.11 [["Biegelinien","ausBelastung"]]));
1.12 @@ -100,7 +100,7 @@
1.13 (prep_pbt Biegelinie.thy "pbl_bieg_randbed" [] e_pblID
1.14 (["setzeRandbedingungen","Biegelinien"],
1.15 [("#Given" ,["Funktionen funs_","FunktionsVariable v_"]),
1.16 - ("#Find" ,["Gleichungen equs_"])],
1.17 + ("#Find" ,["Gleichungen equs___"])],
1.18 append_rls "e_rls" e_rls [],
1.19 None,
1.20 [["Biegelinien","setzeRandbedingungenEin"]]));
1.21 @@ -143,7 +143,7 @@
1.22 rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.23 [Calc ("Atools.ident",eval_ident "#ident_"),
1.24 Thm ("not_true",num_str not_true),
1.25 - Thm ("not_false",num_str not_false)] ,
1.26 + Thm ("not_false",num_str not_false)],
1.27 calc = [], srls = srls, prls = Erls,
1.28 crls = Atools_erls, nrls = Erls},
1.29 "Script BiegelinieScript \
1.30 @@ -214,16 +214,17 @@
1.31 "FunktionsVariable v_"]),
1.32 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.33 ("#Find" ,["Biegelinie b_"]),
1.34 - ("#Relate",["RandbedingungenBiegung rb_",
1.35 - "RandbedingungenMoment rm_"])
1.36 + ("#Relate",["Randbedingungen rb_"])
1.37 ],
1.38 {rew_ord'="tless_true",
1.39 rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.40 [Calc ("Atools.ident",eval_ident "#ident_"),
1.41 Thm ("not_true",num_str not_true),
1.42 - Thm ("not_false",num_str not_false)] ,
1.43 - calc = [], srls = srls, prls = Erls,
1.44 - crls = Atools_erls, nrls = Erls},
1.45 + Thm ("not_false",num_str not_false)],
1.46 + calc = [],
1.47 + srls = append_rls "erls_IntegrierenUndK.." e_rls
1.48 + [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.49 + prls = Erls, crls = Atools_erls, nrls = Erls},
1.50 "Script Biegelinie2Script \
1.51 \(l_::real) (q_::real) (v_::real) (b_::real=>real) (rb_::bool list) = \
1.52 \ (let \
1.53 @@ -293,11 +294,39 @@
1.54 (["Biegelinien","ausBelastung"],
1.55 [("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),
1.56 ("#Find" ,["Funktionen funs_"])],
1.57 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.58 - srls = e_rls,
1.59 - prls=e_rls,
1.60 - crls = Atools_erls, nrls = e_rls},
1.61 -"empty_script"
1.62 + {rew_ord'="tless_true",
1.63 + rls' = append_rls "erls_ausBelastung" e_rls
1.64 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.65 + Thm ("not_true",num_str not_true),
1.66 + Thm ("not_false",num_str not_false)],
1.67 + calc = [],
1.68 + srls = append_rls "srls_ausBelastung" e_rls
1.69 + [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.70 + prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.71 +"Script Belastung2BiegelScript (q_::real) (v_::real) = \
1.72 +\ (let q__ = Take (q v_ = q_); \
1.73 +\ q__ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.74 +\ (Rewrite Belastung_Querkraft True)) q__; \
1.75 +\ (Q__:: bool) = \
1.76 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.77 +\ [Diff,integration,named]) \
1.78 +\ [real_ (rhs q__), real_ v_, real_real_ Q]); \
1.79 +\ Q__ = Rewrite Querkraft_Moment True Q__; \
1.80 +\ (M__::bool) = \
1.81 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.82 +\ [Diff,integration,named]) \
1.83 +\ [real_ (rhs Q__), real_ v_, real_real_ M_b]); \
1.84 +\ M__ = ((Rewrite Moment_Neigung False) @@ \
1.85 +\ (Rewrite make_fun_explicit False)) M__; \
1.86 +\ (N__:: bool) = \
1.87 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.88 +\ [Diff,integration,named]) \
1.89 +\ [real_ (rhs M__), real_ v_, real_real_ y']); \
1.90 +\ (B__:: bool) = \
1.91 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.92 +\ [Diff,integration,named]) \
1.93 +\ [real_ (rhs N__), real_ v_, real_real_ y]) \
1.94 +\ in [q__, Q__, M__, N__, B__])"
1.95 ));
1.96
1.97 store_met
2.1 --- a/src/sml/IsacKnowledge/Biegelinie.thy Thu Aug 31 13:38:22 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Biegelinie.thy Fri Sep 01 09:25:35 2006 +0200
2.3 @@ -57,6 +57,12 @@
2.4 "[real,real,real,real=>real,bool list,bool list,bool list,
2.5 bool] => bool"
2.6 ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
2.7 + Belastung2BiegelScript :: "[real,real,
2.8 + bool list] => bool list"
2.9 + ("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)
2.10 + SetzeRandbedScript :: "[bool list,real,
2.11 + bool list] => bool list"
2.12 + ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
2.13
2.14 rules
2.15
3.1 --- a/src/sml/ME/ptyps.sml Thu Aug 31 13:38:22 2006 +0200
3.2 +++ b/src/sml/ME/ptyps.sml Fri Sep 01 09:25:35 2006 +0200
3.3 @@ -361,20 +361,20 @@
3.4
3.5 (* data for methods stored in 'methods'-database *)
3.6 type met =
3.7 - (*defaults for Rewrite' (rls have their own data):*)
3.8 - {guh : guh, (*unique within this isac-knowledge*)
3.9 - mathauthors: string list, (*copyright*)
3.10 - init : pblID, (*WN060721 introduced mistakenly*)
3.11 - rew_ord' : rew_ord', (*for rules in Detail
3.12 - TODO.WN0509 store fun itself, see 'type pbt'*)
3.13 - erls : rls, (*the eval_rls for cond. in rules FIXME "rls'"*)
3.14 - srls : rls, (*for evaluating list expressions in scr*)
3.15 - prls : rls, (*for evaluating predicates in ppc/pre*)
3.16 - crls : rls, (*for check_elementwise*)
3.17 - nrls : rls, (*canonical simplifier specific for this met*)
3.18 - calc : calc list, (*040207: <--- calclist' in fun prep_met *)
3.19 - (*branch : TransitiveB set in append_problem at generation ob pblobj
3.20 - FIXXXME.8.03: set branch from met in Apply_Method*)
3.21 + {guh : guh, (*unique within this isac-knowledge *)
3.22 + mathauthors: string list,(*copyright *)
3.23 + init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
3.24 + rew_ord' : rew_ord', (*for rules in Detail
3.25 + TODO.WN0509 store fun itself, see 'type pbt'*)
3.26 + erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
3.27 + instead erls in "fun prep_met" *)
3.28 + srls : rls, (*for evaluating list expressions in scr *)
3.29 + prls : rls, (*for evaluating predicates in ppc/pre *)
3.30 + crls : rls, (*for check_elementwise, ie. formulae in calc.*)
3.31 + nrls : rls, (*canonical simplifier specific for this met *)
3.32 + calc : calc list, (*040207: <--- calclist' in fun prep_met *)
3.33 + (*branch : TransitiveB set in append_problem at generation ob pblobj
3.34 + FIXXXME.8.03: set branch from met in Apply_Method *)
3.35
3.36 (* compare type pbt:*)
3.37 ppc: pat list,
3.38 @@ -778,7 +778,6 @@
3.39 in ({guh=guh,mathauthors=maa,init=init,
3.40 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
3.41 calc = if scr = "empty_script" then []
3.42 - (*scr_isa_fns*) (*FIXXXME.040207 de-comment below !*)
3.43 else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
3.44 (filter is_calc) o stacpbls) sc,
3.45 crls=cr, nrls=nr, scr=Script sc}:met,
4.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Thu Aug 31 13:38:22 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Fri Sep 01 09:25:35 2006 +0200
4.3 @@ -17,7 +17,6 @@
4.4 "----------- Bsp 7.27 me -----------------------------------------";
4.5 "----------- Bsp 7.27 autoCalculate ------------------------------";
4.6 "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
4.7 -"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -470,24 +469,104 @@
4.12 "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
4.13 "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
4.14 "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
4.15 -states:=[];
4.16 -CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.17 +"----- met [Biegelinien,ausBelastung]";
4.18 +val fmz = ["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",
4.22 - ["Biegelinien"],
4.23 - ["IntegrierenUndKonstanteBestimmen2"]))];
4.24 -moveActiveRoot 1;
4.25 -autoCalculate 1 CompleteCalcHead;
4.26 + "FunktionsVariable x"];
4.27 +val (dI',pI',mI') = ("Biegelinie.thy", ["Biegelinien"],
4.28 + ["IntegrierenUndKonstanteBestimmen2"]);
4.29 +val p = e_pos'; val c = [];
4.30 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.31 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.32 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.36 +if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
4.37 +then () else raise error "biegelinie.sml met2 a";
4.38 +(*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
4.39 +... THIS MEANS:
4.40 +#a# "Script Biegelinie2Script ..
4.41 +\ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
4.42 +\ [Biegelinien,ausBelastung]) \
4.43 +\ [real_ q_, real_ v_]); \
4.44
4.45 -val ((pt,_),_) = get_calc 1;
4.46 -show_pt pt;
4.47 +#b# prep_met ... (["Biegelinien","ausBelastung"],
4.48 + ... ("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),
4.49 + "Script Belastung2BiegelScript (q_::real) (v_::real) = \
4.50
4.51 +#a#b# BOTH HAVE 2 ARGUMENTS q_ and v_ ...OK
4.52 +##########################################################################
4.53 +BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
4.54 +##########################################################################*)
4.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.59 +if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
4.60 +then () else raise error "biegelinie.sml met2 b";
4.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q x = q_0";
4.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q x = - q_0";
4.63 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
4.64 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
4.65 +| _ => raise error "biegelinie.sml met2 c";
4.66
4.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.68 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.69 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.72
4.73 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
4.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
4.75 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
4.76 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
4.77 +| _ => raise error "biegelinie.sml met2 d";
4.78
4.79 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.83 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.84 + "M_b x = Integral c + -1 * q_0 * x D x";
4.85 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.86 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
4.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.88 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
4.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.90 + "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
4.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.92 + "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
4.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.98 + "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
4.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.100 +"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
4.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.102 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
4.103 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.104 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
4.105 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.106 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.107 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.109 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.110 +"y x =\nIntegral c_3 +\n 1 / (-1 * EI) *\n (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x";
4.111 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.112 +"y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
4.113 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.114 + "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
4.115 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
4.116 + "[Q' x = - q_0, M_b' x = c + -1 * q_0 * x,\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4),\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]";
4.117 +case nxt of (_,Subproblem (_, ["setzeRandbedingungen", "Biegelinien"])) => ()
4.118 +| _ => raise error "biegelinie.sml met2 d";
4.119 +
4.120
4.121
4.122 -"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
4.123 -"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
4.124 -"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
4.125 +
4.126 +(*
4.127 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.128 +*)
4.129 \ No newline at end of file