1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,1040 @@
1.4 +(* tests on biegelinie
1.5 + author: Walther Neuper 050826
1.6 + (c) due to copyright terms
1.7 +
1.8 +use"../smltest/IsacKnowledge/biegelinie.sml";
1.9 +use"biegelinie.sml";
1.10 +*)
1.11 +val thy = Biegelinie.thy;
1.12 +
1.13 +"-----------------------------------------------------------------";
1.14 +"table of contents -----------------------------------------------";
1.15 +"-----------------------------------------------------------------";
1.16 +"----------- the rules -------------------------------------------";
1.17 +"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
1.18 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.19 +"----------- simplify_leaf for this script -----------------------";
1.20 +"----------- Bsp 7.27 me -----------------------------------------";
1.21 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.22 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.23 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.24 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.25 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
1.26 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
1.27 +"----------- investigate normalforms in biegelinien --------------";
1.28 +"-----------------------------------------------------------------";
1.29 +"-----------------------------------------------------------------";
1.30 +"-----------------------------------------------------------------";
1.31 +
1.32 +
1.33 +"----------- the rules -------------------------------------------";
1.34 +"----------- the rules -------------------------------------------";
1.35 +"----------- the rules -------------------------------------------";
1.36 +fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
1.37 +fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
1.38 +fun rewrit thm str =
1.39 + fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
1.40 +
1.41 +val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
1.42 +if term2s t = "Q' x = - q_0" then ()
1.43 +else raise error "/biegelinie.sml: Belastung_Querkraft";
1.44 +
1.45 +val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t;
1.46 +if term2s t = "M_b' x = - q_0 * x + c" then ()
1.47 +else raise error "/biegelinie.sml: Querkraft_Moment";
1.48 +
1.49 +val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.50 + term2s t;
1.51 +if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
1.52 +else raise error "biegelinie.sml: Moment_Neigung";
1.53 +
1.54 +
1.55 +"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
1.56 +"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
1.57 +"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
1.58 +val str =
1.59 +"Script BiegelinieScript \
1.60 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.61 +\(rb_::bool list) (rm_::bool list) = \
1.62 +\ (let q___ = Take (q_ v_ = q__); \
1.63 +\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.64 +\ (Rewrite Belastung_Querkraft True)) q___; \
1.65 +\ (Q__:: bool) = \
1.66 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.67 +\ [diff,integration,named]) \
1.68 +\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
1.69 +\ Q__ = Rewrite Querkraft_Moment True Q__; \
1.70 +\ (M__::bool) = \
1.71 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.72 +\ [diff,integration,named]) \
1.73 +\ [real_ (rhs Q__), real_ v_, real_real_ M_b]); \
1.74 +\ e1__ = nth_ 1 rm_; \
1.75 +\ (x1__::real) = argument_in (lhs e1__); \
1.76 +\ (M1__::bool) = (Substitute [v_ = x1__]) M__; \
1.77 +\ M1__ = (Substitute [e1__]) M1__ ; \
1.78 +\ M2__ = Take M__; "^
1.79 +(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
1.80 +" e2__ = nth_ 2 rm_; \
1.81 +\ (x2__::real) = argument_in (lhs e2__); \
1.82 +\ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \
1.83 +\ (Substitute [e2__])) M2__; \
1.84 +\ (c_1_2__::bool list) = \
1.85 +\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.86 +\ [booll_ [M1__, M2__], reall [c,c_2]]); \
1.87 +\ M__ = Take M__; \
1.88 +\ M__ = ((Substitute c_1_2__) @@ \
1.89 +\ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\
1.90 +\ simplify_System False)) @@ \
1.91 +\ (Rewrite Moment_Neigung False) @@ \
1.92 +\ (Rewrite make_fun_explicit False)) M__; "^
1.93 +(*----------------------- and the same once more ------------------------*)
1.94 +" (N__:: bool) = \
1.95 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.96 +\ [diff,integration,named]) \
1.97 +\ [real_ (rhs M__), real_ v_, real_real_ y']); \
1.98 +\ (B__:: bool) = \
1.99 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.100 +\ [diff,integration,named]) \
1.101 +\ [real_ (rhs N__), real_ v_, real_real_ y]); \
1.102 +\ e1__ = nth_ 1 rb_; \
1.103 +\ (x1__::real) = argument_in (lhs e1__); \
1.104 +\ (B1__::bool) = (Substitute [v_ = x1__]) B__; \
1.105 +\ B1__ = (Substitute [e1__]) B1__ ; \
1.106 +\ B2__ = Take B__; \
1.107 +\ e2__ = nth_ 2 rb_; \
1.108 +\ (x2__::real) = argument_in (lhs e2__); \
1.109 +\ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \
1.110 +\ (Substitute [e2__])) B2__; \
1.111 +\ (c_1_2__::bool list) = \
1.112 +\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.113 +\ [booll_ [B1__, B2__], reall [c,c_2]]); \
1.114 +\ B__ = Take B__; \
1.115 +\ B__ = ((Substitute c_1_2__) @@ \
1.116 +\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
1.117 +\ in B__)"
1.118 +;
1.119 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.120 +(*---^^^-OK-----------------------------------------------------------------*)
1.121 +(*---vvv-NOTok--------------------------------------------------------------*)
1.122 +atomty sc;
1.123 +atomt sc;
1.124 +
1.125 +(* use"../smltest/IsacKnowledge/biegelinie.sml";
1.126 + *)
1.127 +
1.128 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.129 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.130 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.131 +val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
1.132 +val t = rewrit Moment_Neigung t; term2s t;
1.133 +(*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
1.134 + ### before declaring "y''" as a constant *)
1.135 +val t = rewrit make_fun_explicit t; term2s t;
1.136 +
1.137 +
1.138 +"----------- simplify_leaf for this script -----------------------";
1.139 +"----------- simplify_leaf for this script -----------------------";
1.140 +"----------- simplify_leaf for this script -----------------------";
1.141 +val srls = Rls {id="srls_IntegrierenUnd..",
1.142 + preconds = [],
1.143 + rew_ord = ("termlessI",termlessI),
1.144 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.145 + [(*for asm in nth_Cons_ ...*)
1.146 + Calc ("op <",eval_equ "#less_"),
1.147 + (*2nd nth_Cons_ pushes n+-1 into asms*)
1.148 + Calc("op +", eval_binop "#add_")
1.149 + ],
1.150 + srls = Erls, calc = [],
1.151 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.152 + Calc("op +", eval_binop "#add_"),
1.153 + Thm ("nth_Nil_",num_str nth_Nil_),
1.154 + Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.155 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.156 + Calc("Atools.argument'_in",
1.157 + eval_argument_in "Atools.argument'_in")
1.158 + ],
1.159 + scr = EmptyScr};
1.160 +val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
1.161 +val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
1.162 +val SOME (e1__,_) =
1.163 + rewrite_set_ thy false srls
1.164 + (str2term"(nth_::[real,bool list]=>bool) 1 " $ rm_);
1.165 +if term2str e1__ = "M_b 0 = 0" then ()
1.166 +else raise error "biegelinie.sml simplify nth_ 1 rm_";
1.167 +
1.168 +val SOME (x1__,_) =
1.169 + rewrite_set_ thy false srls
1.170 + (str2term"argument_in (lhs (M_b 0 = 0))");
1.171 +if term2str x1__ = "0" then ()
1.172 +else raise error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
1.173 +
1.174 +trace_rewrite:=true;
1.175 +trace_rewrite:=false;
1.176 +
1.177 +
1.178 +
1.179 +"----------- Bsp 7.27 me -----------------------------------------";
1.180 +"----------- Bsp 7.27 me -----------------------------------------";
1.181 +"----------- Bsp 7.27 me -----------------------------------------";
1.182 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.183 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.184 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.185 + "FunktionsVariable x"];
1.186 +val (dI',pI',mI') =
1.187 + ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
1.188 + ["IntegrierenUndKonstanteBestimmen"]);
1.189 +val p = e_pos'; val c = [];
1.190 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.191 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.192 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.193 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.194 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.195 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.196 +
1.197 +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
1.198 +(*if itms2str_ ctxt pits = ... all 5 model-items*)
1.199 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
1.200 +if itms2str_ ctxt mits = "[]" then ()
1.201 +else raise error "biegelinie.sml: Bsp 7.27 #2";
1.202 +
1.203 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.204 +case nxt of (_,Add_Given "FunktionsVariable x") => ()
1.205 + | _ => raise error "biegelinie.sml: Bsp 7.27 #4a";
1.206 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.207 +val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
1.208 +(*if itms2str_ ctxt mits = ... all 6 guard-items*)
1.209 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.210 + | _ => raise error "biegelinie.sml: Bsp 7.27 #4b";
1.211 +
1.212 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.213 +case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.214 + | _ => raise error "biegelinie.sml: Bsp 7.27 #4c";
1.215 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.216 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.217 +
1.218 +case nxt of
1.219 + (_,Subproblem ("Biegelinie.thy", ["named", "integrate", "function"])) => ()
1.220 + | _ => raise error "biegelinie.sml: Bsp 7.27 #4c";
1.221 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.222 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.223 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.224 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.225 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.226 + | _ => raise error "biegelinie.sml: Bsp 7.27 #5";
1.227 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.228 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.229 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.230 +case nxt of
1.231 + ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
1.232 + | _ => raise error "biegelinie.sml: Bsp 7.27 #5a";
1.233 +
1.234 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.235 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.236 +case nxt of
1.237 + (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
1.238 + | _ => raise error "biegelinie.sml: Bsp 7.27 #5b";
1.239 +
1.240 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.241 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.242 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.243 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.244 +case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
1.245 + | _ => raise error "biegelinie.sml: Bsp 7.27 #6";
1.246 +
1.247 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.248 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
1.249 +f2str f;
1.250 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.251 +case nxt of (_, Substitute ["x = 0"]) => ()
1.252 + | _ => raise error "biegelinie.sml: Bsp 7.27 #7";
1.253 +
1.254 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.255 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.256 +if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
1.257 +else raise error "biegelinie.sml: Bsp 7.27 #8";
1.258 +
1.259 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.260 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.261 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.262 +if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
1.263 +else raise error "biegelinie.sml: Bsp 7.27 #9";
1.264 +
1.265 +(*val nxt = (+, Subproblem ("Biegelinie.thy", ["normalize", ..lin..sys]))*)
1.266 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.267 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.268 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.269 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.270 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.271 +case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
1.272 + | _ => raise error "biegelinie.sml: Bsp 7.27 #10";
1.273 +
1.274 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.275 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.276 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.277 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.278 +(*val nxt = Subproblem ["triangular", "2x2", "linear", "system"]*)
1.279 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.280 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.281 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.282 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.283 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.284 +case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
1.285 + | _ => raise error "biegelinie.sml: Bsp 7.27 #11";
1.286 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.287 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.288 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.289 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.290 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.291 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.292 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.293 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.294 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.295 +case nxt of (_, Check_Postcond ["normalize", "2x2", "linear", "system"]) => ()
1.296 + | _ => raise error "biegelinie.sml: Bsp 7.27 #12";
1.297 +
1.298 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.299 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.300 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.301 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.302 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.303 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.304 +case nxt of
1.305 + (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
1.306 + | _ => raise error "biegelinie.sml: Bsp 7.27 #13";
1.307 +
1.308 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.309 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.310 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.311 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.312 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.313 + | _ => raise error "biegelinie.sml: Bsp 7.27 #14";
1.314 +
1.315 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.316 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.317 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.318 +case nxt of
1.319 + (_, Check_Postcond ["named", "integrate", "function"]) => ()
1.320 + | _ => raise error "biegelinie.sml: Bsp 7.27 #15";
1.321 +
1.322 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.323 +if f2str f =
1.324 + "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
1.325 +then () else raise error "biegelinie.sml: Bsp 7.27 #16 f";
1.326 +case nxt of
1.327 + (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
1.328 + | _ => raise error "biegelinie.sml: Bsp 7.27 #16";
1.329 +
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 + | _ => raise error "biegelinie.sml: Bsp 7.27 #17";
1.336 +
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 +if f2str f =
1.340 + "y x =\nc_2 + c * x +\n\
1.341 + \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
1.342 +then () else raise error "biegelinie.sml: Bsp 7.27 #18 f";
1.343 +case nxt of
1.344 + (_, Check_Postcond ["named", "integrate", "function"]) => ()
1.345 + | _ => raise error "biegelinie.sml: Bsp 7.27 #18";
1.346 +
1.347 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.348 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.349 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.350 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.351 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.352 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.353 +case nxt of
1.354 + (_, Subproblem
1.355 + ("Biegelinie.thy", ["normalize", "2x2", "linear", "system"])) => ()
1.356 + | _ => raise error "biegelinie.sml: Bsp 7.27 #19";
1.357 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.358 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.359 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.360 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.361 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.362 +case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
1.363 + | _ => raise error "biegelinie.sml: Bsp 7.27 #20";
1.364 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.368 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.369 +if f2str f = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
1.370 +else raise error "biegelinie.sml: Bsp 7.27 #21 f";
1.371 +case nxt of
1.372 + (_, Subproblem
1.373 + ("Biegelinie.thy", ["triangular", "2x2", "linear", "system"])) =>()
1.374 + | _ => raise error "biegelinie.sml: Bsp 7.27 #21";
1.375 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.376 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.377 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.378 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.379 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.380 +case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
1.381 + | _ => raise error "biegelinie.sml: Bsp 7.27 #22";
1.382 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.383 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.384 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.385 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.386 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.387 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.388 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.389 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.390 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.391 +case nxt of (_, Check_Postcond ["normalize", "2x2", "linear", "system"]) => ()
1.392 + | _ => raise error "biegelinie.sml: Bsp 7.27 #23";
1.393 +
1.394 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.395 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.396 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.397 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.398 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.399 +if f2str f =
1.400 +"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
1.401 + \(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n\
1.402 + \ -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)" then ()
1.403 +else raise error "biegelinie.sml: Bsp 7.27 #24 f";
1.404 +case nxt of ("End_Proof'", End_Proof') => ()
1.405 + | _ => raise error "biegelinie.sml: Bsp 7.27 #24";
1.406 +
1.407 +(* use"../smltest/IsacKnowledge/biegelinie.sml";
1.408 + *)
1.409 +show_pt pt;
1.410 +(*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
1.411 +(([1], Frm), q_ x = q_0),
1.412 +(([1], Res), - q_ x = - q_0),
1.413 +(([2], Res), Q' x = - q_0),
1.414 +(([3], Pbl), Integrate (- q_0, x)),
1.415 +(([3,1], Frm), Q x = Integral - q_0 D x),
1.416 +(([3,1], Res), Q x = -1 * q_0 * x + c),
1.417 +(([3], Res), Q x = -1 * q_0 * x + c),
1.418 +(([4], Res), M_b' x = -1 * q_0 * x + c),
1.419 +(([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
1.420 +(([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
1.421 +(([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
1.422 +(([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
1.423 +(([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
1.424 +(([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
1.425 +(([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
1.426 +(([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
1.427 +(([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
1.428 +(([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
1.429 + 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
1.430 +(([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
1.431 +(([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
1.432 +(([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
1.433 +(([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
1.434 +(([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
1.435 +(([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
1.436 +(([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
1.437 +(([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
1.438 +(([10,4,4], Res), c = L * q_0 / 2),
1.439 +(([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.440 +(([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
1.441 +(([10], Res), [c = L * q_0 / 2, c_2 = 0]),
1.442 +(([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
1.443 +(([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
1.444 +(([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
1.445 +(([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
1.446 +(([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
1.447 +(([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
1.448 +(([15,1], Res), y' x =
1.449 +(Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
1.450 +c)]*)
1.451 +
1.452 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.453 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.454 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.455 + states:=[];
1.456 + CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.457 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.458 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.459 + "FunktionsVariable x"],
1.460 + ("Biegelinie.thy",
1.461 + ["MomentBestimmte","Biegelinien"],
1.462 + ["IntegrierenUndKonstanteBestimmen"]))];
1.463 + moveActiveRoot 1;
1.464 + autoCalculate 1 CompleteCalcHead;
1.465 +
1.466 + fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
1.467 +(*
1.468 +> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
1.469 +> is = e_scrstate;
1.470 +val it = true : bool
1.471 +*)
1.472 + autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
1.473 + val ((pt,_),_) = get_calc 1;
1.474 + case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.475 + | _ => raise error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
1.476 +
1.477 + autoCalculate 1 CompleteCalc;
1.478 +val ((pt,p),_) = get_calc 1;
1.479 +if p = ([], Res) andalso length (children pt) = 23 andalso
1.480 +term2str (get_obj g_res pt (fst p)) =
1.481 +"y x =\n-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.482 +then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
1.483 +
1.484 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.485 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.486 + show_pt pt;
1.487 +
1.488 +(*check all formulae for getTactic*)
1.489 + getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
1.490 + getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
1.491 + getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
1.492 + getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
1.493 + getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
1.494 + getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
1.495 +
1.496 +
1.497 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.498 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.499 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.500 +val fmz =
1.501 + ["Streckenlast q_0","FunktionsVariable x",
1.502 + "Funktionen [Q x = c + -1 * q_0 * x, \
1.503 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
1.504 + \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
1.505 + \ 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.506 +val (dI',pI',mI') = ("Biegelinie.thy", ["vonBelastungZu","Biegelinien"],
1.507 + ["Biegelinien","ausBelastung"]);
1.508 +val p = e_pos'; val c = [];
1.509 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.510 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.511 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.512 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.513 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.514 +if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
1.515 +then () else raise error "biegelinie.sml met2 b";
1.516 +
1.517 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
1.518 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
1.519 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
1.520 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
1.521 +| _ => raise error "biegelinie.sml met2 c";
1.522 +
1.523 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.524 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.525 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.526 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.527 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.528 +
1.529 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.530 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.531 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
1.532 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
1.533 +| _ => raise error "biegelinie.sml met2 d";
1.534 +
1.535 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.536 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.537 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.538 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.539 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.540 + "M_b x = Integral c + -1 * q_0 * x D x";
1.541 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.542 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.543 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.544 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.545 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.546 + "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.547 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.548 + "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.551 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.552 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.553 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.554 + "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.555 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.556 +"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.557 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.558 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.559 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.560 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.561 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.562 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.563 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.564 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.565 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.566 +"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.567 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.568 +"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.569 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.570 + "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.571 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.572 +if nxt = ("End_Proof'", End_Proof') andalso f2str f =
1.573 + "[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)]" then ()
1.574 +else raise error "biegelinie.sml met2 e";
1.575 +
1.576 +
1.577 +
1.578 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.579 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.580 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.581 +val str =
1.582 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.583 +\(equ___::bool)"
1.584 +;
1.585 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.586 +val str =
1.587 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.588 +\ (let v_ = argument_in (lhs fun_)\
1.589 +\ in (equ___::bool))"
1.590 +;
1.591 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.592 +val str =
1.593 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.594 +\ (let v_ = argument_in (lhs fun_);\
1.595 +\ (equ_) = (Substitute [sub_]) fun_\
1.596 +\ in (equ_::bool))"
1.597 +;
1.598 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.599 +val str =
1.600 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.601 +\ (let v_ = argument_in (lhs fun_);\
1.602 +\ equ_ = (Substitute [sub_]) fun_\
1.603 +\ in (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False) equ_)"
1.604 +;
1.605 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.606 +(*---^^^-OK-----------------------------------------------------------------*)
1.607 +val str =
1.608 +(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.609 + 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.610 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.611 +\ (let bdv_ = argument_in (lhs fun_);\
1.612 +\ val_ = argument_in (lhs sub_);\
1.613 +\ equ_ = (Substitute [bdv_ = val_]) fun_;\
1.614 +\ equ_ = (Substitute [sub_]) fun_\
1.615 +\ in (Rewrite_Set_Inst [(bdv_, v_)] make_ratpoly_in False) equ_)"
1.616 +;
1.617 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.618 +(*---vvv-NOTok--------------------------------------------------------------*)
1.619 +atomty sc;
1.620 +
1.621 +val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
1.622 + "substitution (M_b L = 0)",
1.623 + "equality equ___"];
1.624 +val (dI',pI',mI') = ("Biegelinie.thy", ["makeFunctionTo","equation"],
1.625 + ["Equation","fromFunction"]);
1.626 +val p = e_pos'; val c = [];
1.627 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.628 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.629 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.630 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.631 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.632 +
1.633 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.634 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.635 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.636 + "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.637 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.638 + "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.639 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.640 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.641 +if nxt = ("End_Proof'", End_Proof') andalso
1.642 +(* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2"
1.643 +CHANGE NOT considered, already on leave*)
1.644 + f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
1.645 +then () else raise error "biegelinie.sml: SubProblem (_,[setzeRandbed";
1.646 +
1.647 +
1.648 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.649 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.650 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.651 +"----- check the scripts syntax";
1.652 +val str =
1.653 +"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
1.654 +\ (let b1 = Take (nth_ 1 beds_)\
1.655 +\ in (equs_::bool list))"
1.656 +;
1.657 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.658 +val str =
1.659 +"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
1.660 +\ (let b1_ = Take (nth_ 1 beds_); \
1.661 +\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.662 +\ f1_ = hd fs_ \
1.663 +\ in (equs_::bool list))"
1.664 +;
1.665 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.666 +
1.667 +val ttt = str2term "sameFunId (lhs b1_) fun___"; atomty ttt;
1.668 +val ttt = str2term "filter"; atomty ttt;
1.669 +val ttt = str2term "filter::[real => bool, real list] => real list";atomty ttt;
1.670 +val ttt = str2term "filter::[bool => bool, bool list] => bool list";
1.671 +val ttt = str2term "filter (sameFunId (lhs b1_)) funs_"; atomty ttt;
1.672 +
1.673 +val str =
1.674 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
1.675 +\ (let beds_ = rev beds_; \
1.676 +\ b1_ = Take (nth_ 1 beds_); \
1.677 +\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.678 +\ f1_ = hd fs_ \
1.679 +\ in (equs_::bool list))"
1.680 +;
1.681 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.682 +val str =
1.683 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
1.684 +\ (let b1_ = Take (nth_ 1 rb_); \
1.685 +\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.686 +\ (equ_::bool) = \
1.687 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.688 +\ [Equation,fromFunction]) \
1.689 +\ [bool_ (hd fs_), bool_ b1_]) \
1.690 +\ in [equ_])"
1.691 +;
1.692 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.693 +val str =
1.694 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
1.695 +\ (let b1_ = Take (nth_ 1 rb_); \
1.696 +\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.697 +\ (e1_::bool) = \
1.698 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.699 +\ [Equation,fromFunction]) \
1.700 +\ [bool_ (hd fs_), bool_ b1_]); \
1.701 +\ b2_ = Take (nth_ 2 rb_); \
1.702 +\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
1.703 +\ (e2_::bool) = \
1.704 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.705 +\ [Equation,fromFunction]) \
1.706 +\ [bool_ (hd fs_), bool_ b2_]) \
1.707 +\ in [e1_,e1_])"
1.708 +;
1.709 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.710 +(*---vvv-NOTok--------------------------------------------------------------*)
1.711 +(*---^^^-OK-----------------------------------------------------------------*)
1.712 +atomty sc;
1.713 +
1.714 +"----- execute script by manual rewriting";
1.715 +(*show_types := true;*)
1.716 +val funs_ = str2term "funs_::bool list";
1.717 +val funs = str2term
1.718 + "[Q x = c + -1 * q_0 * x,\
1.719 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
1.720 + \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
1.721 + \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.722 +val rb_ = str2term "rb_::bool list";
1.723 +val rb = str2term "[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]";
1.724 +
1.725 +"--- script expression 1";
1.726 +val screxp1_ = str2term "Take (nth_ 1 (rb_::bool list))";
1.727 +val screxp1 = subst_atomic [(rb_, rb)] screxp1_; term2str screxp1;
1.728 +val SOME (b1,_) = rewrite_set_ Isac.thy false srls2 screxp1; term2str b1;
1.729 +if term2str b1 = "Take (y 0 = 0)" then ()
1.730 +else raise error "biegelinie.sml: rew. Bieglie2 --1";
1.731 +val b1 = str2term "(y 0 = 0)";
1.732 +
1.733 +"--- script expression 2";
1.734 +val screxp2_ = str2term "filter (sameFunId (lhs b1_)) funs_";
1.735 +val b1_ = str2term "b1_::bool";
1.736 +val screxp2 = subst_atomic [(b1_,b1),(funs_,funs)] screxp2_; term2str screxp2;
1.737 +val SOME (fs,_) = rewrite_set_ Isac.thy false srls2 screxp2; term2str fs;
1.738 +if term2str fs = "[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)]" then ()
1.739 +else raise error "biegelinie.sml: rew. Bieglie2 --2";
1.740 +
1.741 +"--- script expression 3";
1.742 +val screxp3_ = str2term "SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.743 +\ [Equation,fromFunction]) \
1.744 +\ [bool_ (hd fs_), bool_ b1_]";
1.745 +val fs_ = str2term "fs_::bool list";
1.746 +val screxp3 = subst_atomic [(fs_,fs),(b1_,b1)] screxp3_;
1.747 +writeln (term2str screxp3);
1.748 +val SOME (equ,_) = rewrite_set_ Isac.thy false srls2 screxp3;
1.749 +if term2str equ = "SubProblem\n (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])\n [bool_\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 bool_ (y 0 = 0)]" then ()
1.750 +else raise error "biegelinie.sml: rew. Bieglie2 --3";
1.751 +writeln (term2str equ);
1.752 +(*SubProblem
1.753 + (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])
1.754 + [bool_
1.755 + (y x =
1.756 + c_4 + c_3 * x +
1.757 + 1 / (-1 * EI) *
1.758 + (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
1.759 + bool_ (y 0 = 0)]*)
1.760 +show_types := false;
1.761 +
1.762 +
1.763 +"----- execute script by interpreter: setzeRandbedingungenEin";
1.764 +val fmz = ["Funktionen [Q x = c + -1 * q_0 * x,\
1.765 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
1.766 + \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
1.767 + \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.768 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
1.769 + "Gleichungen equs___"];
1.770 +val (dI',pI',mI') = ("Biegelinie.thy", ["setzeRandbedingungen","Biegelinien"],
1.771 + ["Biegelinien","setzeRandbedingungenEin"]);
1.772 +val p = e_pos'; val c = [];
1.773 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.774 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.775 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.776 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.777 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.778 +
1.779 +"--- before 1.subpbl [Equation, fromFunction]";
1.780 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.781 +case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
1.782 +| _ => raise error "biegelinie.sml: met setzeRandbed*Ein aa";
1.783 +"----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
1.784 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.785 +if (#1 o (get_obj g_fmz pt)) (fst p) =
1.786 + ["functionEq\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.787 + "substitution (y 0 = 0)", "equality equ___"] then ()
1.788 +else raise error "biegelinie.sml met setzeRandbed*Ein bb";
1.789 +(writeln o istate2str) (get_istate pt p);
1.790 +"--- after 1.subpbl [Equation, fromFunction]";
1.791 +
1.792 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.793 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.794 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.795 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.796 +case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
1.797 +| _ => raise error "biegelinie.sml met2 ff";
1.798 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.799 + "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.800 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.801 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.802 +case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
1.803 +| _ => raise error "biegelinie.sml met2 gg";
1.804 +
1.805 +"--- before 2.subpbl [Equation, fromFunction]";
1.806 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)" ;
1.807 +case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
1.808 +| _ => raise error "biegelinie.sml met2 hh";
1.809 +"--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
1.810 +
1.811 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.812 +if (#1 o (get_obj g_fmz pt)) (fst p) =
1.813 + ["functionEq\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.814 + "substitution (y L = 0)", "equality equ___"] then ()
1.815 +else raise error "biegelinie.sml metsetzeRandbed*Ein bb ";
1.816 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.817 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.818 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.819 +
1.820 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.821 +case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
1.822 +| _ => raise error "biegelinie.sml met2 ii";
1.823 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "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.824 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y L =\nc_4 + c_3 * L +\n1 / (-1 * EI) *\n(c_2 / 2 * L ^^^ 2 + c / 6 * L ^^^ 3 + -1 * q_0 / 24 * L ^^^ 4)";
1.825 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + c_3 * L +\n1 / (-1 * EI) *\n(c_2 / 2 * L ^^^ 2 + c / 6 * L ^^^ 3 + -1 * q_0 / 24 * L ^^^ 4)";
1.826 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI)" ;
1.827 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI)";
1.828 +case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
1.829 +| _ => raise error "biegelinie.sml met2 jj";
1.830 +
1.831 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.832 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.833 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.834 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.835 +case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
1.836 +| _ => raise error "biegelinie.sml met2 kk";
1.837 +
1.838 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"(*true*);
1.839 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2";
1.840 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
1.841 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
1.842 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.843 +case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
1.844 +| _ => raise error "biegelinie.sml met2 ll";
1.845 +
1.846 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.847 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.848 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.849 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.850 +case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
1.851 +| _ => raise error "biegelinie.sml met2 mm";
1.852 +
1.853 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.854 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.855 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.856 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
1.857 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
1.858 +case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
1.859 +| _ => raise error "biegelinie.sml met2 nn";
1.860 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.861 +if nxt = ("End_Proof'", End_Proof') andalso f2str f =
1.862 +(* "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" *)
1.863 +"[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /\n (-1 * EI * 24),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
1.864 +then () else raise error "biegelinie.sml met2 oo";
1.865 +
1.866 +(*
1.867 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.868 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.869 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.870 +*)
1.871 +
1.872 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
1.873 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
1.874 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
1.875 +(*---^^^-OK-----------------------------------------------------------------*)
1.876 +(*---vvv-NOTok--------------------------------------------------------------*)
1.877 +val str =
1.878 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
1.879 +\ (let b1_ = nth_ 1 rb_; \
1.880 +\ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
1.881 +\ (e1_::bool) = \
1.882 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.883 +\ [Equation,fromFunction]) \
1.884 +\ [bool_ (hd fs_), bool_ b1_]) \
1.885 +\ in [e1_,e2_,e3_,e4_])"
1.886 +;
1.887 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.888 +(*---vvv-NOTok--------------------------------------------------------------*)
1.889 +val str =
1.890 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
1.891 +\ (let b1_ = nth_ 1 rb_; \
1.892 +\ fs_ = filter_sameFunId (lhs b1_) funs_; \
1.893 +\ (e1_::bool) = \
1.894 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.895 +\ [Equation,fromFunction]) \
1.896 +\ [bool_ (hd fs_), bool_ b1_]); \
1.897 +\ b2_ = nth_ 2 rb_; \
1.898 +\ fs_ = filter_sameFunId (lhs b2_) funs_; \
1.899 +\ (e2_::bool) = \
1.900 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.901 +\ [Equation,fromFunction]) \
1.902 +\ [bool_ (hd fs_), bool_ b2_]); \
1.903 +\ b3_ = nth_ 3 rb_; \
1.904 +\ fs_ = filter_sameFunId (lhs b3_) funs_; \
1.905 +\ (e3_::bool) = \
1.906 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.907 +\ [Equation,fromFunction]) \
1.908 +\ [bool_ (hd fs_), bool_ b3_]); \
1.909 +\ b4_ = nth_ 4 rb_; \
1.910 +\ fs_ = filter_sameFunId (lhs b4_) funs_; \
1.911 +\ (e4_::bool) = \
1.912 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.913 +\ [Equation,fromFunction]) \
1.914 +\ [bool_ (hd fs_), bool_ b4_]) \
1.915 +\ in [e1_,e2_,e3_,e4_])"
1.916 +;
1.917 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.918 +
1.919 +
1.920 +
1.921 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
1.922 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
1.923 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
1.924 +"----- script ";
1.925 +val str =
1.926 +"Script Belastung2BiegelScript (q__::real) (v_::real) = \
1.927 +\ (let q___ = Take (q_ v_ = q__); \
1.928 +\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.929 +\ (Rewrite Belastung_Querkraft True)) q___; \
1.930 +\ (Q__:: bool) = \
1.931 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.932 +\ [diff,integration,named]) \
1.933 +\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
1.934 +\ M__ = Rewrite Querkraft_Moment True Q__; \
1.935 +\ (M__::bool) = \
1.936 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.937 +\ [diff,integration,named]) \
1.938 +\ [real_ (rhs M__), real_ v_, real_real_ M_b]); \
1.939 +\ N__ = ((Rewrite Moment_Neigung False) @@ \
1.940 +\ (Rewrite make_fun_explicit False)) M__; \
1.941 +\ (N__:: bool) = \
1.942 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.943 +\ [diff,integration,named]) \
1.944 +\ [real_ (rhs N__), real_ v_, real_real_ y']); \
1.945 +\ (B__:: bool) = \
1.946 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.947 +\ [diff,integration,named]) \
1.948 +\ [real_ (rhs N__), real_ v_, real_real_ y]) \
1.949 +\ in [Q__, M__, N__, B__])"
1.950 +;
1.951 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.952 +(*---^^^-OK-----------------------------------------------------------------*)
1.953 +(*---vvv-NOTok--------------------------------------------------------------*)
1.954 +
1.955 +
1.956 +"----- Bsp 7.70 with me";
1.957 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.958 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
1.959 + "FunktionsVariable x"];
1.960 +val (dI',pI',mI') = ("Biegelinie.thy", ["Biegelinien"],
1.961 + ["IntegrierenUndKonstanteBestimmen2"]);
1.962 +val p = e_pos'; val c = [];
1.963 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.964 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.965 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.966 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.967 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.968 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.969 +if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
1.970 +then () else raise error "biegelinie.sml met2 a";
1.971 +
1.972 +(*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
1.973 +... THIS MEANS:
1.974 +#a# "Script Biegelinie2Script ..
1.975 +\ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
1.976 +\ [Biegelinien,ausBelastung]) \
1.977 +\ [real_ q__, real_ v_]); \
1.978 +
1.979 +#b# prep_met ... (["Biegelinien","ausBelastung"],
1.980 + ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.981 + "Script Belastung2BiegelScript (q__::real) (v_::real) = \
1.982 +
1.983 +#a#b# BOTH HAVE 2 ARGUMENTS q__ and v_ ...OK
1.984 +##########################################################################
1.985 +BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
1.986 +##########################################################################*)
1.987 +"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
1.988 +\ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
1.989 +
1.990 +"----- Bsp 7.70 with autoCalculate";
1.991 +states:=[];
1.992 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.993 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
1.994 + "FunktionsVariable x"],
1.995 + ("Biegelinie.thy", ["Biegelinien"],
1.996 + ["IntegrierenUndKonstanteBestimmen2"]))];
1.997 +moveActiveRoot 1;
1.998 +autoCalculate 1 CompleteCalc;
1.999 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1000 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
1.1001 +"y x =\n-6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +\n4 * L * q_0 / (-24 * EI) * x ^^^ 3 +\n-1 * q_0 / (-24 * EI) * x ^^^ 4" then ()
1.1002 +else raise error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
1.1003 +
1.1004 +val is = get_istate pt ([],Res); writeln (istate2str is);
1.1005 +val t = str2term " last \
1.1006 +\[Q x = L * q_0 + -1 * q_0 * x, \
1.1007 +\ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
1.1008 +\ y' x = \
1.1009 +\ -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +\
1.1010 +\ -1 * q_0 / (-6 * EI) * x ^^^ 3, \
1.1011 +\ y x = \
1.1012 +\ -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + \
1.1013 +\ 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
1.1014 +\ -1 * q_0 / (-24 * EI) * x ^^^ 4]";
1.1015 +val srls = append_rls "erls_IntegrierenUndK.." e_rls
1.1016 + [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.1017 + Calc ("Atools.ident",eval_ident "#ident_"),
1.1018 + Thm ("last_thmI",num_str last_thmI),
1.1019 + Thm ("if_True",num_str if_True),
1.1020 + Thm ("if_False",num_str if_False)
1.1021 + ]
1.1022 + ;
1.1023 +val t = str2term "last [1,2,3,4]";
1.1024 +trace_rewrite := true;
1.1025 +val SOME (e1__,_) = rewrite_set_ thy false srls t;
1.1026 +trace_rewrite := false;
1.1027 +term2str e1__;
1.1028 +
1.1029 +trace_script := true;
1.1030 +trace_script := false;
1.1031 +
1.1032 +
1.1033 +"----------- investigate normalforms in biegelinien --------------";
1.1034 +"----------- investigate normalforms in biegelinien --------------";
1.1035 +"----------- investigate normalforms in biegelinien --------------";
1.1036 +"----- coming from integration:";
1.1037 +val Q = str2term "Q x = c + -1 * q_0 * x";
1.1038 +val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.1039 +val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.1040 +val y = str2term "y x = c_4 + c_3 * x +\n1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
1.1041 +(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
1.1042 +
1.1043 +"----- functions comming from:";