1.1 --- a/test/Tools/isac/Test_Isac.thy Wed Mar 07 14:20:33 2018 +0100
1.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Mar 08 07:28:17 2018 +0100
1.3 @@ -108,6 +108,7 @@
1.4 open LTool; rule2stac;
1.5 open Rewrite; mk_thm;
1.6 open Calc; get_pair;
1.7 + open TermC; ;
1.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.9 *}
1.10
1.11 @@ -178,6 +179,78 @@
1.12 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.13 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.14 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
1.15 +ML {*
1.16 +"----------- fun autoCalculate -----------------------------------";
1.17 +reset_states ();
1.18 +CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
1.19 + [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
1.20 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
1.21 +Iterator 1;
1.22 +moveActiveRoot 1;
1.23 +(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.24 +modeling is skipped FIXME
1.25 +see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
1.26 + setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
1.27 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
1.28 +
1.29 + fetchProposedTactic 1;
1.30 + setNextTactic 1 (Add_Given "solveFor x");
1.31 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.32 +
1.33 + fetchProposedTactic 1;
1.34 + setNextTactic 1 (Add_Find "solutions L");
1.35 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.36 +
1.37 + fetchProposedTactic 1;
1.38 + setNextTactic 1 (Specify_Theory "Test");
1.39 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.40 +*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.41 +autoCalculate 1 (Step 1);
1.42 +"----- step 1 ---";
1.43 +autoCalculate 1 (Step 1);
1.44 +"----- step 2 ---";
1.45 +autoCalculate 1 (Step 1);
1.46 +"----- step 3 ---";
1.47 +autoCalculate 1 (Step 1);
1.48 +*} ML {*
1.49 +"----- step 4 ---";
1.50 +autoCalculate 1 (Step 1);
1.51 +val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
1.52 +*} ML {*
1.53 +term2str t = "c + x + 1 / (2 + 1) * x ^^^ (2 + 1)";
1.54 +*} ML {*
1.55 +"----- step 5 ---";
1.56 +autoCalculate 1 (Step 1);
1.57 +val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
1.58 +*} ML {*
1.59 +term2str t;
1.60 +*} ML {*
1.61 +"----- step 6 ---";
1.62 +autoCalculate 1 (Step 1);
1.63 +val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
1.64 +*} ML {*
1.65 +term2str t;
1.66 +*} ML {*
1.67 +"----- step 7 ---";
1.68 +autoCalculate 1 (Step 1);
1.69 +val (ptp as (_, p), _) = get_calc 1; val (Form t,_,_) = pt_extract ptp;
1.70 +*} ML {*
1.71 +term2str t;
1.72 +*} ML {*
1.73 +"----- step 8 ---";
1.74 +autoCalculate 1 (Step 1);
1.75 +val (ptp as (_, p), _) = get_calc 1;
1.76 +val (Form t,_,_) = pt_extract ptp;
1.77 +
1.78 +*} ML {*
1.79 +*} ML {*
1.80 +term2str t
1.81 +*} ML {*
1.82 +if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
1.83 +else error "mathengine.sml -- fun autoCalculate -- end";
1.84 +*} ML {*
1.85 +*} ML {*
1.86 +*}
1.87 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
1.88 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
1.89 ML_file "xmlsrc/mathml.sml" (*part.*)
1.90 @@ -219,12 +292,687 @@
1.91 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
1.92 ML_file "Knowledge/diff.sml"
1.93 ML_file "Knowledge/integrate.sml"
1.94 +
1.95 +ML {*
1.96 +*} ML {*
1.97 +"----------- simplify by ruleset reducing make_ratpoly_in";
1.98 +val thy = @{theory "Isac"};
1.99 +"===== test 1";
1.100 +val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
1.101 +
1.102 +"----- stepwise from the rulesets in simplify_Integral and below-----";
1.103 +val rls = norm_Rational_noadd_fractions;
1.104 +case rewrite_set_inst_ thy true subs rls t of
1.105 + SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
1.106 + | NONE => ();
1.107 +
1.108 +"===== test 2";
1.109 +val rls = order_add_mult_in;
1.110 +val SOME (t,[]) = rewrite_set_ thy true rls t;
1.111 +if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
1.112 +else error "integrate.sml simplify by ruleset order_add_mult_in #2";
1.113 +
1.114 +"===== test 3";
1.115 +val rls = discard_parentheses;
1.116 +val SOME (t,[]) = rewrite_set_ thy true rls t;
1.117 +if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
1.118 +else error "integrate.sml simplify by ruleset discard_parenth.. #3";
1.119 +
1.120 +"===== test 4";
1.121 +val rls =
1.122 + (append_rls "separate_bdv" collect_bdv
1.123 + [Thm ("separate_bdv", num_str @{thm separate_bdv}),
1.124 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.125 + Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
1.126 + (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
1.127 + Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
1.128 + (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.129 + Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
1.130 + (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.131 + ]);
1.132 +(*show_types := true; --- do we need type-constraint in thms? *)
1.133 +@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
1.134 +@{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
1.135 +@{thm separate_1_bdv}; (*::?'a*)
1.136 +val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
1.137 +@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
1.138 +(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
1.139 +
1.140 +val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
1.141 +if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
1.142 +else error "integrate.sml simplify by ruleset separate_bdv.. #4";
1.143 +
1.144 +"===== test 5";
1.145 +val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
1.146 +val rls = simplify_Integral;
1.147 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1.148 +(* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
1.149 +if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
1.150 +else error "integrate.sml, simplify_Integral #99";
1.151 +
1.152 +"........... 2nd integral ........................................";
1.153 +"........... 2nd integral ........................................";
1.154 +"........... 2nd integral ........................................";
1.155 +val t = str2t
1.156 +"Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
1.157 +val rls = simplify_Integral;
1.158 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1.159 +if term2str t =
1.160 + "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
1.161 +then () else raise error "integrate.sml, simplify_Integral #198";
1.162 +
1.163 +val rls = integration_rules;
1.164 +val SOME (t,[]) = rewrite_set_ thy true rls t;
1.165 +term2str t;
1.166 +if term2str t =
1.167 + "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
1.168 +then () else error "integrate.sml, simplify_Integral #199";
1.169 +
1.170 +
1.171 +"----------- integrate by ruleset -----------------------";*} ML {*
1.172 +*}
1.173 +
1.174 ML_file "Knowledge/eqsystem.sml"
1.175 ML_file "Knowledge/test.sml"
1.176 ML_file "Knowledge/polyminus.sml"
1.177 ML_file "Knowledge/vect.sml"
1.178 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
1.179 ML_file "Knowledge/biegelinie-1.sml"
1.180 +
1.181 +ML {*
1.182 +*} ML {*
1.183 +(* tests on biegelinie
1.184 + author: Walther Neuper 050826
1.185 + (c) due to copyright terms
1.186 +*)
1.187 +*} ML {*
1.188 +trace_rewrite := false;
1.189 +"-----------------------------------------------------------------";
1.190 +"table of contents -----------------------------------------------";
1.191 +"-----------------------------------------------------------------";
1.192 +"----------- the rules -------------------------------------------";
1.193 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.194 +"----------- simplify_leaf for this script -----------------------";
1.195 +"----------- Bsp 7.27 me -----------------------------------------";
1.196 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.197 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.198 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.199 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.200 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
1.201 +"----------- investigate normalforms in biegelinien --------------";
1.202 +"-----------------------------------------------------------------";
1.203 +"-----------------------------------------------------------------";
1.204 +"-----------------------------------------------------------------";
1.205 +
1.206 +val thy = @{theory "Biegelinie"};
1.207 +val ctxt = thy2ctxt' "Biegelinie";
1.208 +fun str2term str = (Thm.term_of o the o (parse thy)) str;
1.209 +fun term2s t = term_to_string'' "Biegelinie" t;
1.210 +fun rewrit thm str =
1.211 + fst (the (rewrite_ thy tless_true e_rls true thm str));
1.212 +*} ML {*
1.213 +
1.214 +"----------- the rules -------------------------------------------";
1.215 +"----------- the rules -------------------------------------------";
1.216 +"----------- the rules -------------------------------------------";
1.217 +val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
1.218 +if term2s t = "Q' x = - q_0" then ()
1.219 +else error "/biegelinie.sml: Belastung_Querkraft";
1.220 +
1.221 +val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
1.222 +if term2s t = "M_b' x = - q_0 * x + c" then ()
1.223 +else error "/biegelinie.sml: Querkraft_Moment";
1.224 +
1.225 +val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.226 + term2s t;
1.227 +if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
1.228 +else error "biegelinie.sml: Moment_Neigung";
1.229 +*} ML {*
1.230 +
1.231 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.232 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.233 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.234 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.235 +val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
1.236 +val t = rewrit @{thm Moment_Neigung} t;
1.237 +if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
1.238 +else error "Moment_Neigung broken";
1.239 +(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
1.240 + before declaring "y''" as a constant *)
1.241 +
1.242 +val t = rewrit @{thm make_fun_explicit} t;
1.243 +if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
1.244 +else error "make_fun_explicit broken";
1.245 +*} ML {*
1.246 +
1.247 +"----------- simplify_leaf for this script -----------------------";
1.248 +"----------- simplify_leaf for this script -----------------------";
1.249 +"----------- simplify_leaf for this script -----------------------";
1.250 +val srls = Rls {id="srls_IntegrierenUnd..",
1.251 + preconds = [],
1.252 + rew_ord = ("termlessI",termlessI),
1.253 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.254 + [(*for asm in NTH_CONS ...*)
1.255 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.256 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.257 + Calc("Groups.plus_class.plus", eval_binop "#add_")
1.258 + ],
1.259 + srls = Erls, calc = [], errpatts = [],
1.260 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.261 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.262 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.263 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.264 + Calc("Tools.rhs", eval_rhs "eval_rhs_"),
1.265 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
1.266 + ],
1.267 + scr = EmptyScr};
1.268 +val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
1.269 +val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
1.270 +val SOME (e1__,_) = rewrite_set_ thy false srls
1.271 + (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
1.272 +if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
1.273 +
1.274 +val SOME (x1__,_) =
1.275 + rewrite_set_ thy false srls
1.276 + (str2term"argument_in (lhs (M_b 0 = 0))");
1.277 +if term2str x1__ = "0" then ()
1.278 +else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
1.279 +
1.280 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
1.281 +trace_rewrite:=false;
1.282 +*} ML {*
1.283 +
1.284 +"----------- Bsp 7.27 me -----------------------------------------";
1.285 +"----------- Bsp 7.27 me -----------------------------------------";
1.286 +"----------- Bsp 7.27 me -----------------------------------------";
1.287 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.288 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.289 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.290 + "FunktionsVariable x"];
1.291 +val (dI',pI',mI') =
1.292 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
1.293 + ["IntegrierenUndKonstanteBestimmen"]);
1.294 +val p = e_pos'; val c = [];
1.295 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.296 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.297 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.298 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.299 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.300 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.301 +
1.302 +*} ML {*
1.303 +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
1.304 +(*if itms2str_ ctxt pits = ... all 5 model-items*)
1.305 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
1.306 +if itms2str_ ctxt mits = "[]" then ()
1.307 +else error "biegelinie.sml: Bsp 7.27 #2";
1.308 +
1.309 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.310 +case nxt of (_,Add_Given "FunktionsVariable x") => ()
1.311 + | _ => error "biegelinie.sml: Bsp 7.27 #4a";
1.312 +
1.313 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.314 +val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
1.315 +(*if itms2str_ ctxt mits = ... all 6 guard-items*)
1.316 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.317 + | _ => error "biegelinie.sml: Bsp 7.27 #4b";
1.318 +
1.319 +"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
1.320 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.321 +case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.322 + | _ => error "biegelinie.sml: Bsp 7.27 #4c";
1.323 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.324 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.325 +
1.326 +*} ML {*
1.327 +case nxt of
1.328 + (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
1.329 + | _ => error "biegelinie.sml: Bsp 7.27 #4c";
1.330 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.331 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.332 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.333 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.334 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.335 + | _ => error "biegelinie.sml: Bsp 7.27 #5";
1.336 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.337 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.338 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.339 +case nxt of
1.340 + ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
1.341 + | _ => error "biegelinie.sml: Bsp 7.27 #5a";
1.342 +
1.343 +*} ML {*
1.344 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.345 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.346 +case nxt of
1.347 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
1.348 + | _ => error "biegelinie.sml: Bsp 7.27 #5b";
1.349 +
1.350 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.351 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.352 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.353 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.354 +case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
1.355 + | _ => error "biegelinie.sml: Bsp 7.27 #6";
1.356 +
1.357 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.358 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
1.359 +f2str f;
1.360 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.361 +case nxt of (_, Substitute ["x = 0"]) => ()
1.362 + | _ => error "biegelinie.sml: Bsp 7.27 #7";
1.363 +
1.364 +*} ML {*
1.365 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.366 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.367 +if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
1.368 +else error "biegelinie.sml: Bsp 7.27 #8";
1.369 +
1.370 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.371 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.372 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.373 +*} ML {*
1.374 +if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
1.375 +else error "biegelinie.sml: Bsp 7.27 #9";
1.376 +
1.377 +*} ML {*
1.378 +(*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)
1.379 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.380 +*} ML {*
1.381 +nxt;
1.382 +*} ML {*
1.383 +"~~~~~ fun xxx, args:"; val () = ();
1.384 +"~~~~~ fun me, args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.385 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
1.386 + val (pt, p) = ptp;
1.387 +(*step p ((pt, Ctree.e_pos'),[]) Theory loader: undefined entry for theory "Isac.Pure"*)
1.388 +"~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Ctree.e_pos'),[]));
1.389 +val pIopt = get_pblID (pt,ip);
1.390 +ip = ([], Ctree.Res) = false;
1.391 +tacis = [];
1.392 +pIopt (*SOME*);
1.393 +member op = [Ctree.Pbl, Ctree.Met] p_
1.394 + andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) = true;
1.395 +(*nxt_specify_ (pt, ip) Theory loader: undefined entry for theory "Isac.Pure"*)
1.396 +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, (p, p_))) = ((pt, ip));
1.397 +val pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
1.398 + probl, spec = (dI, pI, mI), ...}) = Ctree.get_obj I pt p;
1.399 +Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin = false;
1.400 + val cpI = if pI = e_pblID then pI' else pI;
1.401 + val cmI = if mI = e_metID then mI' else mI;
1.402 + val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
1.403 + val pre = Stool.check_preconds "thy 100820" prls where_ probl;
1.404 + val pb = foldl and_ (true, map fst pre);
1.405 + val (_, tac) =
1.406 + Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
1.407 +tac (*Add_Given "equalities\n [0 = c_2 +..*);
1.408 +*} ML {*
1.409 +(*Chead.nxt_specif tac ptp Theory loader: undefined entry for theory "Isac.Pure"*)
1.410 +"~~~~~ fun nxt_specif, args:"; val ((Tac.Add_Given ct), ptp) = (tac, ptp);
1.411 +"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, (ptp as (pt, (p, Pbl)))) = ( "#Given", ct, ptp);
1.412 +val PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} = get_obj I pt p;
1.413 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.414 + val cpI = if pI = e_pblID then pI' else pI;
1.415 +*} ML {*
1.416 +val Err msg = appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct
1.417 +*} ML {*
1.418 +([(Tac.Tac msg, Tac.Tac_ (Thy_Info_get_theory "Isac", msg,msg,msg),
1.419 + (e_pos', (Selem.e_istate, Selem.e_ctxt)))], [], ptp)
1.420 +*} ML {*
1.421 +*} ML {*
1.422 +*} ML {*
1.423 +*} ML {*
1.424 +*} ML {*
1.425 +*} ML {*
1.426 +*} ML {*
1.427 +*} ML {*
1.428 +*} ML {*
1.429 +*} ML {*
1.430 +*} ML {*
1.431 +*} ML {*
1.432 +*} ML {*
1.433 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.434 +*} ML {*
1.435 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.436 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.437 +*} ML {*
1.438 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.439 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.440 +case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
1.441 + | _ => error "biegelinie.sml: Bsp 7.27 #10";
1.442 +
1.443 +*} ML {*
1.444 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.445 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.446 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.447 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.448 +(*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
1.449 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.450 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.451 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.452 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.453 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.454 +case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
1.455 + | _ => error "biegelinie.sml: Bsp 7.27 #11";
1.456 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.457 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.458 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.459 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.460 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.461 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.462 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.463 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.464 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.465 +case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
1.466 + | _ => error "biegelinie.sml: Bsp 7.27 #12";
1.467 +
1.468 +*} ML {*
1.469 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.470 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.471 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.472 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.473 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.474 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.475 +case nxt of
1.476 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
1.477 + | _ => error "biegelinie.sml: Bsp 7.27 #13";
1.478 +
1.479 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.480 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.481 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.482 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.483 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.484 + | _ => error "biegelinie.sml: Bsp 7.27 #14";
1.485 +
1.486 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.487 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.488 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.489 +case nxt of
1.490 + (_, Check_Postcond ["named", "integrate", "function"]) => ()
1.491 + | _ => error "biegelinie.sml: Bsp 7.27 #15";
1.492 +
1.493 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.494 +if f2str f =
1.495 + "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
1.496 +then () else error "biegelinie.sml: Bsp 7.27 #16 f";
1.497 +case nxt of
1.498 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
1.499 + | _ => error "biegelinie.sml: Bsp 7.27 #16";
1.500 +
1.501 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.502 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.503 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.504 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.505 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.506 + | _ => error "biegelinie.sml: Bsp 7.27 #17";
1.507 +
1.508 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.509 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.510 +if f2str f =
1.511 + "y x =\nc_2 + c * x +\n\
1.512 + \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
1.513 +then () else error "biegelinie.sml: Bsp 7.27 #18 f";
1.514 +case nxt of
1.515 + (_, Check_Postcond ["named", "integrate", "function"]) => ()
1.516 + | _ => error "biegelinie.sml: Bsp 7.27 #18";
1.517 +
1.518 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.519 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.520 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.521 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.522 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.523 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.524 +case nxt of
1.525 + (_, Subproblem
1.526 + ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()
1.527 + | _ => error "biegelinie.sml: Bsp 7.27 #19";
1.528 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.529 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.530 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.531 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.532 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.533 +case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
1.534 + | _ => error "biegelinie.sml: Bsp 7.27 #20";
1.535 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.536 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.537 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.538 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.539 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.540 +if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
1.541 +else error "biegelinie.sml: Bsp 7.27 #21 f";
1.542 +case nxt of
1.543 + (_, Subproblem
1.544 + ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
1.545 + | _ => error "biegelinie.sml: Bsp 7.27 #21";
1.546 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.547 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.548 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.549 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.550 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.551 +case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
1.552 + | _ => error "biegelinie.sml: Bsp 7.27 #22";
1.553 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.554 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.555 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.556 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.557 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.558 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.559 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.560 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.561 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.562 +case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
1.563 + | _ => error "biegelinie.sml: Bsp 7.27 #23";
1.564 +
1.565 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.566 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.567 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.568 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.569 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.570 +if f2str f =
1.571 + "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
1.572 + "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
1.573 +then () else error "biegelinie.sml: Bsp 7.27 #24 f";
1.574 +case nxt of ("End_Proof'", End_Proof') => ()
1.575 + | _ => error "biegelinie.sml: Bsp 7.27 #24";
1.576 +
1.577 +show_pt pt;
1.578 +(*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
1.579 +(([1], Frm), q_ x = q_0),
1.580 +(([1], Res), - q_ x = - q_0),
1.581 +(([2], Res), Q' x = - q_0),
1.582 +(([3], Pbl), Integrate (- q_0, x)),
1.583 +(([3,1], Frm), Q x = Integral - q_0 D x),
1.584 +(([3,1], Res), Q x = -1 * q_0 * x + c),
1.585 +(([3], Res), Q x = -1 * q_0 * x + c),
1.586 +(([4], Res), M_b' x = -1 * q_0 * x + c),
1.587 +(([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
1.588 +(([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
1.589 +(([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
1.590 +(([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
1.591 +(([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
1.592 +(([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
1.593 +(([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
1.594 +(([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
1.595 +(([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
1.596 +(([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
1.597 + 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
1.598 +(([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
1.599 +(([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
1.600 +(([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
1.601 +(([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
1.602 +(([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
1.603 +(([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
1.604 +(([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
1.605 +(([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
1.606 +(([10,4,4], Res), c = L * q_0 / 2),
1.607 +(([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.608 +(([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
1.609 +(([10], Res), [c = L * q_0 / 2, c_2 = 0]),
1.610 +(([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
1.611 +(([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
1.612 +(([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
1.613 +(([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
1.614 +(([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
1.615 +(([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
1.616 +(([15,1], Res), y' x =
1.617 +(Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
1.618 +c)]*)
1.619 +
1.620 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.621 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.622 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.623 + reset_states ();
1.624 + CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.625 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.626 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.627 + "FunktionsVariable x"],
1.628 + ("Biegelinie",
1.629 + ["MomentBestimmte","Biegelinien"],
1.630 + ["IntegrierenUndKonstanteBestimmen"]))];
1.631 + moveActiveRoot 1;
1.632 + autoCalculate 1 CompleteCalcHead;
1.633 +
1.634 + fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
1.635 +(*
1.636 +> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
1.637 +val it = true : bool
1.638 +*)
1.639 + autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
1.640 + val ((pt,_),_) = get_calc 1;
1.641 + case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.642 + | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
1.643 +
1.644 + autoCalculate 1 CompleteCalc;
1.645 +val ((pt,p),_) = get_calc 1;
1.646 +if p = ([], Res) andalso length (children pt) = 23 andalso
1.647 +term2str (get_obj g_res pt (fst p)) =
1.648 +"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)"
1.649 +then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.650 +
1.651 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.652 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.653 + show_pt pt;
1.654 +
1.655 +(*check all formulae for getTactic*)
1.656 + getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
1.657 + getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
1.658 + getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
1.659 + getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
1.660 + getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
1.661 + getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
1.662 +
1.663 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.664 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.665 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.666 +val fmz =
1.667 + ["Streckenlast q_0","FunktionsVariable x",
1.668 + "Funktionen [Q x = c + -1 * q_0 * x, \
1.669 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
1.670 + \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
1.671 + \ 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)]"];
1.672 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
1.673 + ["Biegelinien","ausBelastung"]);
1.674 +val p = e_pos'; val c = [];
1.675 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.676 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.677 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.678 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.679 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.680 +case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
1.681 +| _ => error "biegelinie.sml met2 b";
1.682 +
1.683 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
1.684 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
1.685 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
1.686 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
1.687 +| _ => error "biegelinie.sml met2 c";
1.688 +
1.689 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.690 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.691 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.692 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.693 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.694 +
1.695 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.696 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.697 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
1.698 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
1.699 +| _ => error "biegelinie.sml met2 d";
1.700 +
1.701 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.702 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.703 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.704 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.705 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.706 + "M_b x = Integral c + -1 * q_0 * x D x";
1.707 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.708 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.709 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.710 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.711 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.712 + "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.713 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.714 + "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
1.715 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.716 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.717 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.718 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.719 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.720 + "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.721 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.722 +"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.723 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.724 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.725 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.726 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.727 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.728 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.729 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.730 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.731 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.732 +"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";
1.733 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.734 +"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)";
1.735 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.736 + "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)";
1.737 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.738 +if f2str f =
1.739 + "[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)]"
1.740 +then case nxt of ("End_Proof'", End_Proof') => ()
1.741 + | _ => error "biegelinie.sml met2 e 1"
1.742 +else error "biegelinie.sml met2 e 2";
1.743 +
1.744 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.745 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.746 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.747 +val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
1.748 + "substitution (M_b L = 0)",
1.749 + "equality equ_equ"];
1.750 +val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
1.751 + ["Equation","fromFunction"]);
1.752 +val p = e_pos'; val c = [];
1.753 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.754 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.755 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.756 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.757 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.758 +
1.759 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.760 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.761 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.762 + "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.763 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.764 + "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.765 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.766 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.767 +if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
1.768 + f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
1.769 +then case nxt of ("End_Proof'", End_Proof') => ()
1.770 + | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
1.771 +else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
1.772 +*} ML {*
1.773 +*}
1.774 +
1.775 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)
1.776 ML_file "Knowledge/algein.sml"
1.777 ML_file "Knowledge/diophanteq.sml"