1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Thu Aug 31 10:49:48 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Thu Aug 31 13:38:22 2006 +0200
1.3 @@ -42,10 +42,14 @@
1.4 store_pbt
1.5 (prep_pbt Biegelinie.thy "pbl_bieg" [] e_pblID
1.6 (["Biegelinien"],
1.7 - [],
1.8 + [("#Given" ,["Traegerlaenge l_", "Streckenlast q_"]),
1.9 + (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.10 + ("#Find" ,["Biegelinie b_"]),
1.11 + ("#Relate",["Randbedingungen rb_"])
1.12 + ],
1.13 append_rls "e_rls" e_rls [],
1.14 None,
1.15 - []));
1.16 + [["IntegrierenUndKonstanteBestimmen2"]]));
1.17
1.18 store_pbt
1.19 (prep_pbt Biegelinie.thy "pbl_bieg_mom" [] e_pblID
1.20 @@ -83,6 +87,24 @@
1.21 None,
1.22 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
1.23
1.24 +store_pbt
1.25 + (prep_pbt Biegelinie.thy "pbl_bieg_vonq" [] e_pblID
1.26 + (["vonBelastungZu","Biegelinien"],
1.27 + [("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),
1.28 + ("#Find" ,["Funktionen funs_"])],
1.29 + append_rls "e_rls" e_rls [],
1.30 + None,
1.31 + [["Biegelinien","ausBelastung"]]));
1.32 +
1.33 +store_pbt
1.34 + (prep_pbt Biegelinie.thy "pbl_bieg_randbed" [] e_pblID
1.35 + (["setzeRandbedingungen","Biegelinien"],
1.36 + [("#Given" ,["Funktionen funs_","FunktionsVariable v_"]),
1.37 + ("#Find" ,["Gleichungen equs_"])],
1.38 + append_rls "e_rls" e_rls [],
1.39 + None,
1.40 + [["Biegelinien","setzeRandbedingungenEin"]]));
1.41 +
1.42
1.43
1.44 (** methods **)
1.45 @@ -186,6 +208,43 @@
1.46 ));
1.47
1.48 store_met
1.49 + (prep_met Biegelinie.thy "met_biege_2" [] e_metID
1.50 + (["IntegrierenUndKonstanteBestimmen2"],
1.51 + [("#Given" ,["Traegerlaenge l_", "Streckenlast q_",
1.52 + "FunktionsVariable v_"]),
1.53 + (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.54 + ("#Find" ,["Biegelinie b_"]),
1.55 + ("#Relate",["RandbedingungenBiegung rb_",
1.56 + "RandbedingungenMoment rm_"])
1.57 + ],
1.58 + {rew_ord'="tless_true",
1.59 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.60 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.61 + Thm ("not_true",num_str not_true),
1.62 + Thm ("not_false",num_str not_false)] ,
1.63 + calc = [], srls = srls, prls = Erls,
1.64 + crls = Atools_erls, nrls = Erls},
1.65 +"Script Biegelinie2Script \
1.66 +\(l_::real) (q_::real) (v_::real) (b_::real=>real) (rb_::bool list) = \
1.67 +\ (let \
1.68 +\ (funs_:: bool list) = \
1.69 +\ (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
1.70 +\ [Biegelinien,ausBelastung]) \
1.71 +\ [real_ q_, real_ v_]); \
1.72 +\ (equs_::bool list) = \
1.73 +\ (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien],\
1.74 +\ [Biegelinien,setzeRandbedingungenEin]) \
1.75 +\ [booll_ funs_, real_ v_]); \
1.76 +\ (cons_::bool list) = \
1.77 +\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.78 +\ [booll_ equs_, reall [c,c_2,c_3,c_4]]); \
1.79 +\ B_ = Take (last_elem funs_); \
1.80 +\ B_ = ((Substitute cons_) @@ \
1.81 +\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B_ \
1.82 +\ in B_)"
1.83 +));
1.84 +
1.85 +store_met
1.86 (prep_met Biegelinie.thy "met_biege_intconst_2" [] e_metID
1.87 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.88 [],
1.89 @@ -218,6 +277,40 @@
1.90 "empty_script"
1.91 ));
1.92
1.93 -(*
1.94 -use"IsacKnowledge/Biegelinie.ML";
1.95 -*)
1.96 +store_met
1.97 + (prep_met Biegelinie.thy "met_biege2" [] e_metID
1.98 + (["Biegelinien"],
1.99 + [],
1.100 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.101 + srls = e_rls,
1.102 + prls=e_rls,
1.103 + crls = Atools_erls, nrls = e_rls},
1.104 +"empty_script"
1.105 +));
1.106 +
1.107 +store_met
1.108 + (prep_met Biegelinie.thy "met_biege_ausbelast" [] e_metID
1.109 + (["Biegelinien","ausBelastung"],
1.110 + [("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),
1.111 + ("#Find" ,["Funktionen funs_"])],
1.112 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.113 + srls = e_rls,
1.114 + prls=e_rls,
1.115 + crls = Atools_erls, nrls = e_rls},
1.116 +"empty_script"
1.117 +));
1.118 +
1.119 +store_met
1.120 + (prep_met Biegelinie.thy "met_biege_setzrand" [] e_metID
1.121 + (["Biegelinien","setzeRandbedingungenEin"],
1.122 + [("#Given" ,["Funktionen funs_","FunktionsVariable v_"]),
1.123 + ("#Find" ,["Gleichungen equs_"])],
1.124 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.125 + srls = e_rls,
1.126 + prls=e_rls,
1.127 + crls = Atools_erls, nrls = e_rls},
1.128 +"empty_script"
1.129 +));
1.130 +
1.131 +(* use"Biegelinie.ML";
1.132 + *)
1.133 \ No newline at end of file
2.1 --- a/src/sml/IsacKnowledge/Biegelinie.thy Thu Aug 31 10:49:48 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Biegelinie.thy Thu Aug 31 13:38:22 2006 +0200
2.3 @@ -31,13 +31,19 @@
2.4 Streckenlast :: real => una
2.5 BiegemomentVerlauf :: bool => una
2.6 Biegelinie :: (real => real) => una
2.7 + Randbedingungen :: bool list => una
2.8 RandbedingungenBiegung :: bool list => una
2.9 RandbedingungenNeigung :: bool list => una
2.10 RandbedingungenMoment :: bool list => una
2.11 RandbedingungenQuerkraft :: bool list => una
2.12 FunktionsVariable :: real => una
2.13 + Funktionen :: bool list => una
2.14 + Gleichungen :: bool list => una
2.15
2.16 (*Script-names*)
2.17 + Biegelinie2Script :: "[real,real,real,real=>real,bool list,
2.18 + bool] => bool"
2.19 + ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)
2.20 BiegelinieScript :: "[real,real,real,real=>real,bool list,bool list,
2.21 bool] => bool"
2.22 ("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)
3.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Thu Aug 31 10:49:48 2006 +0200
3.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Thu Aug 31 13:38:22 2006 +0200
3.3 @@ -16,6 +16,8 @@
3.4 "----------- simplify_leaf for this script -----------------------";
3.5 "----------- Bsp 7.27 me -----------------------------------------";
3.6 "----------- Bsp 7.27 autoCalculate ------------------------------";
3.7 +"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
3.8 +"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
3.9 "-----------------------------------------------------------------";
3.10 "-----------------------------------------------------------------";
3.11 "-----------------------------------------------------------------";
3.12 @@ -463,3 +465,29 @@
3.13 getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
3.14 getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
3.15 getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
3.16 +
3.17 +
3.18 +"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
3.19 +"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
3.20 +"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
3.21 +states:=[];
3.22 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.23 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
3.24 + "FunktionsVariable x"],
3.25 + ("Biegelinie.thy",
3.26 + ["Biegelinien"],
3.27 + ["IntegrierenUndKonstanteBestimmen2"]))];
3.28 +moveActiveRoot 1;
3.29 +autoCalculate 1 CompleteCalcHead;
3.30 +
3.31 +val ((pt,_),_) = get_calc 1;
3.32 +show_pt pt;
3.33 +
3.34 +
3.35 +
3.36 +
3.37 +
3.38 +
3.39 +"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
3.40 +"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";
3.41 +"----------- IntegrierenUndKonstanteBestimmen2 by rewriting ------";