1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Mar 10 17:20:15 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Mar 13 09:09:14 2018 +0100
1.3 @@ -126,16 +126,16 @@
1.4 rules = [(*for rewriting conditions in Thm's*)
1.5 Calc ("Atools.occurs'_in",
1.6 eval_occurs_in "#occurs_in_"),
1.7 - Thm ("not_true", @{thm not_true}),
1.8 + Thm ("not_true", TermC.num_str @{thm not_true}),
1.9 Thm ("not_false",@{thm not_false})
1.10 ],
1.11 scr = EmptyScr},
1.12 srls = Erls, calc = [], errpatts = [],
1.13 rules = [
1.14 - Thm ("integral_const", @{thm integral_const}),
1.15 - Thm ("integral_var", @{thm integral_var}),
1.16 - Thm ("integral_add", @{thm integral_add}),
1.17 - Thm ("integral_mult", @{thm integral_mult}),
1.18 + Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.19 + Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.20 + Thm ("integral_add", TermC.num_str @{thm integral_add}),
1.21 + Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
1.22 Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.23 Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.24 ],
1.25 @@ -153,12 +153,12 @@
1.26 rules = [Calc ("Tools.matches", eval_matches""),
1.27 Calc ("Integrate.is'_f'_x",
1.28 eval_is_f_x "is_f_x_"),
1.29 - Thm ("not_true", @{thm not_true}),
1.30 - Thm ("not_false", @{thm not_false})
1.31 + Thm ("not_true", TermC.num_str @{thm not_true}),
1.32 + Thm ("not_false", TermC.num_str @{thm not_false})
1.33 ],
1.34 scr = EmptyScr},
1.35 srls = Erls, calc = [], errpatts = [],
1.36 - rules = [ (*Thm ("call_for_new_c", @{thm call_for_new_c}),*)
1.37 + rules = [ (*Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.38 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.39 ],
1.40 scr = EmptyScr};
1.41 @@ -181,25 +181,25 @@
1.42 [Calc ("Poly.is'_polyexp",
1.43 eval_is_polyexp "")],
1.44 srls = Erls, calc = [], errpatts = [],
1.45 - rules = [Thm ("rat_mult", @{thm rat_mult}),
1.46 + rules = [Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.47 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.48 - Thm ("rat_mult_poly_l", @{thm rat_mult_poly_l}),
1.49 + Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.50 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.51 - Thm ("rat_mult_poly_r", @{thm rat_mult_poly_r}),
1.52 + Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.53 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.54
1.55 Thm ("real_divide_divide1_mg",
1.56 - @{thm real_divide_divide1_mg}),
1.57 + TermC.num_str @{thm real_divide_divide1_mg}),
1.58 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.59 Thm ("divide_divide_eq_right",
1.60 - @{thm divide_divide_eq_right}),
1.61 + TermC.num_str @{thm divide_divide_eq_right}),
1.62 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.63 Thm ("divide_divide_eq_left",
1.64 - @{thm divide_divide_eq_left}),
1.65 + TermC.num_str @{thm divide_divide_eq_left}),
1.66 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.67 Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
1.68
1.69 - Thm ("rat_power", @{thm rat_power})
1.70 + Thm ("rat_power", TermC.num_str @{thm rat_power})
1.71 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.72 ],
1.73 scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.74 @@ -235,15 +235,15 @@
1.75 val separate_bdv2 =
1.76 append_rls "separate_bdv2"
1.77 collect_bdv
1.78 - [Thm ("separate_bdv", @{thm separate_bdv}),
1.79 + [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.80 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.81 - Thm ("separate_bdv_n", @{thm separate_bdv_n}),
1.82 - Thm ("separate_1_bdv", @{thm separate_1_bdv}),
1.83 + Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.84 + Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.85 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.86 - Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})(*,
1.87 + Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.88 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.89 *****Thm ("add_divide_distrib",
1.90 - ***** @{thm add_divide_distrib})
1.91 + ***** TermC.num_str @{thm add_divide_distrib})
1.92 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.93 ];
1.94 val simplify_Integral =
1.95 @@ -251,9 +251,9 @@
1.96 rew_ord = ("dummy_ord", dummy_ord),
1.97 erls = Atools_erls, srls = Erls,
1.98 calc = [], errpatts = [],
1.99 - rules = [Thm ("distrib_right", @{thm distrib_right}),
1.100 + rules = [Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.101 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.102 - Thm ("add_divide_distrib", @{thm add_divide_distrib}),
1.103 + Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
1.104 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.105 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.106 Rls_ norm_Rational_noadd_fractions,
1.107 @@ -282,21 +282,21 @@
1.108 * Rls_ simplify_power,
1.109 * Rls_ collect_numerals,
1.110 * Rls_ reduce_012,
1.111 -* Thm ("realpow_oneI", @{thm realpow_oneI}),
1.112 +* Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
1.113 * Rls_ discard_parentheses,
1.114 * Rls_ collect_bdv,
1.115 * (*below inserted from 'make_ratpoly_in'*)
1.116 * Rls_ (append_rls "separate_bdv"
1.117 * collect_bdv
1.118 -* [Thm ("separate_bdv", @{thm separate_bdv}),
1.119 +* [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.120 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.121 -* Thm ("separate_bdv_n", @{thm separate_bdv_n}),
1.122 -* Thm ("separate_1_bdv", @{thm separate_1_bdv}),
1.123 +* Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.124 +* Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.125 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.126 -* Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})(*,
1.127 +* Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.128 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.129 * Thm ("add_divide_distrib",
1.130 -* @{thm add_divide_distrib})
1.131 +* TermC.num_str @{thm add_divide_distrib})
1.132 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.133 * ]),
1.134 * Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
2.1 --- a/test/Tools/isac/Test_Isac.thy Sat Mar 10 17:20:15 2018 +0100
2.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Mar 13 09:09:14 2018 +0100
2.3 @@ -292,703 +292,12 @@
2.4 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
2.5 ML_file "Knowledge/diff.sml"
2.6 ML_file "Knowledge/integrate.sml"
2.7 -
2.8 -ML {*
2.9 -*} ML {*
2.10 -"----------- integrate by ruleset -----------------------";
2.11 -"----------- integrate by ruleset -----------------------";
2.12 -"----------- integrate by ruleset -----------------------";
2.13 -val thy = @{theory "Integrate"};
2.14 -val rls = integration_rules;
2.15 -val subs = [(@{term "bdv::real"}, @{term "x::real"})];
2.16 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.17 -
2.18 -val t = (Thm.term_of o the o (parse thy)) "Integral x D x";
2.19 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.20 -if term2str res = "x ^^^ 2 / 2" then () else error "Integral x D x changed";
2.21 -
2.22 -val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
2.23 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.24 -if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x" then () else error "Integral c * x ^^^ 2 + c_2 D x";
2.25 -
2.26 -val rls = add_new_c;
2.27 -val t = (Thm.term_of o the o (parse thy)) "c * (x ^^^ 3 / 3) + c_2 * x";
2.28 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.29 -if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
2.30 -else error "integrate.sml: diff.behav. in add_new_c simpl.";
2.31 -
2.32 -val t = (Thm.term_of o the o (parse thy)) "F x = x ^^^ 3 / 3 + x";
2.33 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.34 -if term2str res = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
2.35 -else error "integrate.sml: diff.behav. in add_new_c equation";
2.36 -
2.37 -val rls = simplify_Integral;
2.38 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.39 -val t = (Thm.term_of o the o (parse thy)) "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
2.40 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.41 -if term2str res = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
2.42 -then () else error "integrate.sml: diff.behav. in simplify_I #1";
2.43 -
2.44 -val rls = integration;
2.45 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.46 -val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
2.47 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.48 -if term2str res = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
2.49 -then () else error "integrate.sml: diff.behav. in integration #1";
2.50 -
2.51 -val t = (Thm.term_of o the o (parse thy)) "Integral 3*x^^^2 + 2*x + 1 D x";
2.52 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.53 -*} ML {*
2.54 -term2str res = "c + x + 2 / 2 * x ^^^ 2 + x ^^^ 3";
2.55 -*} ML {*
2.56 -if term2str res = "c + x + x ^^^ 2 + x ^^^ 3" then ()
2.57 -else error "integrate.sml: diff.behav. in integration #2";
2.58 -*} ML {*
2.59 -
2.60 -val t = (Thm.term_of o the o (parse thy))
2.61 - "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
2.62 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.63 -"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
2.64 -*} ML {*
2.65 -term2str res = "c + 1 / EI * (L * q_0 / (2 * 2) * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
2.66 -*} ML {*
2.67 -if term2str res = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
2.68 -then () else error "integrate.sml: diff.behav. in integration #3";
2.69 -
2.70 -val t = (Thm.term_of o the o (parse thy)) ("Integral " ^ term2str res ^ " D x");
2.71 -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
2.72 -*} ML {*
2.73 -*} ML {* (* folgefehler --------------------------------- ^^^^^^^^^^^ *)
2.74 -if term2str res = "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
2.75 -then () else error "integrate.sml: diff.behav. in integration #4";
2.76 -
2.77 -"----------- rewrite 3rd integration in 7.27 ------------";
2.78 -*} ML {*
2.79 -*} ML {*
2.80 -*} ML {*
2.81 -*} ML {*
2.82 -*} ML {*
2.83 -*}
2.84 -
2.85 -
2.86 -
2.87 -
2.88 -
2.89 -
2.90 -
2.91 -
2.92 -
2.93 -
2.94 -
2.95 -
2.96 -
2.97 -
2.98 -
2.99 -
2.100 -
2.101 ML_file "Knowledge/eqsystem.sml"
2.102 ML_file "Knowledge/test.sml"
2.103 ML_file "Knowledge/polyminus.sml"
2.104 ML_file "Knowledge/vect.sml"
2.105 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
2.106 ML_file "Knowledge/biegelinie-1.sml"
2.107 -
2.108 -ML {*
2.109 -*} ML {*
2.110 -(* tests on biegelinie
2.111 - author: Walther Neuper 050826
2.112 - (c) due to copyright terms
2.113 -*)
2.114 -*} ML {*
2.115 -trace_rewrite := false;
2.116 -"-----------------------------------------------------------------";
2.117 -"table of contents -----------------------------------------------";
2.118 -"-----------------------------------------------------------------";
2.119 -"----------- the rules -------------------------------------------";
2.120 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.121 -"----------- simplify_leaf for this script -----------------------";
2.122 -"----------- Bsp 7.27 me -----------------------------------------";
2.123 -"----------- Bsp 7.27 autoCalculate ------------------------------";
2.124 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
2.125 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
2.126 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
2.127 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
2.128 -"----------- investigate normalforms in biegelinien --------------";
2.129 -"-----------------------------------------------------------------";
2.130 -"-----------------------------------------------------------------";
2.131 -"-----------------------------------------------------------------";
2.132 -
2.133 -val thy = @{theory "Biegelinie"};
2.134 -val ctxt = thy2ctxt' "Biegelinie";
2.135 -fun str2term str = (Thm.term_of o the o (parse thy)) str;
2.136 -fun term2s t = term_to_string'' "Biegelinie" t;
2.137 -fun rewrit thm str =
2.138 - fst (the (rewrite_ thy tless_true e_rls true thm str));
2.139 -*} ML {*
2.140 -
2.141 -"----------- the rules -------------------------------------------";
2.142 -"----------- the rules -------------------------------------------";
2.143 -"----------- the rules -------------------------------------------";
2.144 -val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
2.145 -if term2s t = "Q' x = - q_0" then ()
2.146 -else error "/biegelinie.sml: Belastung_Querkraft";
2.147 -
2.148 -val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
2.149 -if term2s t = "M_b' x = - q_0 * x + c" then ()
2.150 -else error "/biegelinie.sml: Querkraft_Moment";
2.151 -
2.152 -val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
2.153 - term2s t;
2.154 -if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
2.155 -else error "biegelinie.sml: Moment_Neigung";
2.156 -*} ML {*
2.157 -
2.158 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.159 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.160 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.161 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.162 -val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
2.163 -val t = rewrit @{thm Moment_Neigung} t;
2.164 -if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
2.165 -else error "Moment_Neigung broken";
2.166 -(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
2.167 - before declaring "y''" as a constant *)
2.168 -
2.169 -val t = rewrit @{thm make_fun_explicit} t;
2.170 -if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
2.171 -else error "make_fun_explicit broken";
2.172 -*} ML {*
2.173 -
2.174 -"----------- simplify_leaf for this script -----------------------";
2.175 -"----------- simplify_leaf for this script -----------------------";
2.176 -"----------- simplify_leaf for this script -----------------------";
2.177 -val srls = Rls {id="srls_IntegrierenUnd..",
2.178 - preconds = [],
2.179 - rew_ord = ("termlessI",termlessI),
2.180 - erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
2.181 - [(*for asm in NTH_CONS ...*)
2.182 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
2.183 - (*2nd NTH_CONS pushes n+-1 into asms*)
2.184 - Calc("Groups.plus_class.plus", eval_binop "#add_")
2.185 - ],
2.186 - srls = Erls, calc = [], errpatts = [],
2.187 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
2.188 - Calc("Groups.plus_class.plus", eval_binop "#add_"),
2.189 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
2.190 - Calc("Tools.lhs", eval_lhs "eval_lhs_"),
2.191 - Calc("Tools.rhs", eval_rhs "eval_rhs_"),
2.192 - Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
2.193 - ],
2.194 - scr = EmptyScr};
2.195 -val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
2.196 -val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
2.197 -val SOME (e1__,_) = rewrite_set_ thy false srls
2.198 - (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
2.199 -if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
2.200 -
2.201 -val SOME (x1__,_) =
2.202 - rewrite_set_ thy false srls
2.203 - (str2term"argument_in (lhs (M_b 0 = 0))");
2.204 -if term2str x1__ = "0" then ()
2.205 -else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
2.206 -
2.207 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
2.208 -trace_rewrite:=false;
2.209 -*} ML {*
2.210 -
2.211 -"----------- Bsp 7.27 me -----------------------------------------";
2.212 -"----------- Bsp 7.27 me -----------------------------------------";
2.213 -"----------- Bsp 7.27 me -----------------------------------------";
2.214 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
2.215 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
2.216 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
2.217 - "FunktionsVariable x"];
2.218 -val (dI',pI',mI') =
2.219 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
2.220 - ["IntegrierenUndKonstanteBestimmen"]);
2.221 -val p = e_pos'; val c = [];
2.222 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.223 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.224 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.225 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.226 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.227 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.228 -
2.229 -*} ML {*
2.230 -val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
2.231 -(*if itms2str_ ctxt pits = ... all 5 model-items*)
2.232 -val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
2.233 -if itms2str_ ctxt mits = "[]" then ()
2.234 -else error "biegelinie.sml: Bsp 7.27 #2";
2.235 -
2.236 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.237 -case nxt of (_,Add_Given "FunktionsVariable x") => ()
2.238 - | _ => error "biegelinie.sml: Bsp 7.27 #4a";
2.239 -
2.240 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.241 -val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
2.242 -(*if itms2str_ ctxt mits = ... all 6 guard-items*)
2.243 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
2.244 - | _ => error "biegelinie.sml: Bsp 7.27 #4b";
2.245 -
2.246 -"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
2.247 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.248 -case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
2.249 - | _ => error "biegelinie.sml: Bsp 7.27 #4c";
2.250 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.251 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.252 -
2.253 -*} ML {*
2.254 -case nxt of
2.255 - (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
2.256 - | _ => error "biegelinie.sml: Bsp 7.27 #4c";
2.257 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.258 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.259 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.260 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.261 -case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
2.262 - | _ => error "biegelinie.sml: Bsp 7.27 #5";
2.263 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.264 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.265 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.266 -case nxt of
2.267 - ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
2.268 - | _ => error "biegelinie.sml: Bsp 7.27 #5a";
2.269 -
2.270 -*} ML {*
2.271 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.272 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.273 -case nxt of
2.274 - (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
2.275 - | _ => error "biegelinie.sml: Bsp 7.27 #5b";
2.276 -
2.277 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.278 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.279 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.280 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.281 -case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
2.282 - | _ => error "biegelinie.sml: Bsp 7.27 #6";
2.283 -
2.284 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.285 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
2.286 -f2str f;
2.287 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.288 -case nxt of (_, Substitute ["x = 0"]) => ()
2.289 - | _ => error "biegelinie.sml: Bsp 7.27 #7";
2.290 -
2.291 -*} ML {*
2.292 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.293 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.294 -if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
2.295 -else error "biegelinie.sml: Bsp 7.27 #8";
2.296 -
2.297 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.298 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.299 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.300 -*} ML {*
2.301 -if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
2.302 -else error "biegelinie.sml: Bsp 7.27 #9";
2.303 -
2.304 -*} ML {*
2.305 -nxt
2.306 -*} ML {*
2.307 -(*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)
2.308 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.309 -*} ML {*
2.310 -nxt;
2.311 -*} ML {*
2.312 -"~~~~~ fun xxx, args:"; val () = ();
2.313 -"~~~~~ fun me, args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
2.314 -val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
2.315 - val (pt, p) = ptp;
2.316 -(*step p ((pt, Ctree.e_pos'),[]) Theory loader: undefined entry for theory "Isac.Pure"*)
2.317 -"~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Ctree.e_pos'),[]));
2.318 -val pIopt = get_pblID (pt,ip);
2.319 -ip = ([], Ctree.Res) = false;
2.320 -tacis = [];
2.321 -pIopt (*SOME*);
2.322 -member op = [Ctree.Pbl, Ctree.Met] p_
2.323 - andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) = true;
2.324 -(*nxt_specify_ (pt, ip) Theory loader: undefined entry for theory "Isac.Pure"*)
2.325 -"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, (p, p_))) = ((pt, ip));
2.326 -val pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
2.327 - probl, spec = (dI, pI, mI), ...}) = Ctree.get_obj I pt p;
2.328 -Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin = false;
2.329 - val cpI = if pI = e_pblID then pI' else pI;
2.330 - val cmI = if mI = e_metID then mI' else mI;
2.331 - val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
2.332 - val pre = Stool.check_preconds "thy 100820" prls where_ probl;
2.333 - val pb = foldl and_ (true, map fst pre);
2.334 - val (_, tac) =
2.335 - Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
2.336 -tac (*Add_Given "equalities\n [0 = c_2 +..*);
2.337 -*} ML {*
2.338 -(*Chead.nxt_specif tac ptp Theory loader: undefined entry for theory "Isac.Pure"*)
2.339 -"~~~~~ fun nxt_specif, args:"; val ((Tac.Add_Given ct), ptp) = (tac, ptp);
2.340 -"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, (ptp as (pt, (p, Pbl)))) = ( "#Given", ct, ptp);
2.341 -val PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} = get_obj I pt p;
2.342 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
2.343 - val cpI = if pI = e_pblID then pI' else pI;
2.344 -*} ML {*
2.345 -val Err msg = appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct
2.346 -*} ML {*
2.347 -([(Tac.Tac msg, Tac.Tac_ (Thy_Info_get_theory "Isac", msg,msg,msg),
2.348 - (e_pos', (Selem.e_istate, Selem.e_ctxt)))], [], ptp)
2.349 -*} ML {*
2.350 -*} ML {*
2.351 -*} ML {*
2.352 -*} ML {*
2.353 -*} ML {*
2.354 -*} ML {*
2.355 -*} ML {*
2.356 -*} ML {*
2.357 -*} ML {*
2.358 -*} ML {*
2.359 -*} ML {*
2.360 -*} ML {*
2.361 -*} ML {*
2.362 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.363 -*} ML {*
2.364 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.365 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.366 -*} ML {*
2.367 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.368 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.369 -case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
2.370 - | _ => error "biegelinie.sml: Bsp 7.27 #10";
2.371 -
2.372 -*} ML {*
2.373 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.374 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.375 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.376 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.377 -(*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
2.378 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.379 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.380 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.381 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.382 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.383 -case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
2.384 - | _ => error "biegelinie.sml: Bsp 7.27 #11";
2.385 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.386 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.387 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.388 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.389 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.390 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.391 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.392 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.393 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.394 -case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
2.395 - | _ => error "biegelinie.sml: Bsp 7.27 #12";
2.396 -
2.397 -*} ML {*
2.398 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.399 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.400 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.401 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.402 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.403 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.404 -case nxt of
2.405 - (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
2.406 - | _ => error "biegelinie.sml: Bsp 7.27 #13";
2.407 -
2.408 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.409 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.410 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.411 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.412 -case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
2.413 - | _ => error "biegelinie.sml: Bsp 7.27 #14";
2.414 -
2.415 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.416 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.417 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.418 -case nxt of
2.419 - (_, Check_Postcond ["named", "integrate", "function"]) => ()
2.420 - | _ => error "biegelinie.sml: Bsp 7.27 #15";
2.421 -
2.422 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.423 -if f2str f =
2.424 - "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
2.425 -then () else error "biegelinie.sml: Bsp 7.27 #16 f";
2.426 -case nxt of
2.427 - (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
2.428 - | _ => error "biegelinie.sml: Bsp 7.27 #16";
2.429 -
2.430 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.431 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.432 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.433 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.434 -case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
2.435 - | _ => error "biegelinie.sml: Bsp 7.27 #17";
2.436 -
2.437 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.438 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.439 -if f2str f =
2.440 - "y x =\nc_2 + c * x +\n\
2.441 - \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
2.442 -then () else error "biegelinie.sml: Bsp 7.27 #18 f";
2.443 -case nxt of
2.444 - (_, Check_Postcond ["named", "integrate", "function"]) => ()
2.445 - | _ => error "biegelinie.sml: Bsp 7.27 #18";
2.446 -
2.447 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.448 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.449 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.450 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.451 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.452 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.453 -case nxt of
2.454 - (_, Subproblem
2.455 - ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()
2.456 - | _ => error "biegelinie.sml: Bsp 7.27 #19";
2.457 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.458 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.459 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.460 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.461 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.462 -case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
2.463 - | _ => error "biegelinie.sml: Bsp 7.27 #20";
2.464 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.465 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.466 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.467 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.468 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.469 -if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
2.470 -else error "biegelinie.sml: Bsp 7.27 #21 f";
2.471 -case nxt of
2.472 - (_, Subproblem
2.473 - ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
2.474 - | _ => error "biegelinie.sml: Bsp 7.27 #21";
2.475 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.476 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.477 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.478 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.479 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.480 -case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
2.481 - | _ => error "biegelinie.sml: Bsp 7.27 #22";
2.482 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.483 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.484 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.485 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.486 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.487 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.488 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.489 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.490 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.491 -case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
2.492 - | _ => error "biegelinie.sml: Bsp 7.27 #23";
2.493 -
2.494 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.495 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.496 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.497 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.498 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.499 -if f2str f =
2.500 - "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
2.501 - "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
2.502 -then () else error "biegelinie.sml: Bsp 7.27 #24 f";
2.503 -case nxt of ("End_Proof'", End_Proof') => ()
2.504 - | _ => error "biegelinie.sml: Bsp 7.27 #24";
2.505 -
2.506 -show_pt pt;
2.507 -(*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
2.508 -(([1], Frm), q_ x = q_0),
2.509 -(([1], Res), - q_ x = - q_0),
2.510 -(([2], Res), Q' x = - q_0),
2.511 -(([3], Pbl), Integrate (- q_0, x)),
2.512 -(([3,1], Frm), Q x = Integral - q_0 D x),
2.513 -(([3,1], Res), Q x = -1 * q_0 * x + c),
2.514 -(([3], Res), Q x = -1 * q_0 * x + c),
2.515 -(([4], Res), M_b' x = -1 * q_0 * x + c),
2.516 -(([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
2.517 -(([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
2.518 -(([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
2.519 -(([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
2.520 -(([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
2.521 -(([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
2.522 -(([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
2.523 -(([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
2.524 -(([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
2.525 -(([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
2.526 - 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
2.527 -(([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
2.528 -(([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
2.529 -(([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
2.530 -(([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
2.531 -(([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
2.532 -(([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
2.533 -(([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
2.534 -(([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
2.535 -(([10,4,4], Res), c = L * q_0 / 2),
2.536 -(([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
2.537 -(([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
2.538 -(([10], Res), [c = L * q_0 / 2, c_2 = 0]),
2.539 -(([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
2.540 -(([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
2.541 -(([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
2.542 -(([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
2.543 -(([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
2.544 -(([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
2.545 -(([15,1], Res), y' x =
2.546 -(Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
2.547 -c)]*)
2.548 -
2.549 -"----------- Bsp 7.27 autoCalculate ------------------------------";
2.550 -"----------- Bsp 7.27 autoCalculate ------------------------------";
2.551 -"----------- Bsp 7.27 autoCalculate ------------------------------";
2.552 - reset_states ();
2.553 - CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
2.554 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
2.555 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
2.556 - "FunktionsVariable x"],
2.557 - ("Biegelinie",
2.558 - ["MomentBestimmte","Biegelinien"],
2.559 - ["IntegrierenUndKonstanteBestimmen"]))];
2.560 - moveActiveRoot 1;
2.561 - autoCalculate 1 CompleteCalcHead;
2.562 -
2.563 - fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
2.564 -(*
2.565 -> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
2.566 -val it = true : bool
2.567 -*)
2.568 - autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
2.569 - val ((pt,_),_) = get_calc 1;
2.570 - case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
2.571 - | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
2.572 -
2.573 - autoCalculate 1 CompleteCalc;
2.574 -val ((pt,p),_) = get_calc 1;
2.575 -if p = ([], Res) andalso length (children pt) = 23 andalso
2.576 -term2str (get_obj g_res pt (fst p)) =
2.577 -"y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
2.578 -then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
2.579 -
2.580 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
2.581 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
2.582 - show_pt pt;
2.583 -
2.584 -(*check all formulae for getTactic*)
2.585 - getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
2.586 - getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
2.587 - getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
2.588 - getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
2.589 - getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
2.590 - getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
2.591 -
2.592 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
2.593 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
2.594 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
2.595 -val fmz =
2.596 - ["Streckenlast q_0","FunktionsVariable x",
2.597 - "Funktionen [Q x = c + -1 * q_0 * x, \
2.598 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
2.599 - \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
2.600 - \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"];
2.601 -val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
2.602 - ["Biegelinien","ausBelastung"]);
2.603 -val p = e_pos'; val c = [];
2.604 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.605 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.606 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.607 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.608 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.609 -case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
2.610 -| _ => error "biegelinie.sml met2 b";
2.611 -
2.612 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
2.613 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
2.614 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
2.615 -case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
2.616 -| _ => error "biegelinie.sml met2 c";
2.617 -
2.618 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.619 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.620 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.621 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.622 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.623 -
2.624 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
2.625 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
2.626 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
2.627 -case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
2.628 -| _ => error "biegelinie.sml met2 d";
2.629 -
2.630 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.631 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.632 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.633 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.634 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.635 - "M_b x = Integral c + -1 * q_0 * x D x";
2.636 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.637 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
2.638 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.639 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
2.640 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.641 - "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
2.642 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.643 - "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
2.644 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.645 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.646 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.647 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.648 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.649 - "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
2.650 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.651 -"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
2.652 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.653 -"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
2.654 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.655 -"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
2.656 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.657 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.658 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.659 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.660 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.661 -"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";
2.662 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.663 -"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)";
2.664 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.665 - "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)";
2.666 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.667 -if f2str f =
2.668 - "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\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)]"
2.669 -then case nxt of ("End_Proof'", End_Proof') => ()
2.670 - | _ => error "biegelinie.sml met2 e 1"
2.671 -else error "biegelinie.sml met2 e 2";
2.672 -
2.673 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
2.674 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
2.675 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
2.676 -val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
2.677 - "substitution (M_b L = 0)",
2.678 - "equality equ_equ"];
2.679 -val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
2.680 - ["Equation","fromFunction"]);
2.681 -val p = e_pos'; val c = [];
2.682 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.683 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.684 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.685 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.686 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.687 -
2.688 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.689 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
2.690 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.691 - "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
2.692 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.693 - "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
2.694 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.695 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.696 -if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
2.697 - f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
2.698 -then case nxt of ("End_Proof'", End_Proof') => ()
2.699 - | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
2.700 -else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
2.701 -*} ML {*
2.702 -*}
2.703 -
2.704 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)
2.705 ML_file "Knowledge/algein.sml"
2.706 ML_file "Knowledge/diophanteq.sml"