1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Wed Feb 14 10:50:12 2018 +0100
1.3 @@ -0,0 +1,520 @@
1.4 +(* tests on biegelinie
1.5 + author: Walther Neuper 050826
1.6 + (c) due to copyright terms
1.7 +*)
1.8 +trace_rewrite := false;
1.9 +"-----------------------------------------------------------------";
1.10 +"table of contents -----------------------------------------------";
1.11 +"-----------------------------------------------------------------";
1.12 +"----------- the rules -------------------------------------------";
1.13 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.14 +"----------- simplify_leaf for this script -----------------------";
1.15 +"----------- Bsp 7.27 me -----------------------------------------";
1.16 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.17 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.18 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.19 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.20 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
1.21 +"----------- investigate normalforms in biegelinien --------------";
1.22 +"-----------------------------------------------------------------";
1.23 +"-----------------------------------------------------------------";
1.24 +"-----------------------------------------------------------------";
1.25 +
1.26 +val thy = @{theory "Biegelinie"};
1.27 +val ctxt = thy2ctxt' "Biegelinie";
1.28 +fun str2term str = (Thm.term_of o the o (parse thy)) str;
1.29 +fun term2s t = term_to_string'' "Biegelinie" t;
1.30 +fun rewrit thm str =
1.31 + fst (the (rewrite_ thy tless_true e_rls true thm str));
1.32 +
1.33 +"----------- the rules -------------------------------------------";
1.34 +"----------- the rules -------------------------------------------";
1.35 +"----------- the rules -------------------------------------------";
1.36 +val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
1.37 +if term2s t = "Q' x = - q_0" then ()
1.38 +else error "/biegelinie.sml: Belastung_Querkraft";
1.39 +
1.40 +val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
1.41 +if term2s t = "M_b' x = - q_0 * x + c" then ()
1.42 +else error "/biegelinie.sml: Querkraft_Moment";
1.43 +
1.44 +val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.45 + term2s t;
1.46 +if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
1.47 +else error "biegelinie.sml: Moment_Neigung";
1.48 +
1.49 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.50 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.51 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.52 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.53 +val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
1.54 +val t = rewrit @{thm Moment_Neigung} t;
1.55 +if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
1.56 +else error "Moment_Neigung broken";
1.57 +(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
1.58 + before declaring "y''" as a constant *)
1.59 +
1.60 +val t = rewrit @{thm make_fun_explicit} t;
1.61 +if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
1.62 +else error "make_fun_explicit broken";
1.63 +
1.64 +"----------- simplify_leaf for this script -----------------------";
1.65 +"----------- simplify_leaf for this script -----------------------";
1.66 +"----------- simplify_leaf for this script -----------------------";
1.67 +val srls = Rls {id="srls_IntegrierenUnd..",
1.68 + preconds = [],
1.69 + rew_ord = ("termlessI",termlessI),
1.70 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.71 + [(*for asm in NTH_CONS ...*)
1.72 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.73 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.74 + Calc("Groups.plus_class.plus", eval_binop "#add_")
1.75 + ],
1.76 + srls = Erls, calc = [], errpatts = [],
1.77 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.78 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.79 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.80 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.81 + Calc("Tools.rhs", eval_rhs "eval_rhs_"),
1.82 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
1.83 + ],
1.84 + scr = EmptyScr};
1.85 +val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
1.86 +val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
1.87 +val SOME (e1__,_) = rewrite_set_ thy false srls
1.88 + (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
1.89 +if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
1.90 +
1.91 +val SOME (x1__,_) =
1.92 + rewrite_set_ thy false srls
1.93 + (str2term"argument_in (lhs (M_b 0 = 0))");
1.94 +if term2str x1__ = "0" then ()
1.95 +else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
1.96 +
1.97 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
1.98 +trace_rewrite:=false;
1.99 +
1.100 +"----------- Bsp 7.27 me -----------------------------------------";
1.101 +"----------- Bsp 7.27 me -----------------------------------------";
1.102 +"----------- Bsp 7.27 me -----------------------------------------";
1.103 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.104 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.105 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.106 + "FunktionsVariable x"];
1.107 +val (dI',pI',mI') =
1.108 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
1.109 + ["IntegrierenUndKonstanteBestimmen"]);
1.110 +val p = e_pos'; val c = [];
1.111 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.112 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.113 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.114 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.115 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.116 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.117 +
1.118 +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
1.119 +(*if itms2str_ ctxt pits = ... all 5 model-items*)
1.120 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
1.121 +if itms2str_ ctxt mits = "[]" then ()
1.122 +else error "biegelinie.sml: Bsp 7.27 #2";
1.123 +
1.124 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.125 +case nxt of (_,Add_Given "FunktionsVariable x") => ()
1.126 + | _ => error "biegelinie.sml: Bsp 7.27 #4a";
1.127 +
1.128 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.129 +val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
1.130 +(*if itms2str_ ctxt mits = ... all 6 guard-items*)
1.131 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.132 + | _ => error "biegelinie.sml: Bsp 7.27 #4b";
1.133 +
1.134 +"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
1.135 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.136 +case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.137 + | _ => error "biegelinie.sml: Bsp 7.27 #4c";
1.138 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.139 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.140 +
1.141 +case nxt of
1.142 + (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
1.143 + | _ => error "biegelinie.sml: Bsp 7.27 #4c";
1.144 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.145 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.146 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.147 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.148 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.149 + | _ => error "biegelinie.sml: Bsp 7.27 #5";
1.150 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.151 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.152 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.153 +case nxt of
1.154 + ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
1.155 + | _ => error "biegelinie.sml: Bsp 7.27 #5a";
1.156 +
1.157 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.158 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.159 +case nxt of
1.160 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
1.161 + | _ => error "biegelinie.sml: Bsp 7.27 #5b";
1.162 +
1.163 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.164 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.165 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.166 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.167 +case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
1.168 + | _ => error "biegelinie.sml: Bsp 7.27 #6";
1.169 +
1.170 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.171 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
1.172 +f2str f;
1.173 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.174 +case nxt of (_, Substitute ["x = 0"]) => ()
1.175 + | _ => error "biegelinie.sml: Bsp 7.27 #7";
1.176 +
1.177 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.178 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.179 +if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
1.180 +else error "biegelinie.sml: Bsp 7.27 #8";
1.181 +
1.182 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.183 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.184 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.185 +if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
1.186 +else error "biegelinie.sml: Bsp 7.27 #9";
1.187 +
1.188 +(*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)
1.189 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.190 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
1.194 +case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
1.195 + | _ => error "biegelinie.sml: Bsp 7.27 #10";
1.196 +
1.197 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.198 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.199 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.200 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.201 +(*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
1.202 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.203 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.204 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.205 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.206 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.207 +case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
1.208 + | _ => error "biegelinie.sml: Bsp 7.27 #11";
1.209 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.210 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.211 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.212 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.213 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.214 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.218 +case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
1.219 + | _ => error "biegelinie.sml: Bsp 7.27 #12";
1.220 +
1.221 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.222 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.223 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.224 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.225 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.226 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.227 +case nxt of
1.228 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
1.229 + | _ => error "biegelinie.sml: Bsp 7.27 #13";
1.230 +
1.231 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.232 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.233 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.234 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.235 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.236 + | _ => error "biegelinie.sml: Bsp 7.27 #14";
1.237 +
1.238 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.239 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.240 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.241 +case nxt of
1.242 + (_, Check_Postcond ["named", "integrate", "function"]) => ()
1.243 + | _ => error "biegelinie.sml: Bsp 7.27 #15";
1.244 +
1.245 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.246 +if f2str f =
1.247 + "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
1.248 +then () else error "biegelinie.sml: Bsp 7.27 #16 f";
1.249 +case nxt of
1.250 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
1.251 + | _ => error "biegelinie.sml: Bsp 7.27 #16";
1.252 +
1.253 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.254 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.255 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.256 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.257 +case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
1.258 + | _ => error "biegelinie.sml: Bsp 7.27 #17";
1.259 +
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 =
1.263 + "y x =\nc_2 + c * x +\n\
1.264 + \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
1.265 +then () else error "biegelinie.sml: Bsp 7.27 #18 f";
1.266 +case nxt of
1.267 + (_, Check_Postcond ["named", "integrate", "function"]) => ()
1.268 + | _ => error "biegelinie.sml: Bsp 7.27 #18";
1.269 +
1.270 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.271 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.272 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.273 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 +case nxt of
1.277 + (_, Subproblem
1.278 + ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()
1.279 + | _ => error "biegelinie.sml: Bsp 7.27 #19";
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 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.285 +case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
1.286 + | _ => error "biegelinie.sml: Bsp 7.27 #20";
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 +if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
1.293 +else error "biegelinie.sml: Bsp 7.27 #21 f";
1.294 +case nxt of
1.295 + (_, Subproblem
1.296 + ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
1.297 + | _ => error "biegelinie.sml: Bsp 7.27 #21";
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 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.302 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.303 +case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
1.304 + | _ => error "biegelinie.sml: Bsp 7.27 #22";
1.305 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.306 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.307 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.308 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.309 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.310 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.311 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.312 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.313 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.314 +case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
1.315 + | _ => error "biegelinie.sml: Bsp 7.27 #23";
1.316 +
1.317 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.318 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.319 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.320 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.321 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.322 +if f2str f =
1.323 + "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
1.324 + "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
1.325 +then () else error "biegelinie.sml: Bsp 7.27 #24 f";
1.326 +case nxt of ("End_Proof'", End_Proof') => ()
1.327 + | _ => error "biegelinie.sml: Bsp 7.27 #24";
1.328 +
1.329 +show_pt pt;
1.330 +(*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
1.331 +(([1], Frm), q_ x = q_0),
1.332 +(([1], Res), - q_ x = - q_0),
1.333 +(([2], Res), Q' x = - q_0),
1.334 +(([3], Pbl), Integrate (- q_0, x)),
1.335 +(([3,1], Frm), Q x = Integral - q_0 D x),
1.336 +(([3,1], Res), Q x = -1 * q_0 * x + c),
1.337 +(([3], Res), Q x = -1 * q_0 * x + c),
1.338 +(([4], Res), M_b' x = -1 * q_0 * x + c),
1.339 +(([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
1.340 +(([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
1.341 +(([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
1.342 +(([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
1.343 +(([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
1.344 +(([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
1.345 +(([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
1.346 +(([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
1.347 +(([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
1.348 +(([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
1.349 + 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
1.350 +(([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
1.351 +(([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
1.352 +(([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
1.353 +(([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
1.354 +(([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
1.355 +(([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
1.356 +(([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
1.357 +(([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
1.358 +(([10,4,4], Res), c = L * q_0 / 2),
1.359 +(([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
1.360 +(([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
1.361 +(([10], Res), [c = L * q_0 / 2, c_2 = 0]),
1.362 +(([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
1.363 +(([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
1.364 +(([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
1.365 +(([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
1.366 +(([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
1.367 +(([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
1.368 +(([15,1], Res), y' x =
1.369 +(Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
1.370 +c)]*)
1.371 +
1.372 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.373 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.374 +"----------- Bsp 7.27 autoCalculate ------------------------------";
1.375 + reset_states ();
1.376 + CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.377 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.378 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.379 + "FunktionsVariable x"],
1.380 + ("Biegelinie",
1.381 + ["MomentBestimmte","Biegelinien"],
1.382 + ["IntegrierenUndKonstanteBestimmen"]))];
1.383 + moveActiveRoot 1;
1.384 + autoCalculate 1 CompleteCalcHead;
1.385 +
1.386 + fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
1.387 +(*
1.388 +> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
1.389 +val it = true : bool
1.390 +*)
1.391 + autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
1.392 + val ((pt,_),_) = get_calc 1;
1.393 + case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.394 + | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
1.395 +
1.396 + autoCalculate 1 CompleteCalc;
1.397 +val ((pt,p),_) = get_calc 1;
1.398 +if p = ([], Res) andalso length (children pt) = 23 andalso
1.399 +term2str (get_obj g_res pt (fst p)) =
1.400 +"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.401 +then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.402 +
1.403 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.404 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.405 + show_pt pt;
1.406 +
1.407 +(*check all formulae for getTactic*)
1.408 + getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
1.409 + getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
1.410 + getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
1.411 + getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
1.412 + getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
1.413 + getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
1.414 +
1.415 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.416 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.417 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.418 +val fmz =
1.419 + ["Streckenlast q_0","FunktionsVariable x",
1.420 + "Funktionen [Q x = c + -1 * q_0 * x, \
1.421 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
1.422 + \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
1.423 + \ 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.424 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
1.425 + ["Biegelinien","ausBelastung"]);
1.426 +val p = e_pos'; val c = [];
1.427 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.428 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.429 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.430 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.431 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.432 +case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
1.433 +| _ => error "biegelinie.sml met2 b";
1.434 +
1.435 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
1.436 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
1.437 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
1.438 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
1.439 +| _ => error "biegelinie.sml met2 c";
1.440 +
1.441 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.442 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.443 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.444 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.445 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.446 +
1.447 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.448 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.449 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
1.450 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
1.451 +| _ => error "biegelinie.sml met2 d";
1.452 +
1.453 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.454 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.455 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.456 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.457 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.458 + "M_b x = Integral c + -1 * q_0 * x D x";
1.459 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.460 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.461 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.462 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.463 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.464 + "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.465 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.466 + "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
1.467 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.468 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.469 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.470 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.471 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.472 + "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.473 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.474 +"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.475 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.476 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.477 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.478 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
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 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.484 +"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.485 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.486 +"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.487 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.488 + "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.489 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.490 +if f2str f =
1.491 + "[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.492 +then case nxt of ("End_Proof'", End_Proof') => ()
1.493 + | _ => error "biegelinie.sml met2 e 1"
1.494 +else error "biegelinie.sml met2 e 2";
1.495 +
1.496 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.497 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.498 +"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
1.499 +val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
1.500 + "substitution (M_b L = 0)",
1.501 + "equality equ_equ"];
1.502 +val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
1.503 + ["Equation","fromFunction"]);
1.504 +val p = e_pos'; val c = [];
1.505 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.506 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.507 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.508 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.509 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.510 +
1.511 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.512 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.513 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.514 + "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.515 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.516 + "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
1.517 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.518 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.519 +if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
1.520 + f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
1.521 +then case nxt of ("End_Proof'", End_Proof') => ()
1.522 + | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
1.523 +else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
1.524 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Wed Feb 14 10:50:12 2018 +0100
2.3 @@ -0,0 +1,246 @@
2.4 +(* Isabelle2015->17: divided into 2 files, because if
2.5 + in 1 file: exception Size raised (line 182 of "./basis/LibrarySupport.sml")
2.6 + author: Walther Neuper 180214
2.7 + (c) due to copyright terms
2.8 +*)
2.9 +"table of contents -----------------------------------------------";
2.10 +"-----------------------------------------------------------------";
2.11 +"----------- see biegelinie-1.sml---------------------------------";
2.12 +"----------- shift next exp up: exception Size raised ------------";
2.13 +"-----------------------------------------------------------------";
2.14 +"-----------------------------------------------------------------";
2.15 +"-----------------------------------------------------------------";
2.16 +
2.17 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
2.18 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
2.19 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
2.20 +"----- check the scripts syntax";
2.21 +"----- execute script by interpreter: setzeRandbedingungenEin";
2.22 +val fmz = ["Funktionen [Q x = c + -1 * q_0 * x," ^
2.23 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2," ^
2.24 + "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)," ^
2.25 + "y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]",
2.26 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
2.27 + "Gleichungen equ_s"];
2.28 +val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
2.29 + ["Biegelinien","setzeRandbedingungenEin"]);
2.30 +val p = e_pos'; val c = [];
2.31 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.32 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.36 +
2.37 +"--- before 1.subpbl [Equation, fromFunction]";
2.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.39 +case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
2.40 +| _ => error "biegelinie.sml: met setzeRandbed*Ein aa";
2.41 +"----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
2.42 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.43 +if (#1 o (get_obj g_fmz pt)) (fst p) =
2.44 + ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *" ^
2.45 + "\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
2.46 + "substitution (y 0 = 0)", "equality equ'''"] then ()
2.47 +else error "biegelinie.sml met setzeRandbed*Ein bb";
2.48 +(writeln o istate2str) (get_istate pt p);
2.49 +"--- after 1.subpbl [Equation, fromFunction]";
2.50 +
2.51 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.52 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.53 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.55 +case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
2.56 +| _ => error "biegelinie.sml met2 ff";
2.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
2.58 + "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
2.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.61 +case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
2.62 +| _ => error "biegelinie.sml met2 gg";
2.63 +
2.64 +"--- before 2.subpbl [Equation, fromFunction]";
2.65 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)" ;
2.66 +case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
2.67 +| _ => error "biegelinie.sml met2 hh";
2.68 +"--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
2.69 +
2.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.71 +if (#1 o (get_obj g_fmz pt)) (fst p) =
2.72 + ["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))",
2.73 + "substitution (y L = 0)", "equality equ'''"] then ()
2.74 +else error "biegelinie.sml metsetzeRandbed*Ein bb ";
2.75 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.77 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.78 +
2.79 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.80 +case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
2.81 +| _ => error "biegelinie.sml met2 ii";
2.82 +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)";
2.83 +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)";
2.84 +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)";
2.85 +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)" ;
2.86 +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)";
2.87 +case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
2.88 +| _ => error "biegelinie.sml met2 jj";
2.89 +
2.90 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.92 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.94 +case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
2.95 +| _ => error "biegelinie.sml met2 kk";
2.96 +
2.97 +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*);
2.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2";
2.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
2.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
2.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.102 +(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
2.103 +
2.104 +case nxt of (_, Subproblem (_, ["makeFunctionTo", "equation"])) => ()
2.105 +| _ => error "biegelinie.sml met2 ll";
2.106 +
2.107 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.109 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.111 +case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
2.112 +| _ => error "biegelinie.sml met2 mm";
2.113 +
2.114 +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";
2.115 +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";
2.116 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
2.117 +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";
2.118 +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";
2.119 +case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
2.120 +| _ => error "biegelinie.sml met2 nn";
2.121 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.122 +if nxt = ("End_Proof'", End_Proof') andalso f2str f =
2.123 +(* "[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]" *)
2.124 +"[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]"
2.125 +then () else error "biegelinie.sml met2 oo";
2.126 +============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
2.127 +
2.128 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
2.129 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
2.130 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
2.131 +"----- Bsp 7.70 with me";
2.132 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
2.133 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
2.134 + "FunktionsVariable x"];
2.135 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
2.136 + ["IntegrierenUndKonstanteBestimmen2"]);
2.137 +val p = e_pos'; val c = [];
2.138 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.139 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.140 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.141 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.142 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.143 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.144 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.145 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.146 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.147 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.148 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.149 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.150 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.151 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.152 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.153 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.154 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.155 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.156 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.157 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.158 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.159 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.160 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.161 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.162 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.163 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.164 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.165 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.166 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.167 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.168 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.169 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.170 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.171 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.172 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.173 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.174 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.175 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.176 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.177 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.178 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.179 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.180 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.181 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.182 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.183 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.184 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.185 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.186 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.187 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.188 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.189 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.190 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.191 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.192 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.193 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.194 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.195 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.196 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.197 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.198 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.199 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.200 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.201 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.202 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.203 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.204 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.205 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.206 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.207 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.208 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.209 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.210 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.211 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.212 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.213 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.214 +if p = ([3, 7], Res) then () else error "Bsp.7.70 ok: p = ([3, 7], Res)";
2.215 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.216 +if p = ([3, 8], Pbl) then () else error "Bsp.7.70 ok: p = ([3, 8], Pbl)";
2.217 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.218 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.219 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.220 +if p = ([3, 8], Pbl) then () else error "Bsp.7.70 ok: p = ([3, 8], Pbl)";
2.221 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.222 +if p = ([3, 8, 1], Frm) then () else error "Bsp.7.70 ok: p = ([3, 8, 1], Frm)";
2.223 +(* no progress from here ...*)
2.224 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.225 +if p = ([3, 8, 1], Res) then () else error "Bsp.7.70 ok: p = ([3, 8, 1], Res)";
2.226 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.227 +if p = ([3, 8, 1], Res) then () else error "Bsp.7.70 ok: p = ([3, 8, 1], Res)";
2.228 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.229 +if p = ([3, 8, 1], Res) then () else error "Bsp.7.70 ok: p = ([3, 8, 1], Res)";
2.230 +(*... no progress leads to: exception Size raised (line 182 of "./basis/LibrarySupport.sml")
2.231 +
2.232 +^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^
2.233 +
2.234 +On correction don't forget to reactivate --- test parallel calls to autoCalculate ---,
2.235 +which uses this example.*)
2.236 +
2.237 +"----------- investigate normalforms in biegelinien --------------";
2.238 +"----------- investigate normalforms in biegelinien --------------";
2.239 +"----------- investigate normalforms in biegelinien --------------";
2.240 +"----- coming from integration:";
2.241 +val Q = str2term "Q x = c + -1 * q_0 * x";
2.242 +val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
2.243 +val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
2.244 +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)";
2.245 +(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
2.246 +
2.247 +"----- functions comming from:";
2.248 +
2.249 +
3.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Wed Feb 14 08:05:37 2018 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,725 +0,0 @@
3.4 -(* tests on biegelinie
3.5 - author: Walther Neuper 050826
3.6 - (c) due to copyright terms
3.7 -*)
3.8 -trace_rewrite := false;
3.9 -"-----------------------------------------------------------------";
3.10 -"table of contents -----------------------------------------------";
3.11 -"-----------------------------------------------------------------";
3.12 -"----------- the rules -------------------------------------------";
3.13 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
3.14 -"----------- simplify_leaf for this script -----------------------";
3.15 -"----------- Bsp 7.27 me -----------------------------------------";
3.16 -"----------- Bsp 7.27 autoCalculate ------------------------------";
3.17 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
3.18 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
3.19 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
3.20 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
3.21 -"----------- investigate normalforms in biegelinien --------------";
3.22 -"-----------------------------------------------------------------";
3.23 -"-----------------------------------------------------------------";
3.24 -"-----------------------------------------------------------------";
3.25 -
3.26 -val thy = @{theory "Biegelinie"};
3.27 -val ctxt = thy2ctxt' "Biegelinie";
3.28 -fun str2term str = (Thm.term_of o the o (parse thy)) str;
3.29 -fun term2s t = term_to_string'' "Biegelinie" t;
3.30 -fun rewrit thm str =
3.31 - fst (the (rewrite_ thy tless_true e_rls true thm str));
3.32 -
3.33 -"----------- the rules -------------------------------------------";
3.34 -"----------- the rules -------------------------------------------";
3.35 -"----------- the rules -------------------------------------------";
3.36 -val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
3.37 -if term2s t = "Q' x = - q_0" then ()
3.38 -else error "/biegelinie.sml: Belastung_Querkraft";
3.39 -
3.40 -val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
3.41 -if term2s t = "M_b' x = - q_0 * x + c" then ()
3.42 -else error "/biegelinie.sml: Querkraft_Moment";
3.43 -
3.44 -val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
3.45 - term2s t;
3.46 -if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
3.47 -else error "biegelinie.sml: Moment_Neigung";
3.48 -
3.49 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
3.50 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
3.51 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
3.52 -"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
3.53 -val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
3.54 -val t = rewrit @{thm Moment_Neigung} t;
3.55 -if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
3.56 -else error "Moment_Neigung broken";
3.57 -(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
3.58 - before declaring "y''" as a constant *)
3.59 -
3.60 -val t = rewrit @{thm make_fun_explicit} t;
3.61 -if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
3.62 -else error "make_fun_explicit broken";
3.63 -
3.64 -"----------- simplify_leaf for this script -----------------------";
3.65 -"----------- simplify_leaf for this script -----------------------";
3.66 -"----------- simplify_leaf for this script -----------------------";
3.67 -val srls = Rls {id="srls_IntegrierenUnd..",
3.68 - preconds = [],
3.69 - rew_ord = ("termlessI",termlessI),
3.70 - erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
3.71 - [(*for asm in NTH_CONS ...*)
3.72 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
3.73 - (*2nd NTH_CONS pushes n+-1 into asms*)
3.74 - Calc("Groups.plus_class.plus", eval_binop "#add_")
3.75 - ],
3.76 - srls = Erls, calc = [], errpatts = [],
3.77 - rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
3.78 - Calc("Groups.plus_class.plus", eval_binop "#add_"),
3.79 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
3.80 - Calc("Tools.lhs", eval_lhs "eval_lhs_"),
3.81 - Calc("Tools.rhs", eval_rhs "eval_rhs_"),
3.82 - Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
3.83 - ],
3.84 - scr = EmptyScr};
3.85 -val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
3.86 -val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
3.87 -val SOME (e1__,_) = rewrite_set_ thy false srls
3.88 - (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
3.89 -if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
3.90 -
3.91 -val SOME (x1__,_) =
3.92 - rewrite_set_ thy false srls
3.93 - (str2term"argument_in (lhs (M_b 0 = 0))");
3.94 -if term2str x1__ = "0" then ()
3.95 -else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
3.96 -
3.97 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
3.98 -trace_rewrite:=false;
3.99 -
3.100 -"----------- Bsp 7.27 me -----------------------------------------";
3.101 -"----------- Bsp 7.27 me -----------------------------------------";
3.102 -"----------- Bsp 7.27 me -----------------------------------------";
3.103 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.104 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
3.105 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
3.106 - "FunktionsVariable x"];
3.107 -val (dI',pI',mI') =
3.108 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
3.109 - ["IntegrierenUndKonstanteBestimmen"]);
3.110 -val p = e_pos'; val c = [];
3.111 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.112 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.113 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.114 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.115 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.116 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.117 -
3.118 -val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
3.119 -(*if itms2str_ ctxt pits = ... all 5 model-items*)
3.120 -val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
3.121 -if itms2str_ ctxt mits = "[]" then ()
3.122 -else error "biegelinie.sml: Bsp 7.27 #2";
3.123 -
3.124 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.125 -case nxt of (_,Add_Given "FunktionsVariable x") => ()
3.126 - | _ => error "biegelinie.sml: Bsp 7.27 #4a";
3.127 -
3.128 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.129 -val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
3.130 -(*if itms2str_ ctxt mits = ... all 6 guard-items*)
3.131 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
3.132 - | _ => error "biegelinie.sml: Bsp 7.27 #4b";
3.133 -
3.134 -"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
3.135 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.136 -case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
3.137 - | _ => error "biegelinie.sml: Bsp 7.27 #4c";
3.138 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.139 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.140 -
3.141 -case nxt of
3.142 - (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
3.143 - | _ => error "biegelinie.sml: Bsp 7.27 #4c";
3.144 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.145 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.146 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.147 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.148 -case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
3.149 - | _ => error "biegelinie.sml: Bsp 7.27 #5";
3.150 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.151 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.152 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.153 -case nxt of
3.154 - ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
3.155 - | _ => error "biegelinie.sml: Bsp 7.27 #5a";
3.156 -
3.157 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.158 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.159 -case nxt of
3.160 - (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
3.161 - | _ => error "biegelinie.sml: Bsp 7.27 #5b";
3.162 -
3.163 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.164 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.165 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.166 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.167 -case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
3.168 - | _ => error "biegelinie.sml: Bsp 7.27 #6";
3.169 -
3.170 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.171 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
3.172 -f2str f;
3.173 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.174 -case nxt of (_, Substitute ["x = 0"]) => ()
3.175 - | _ => error "biegelinie.sml: Bsp 7.27 #7";
3.176 -
3.177 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.178 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.179 -if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
3.180 -else error "biegelinie.sml: Bsp 7.27 #8";
3.181 -
3.182 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.183 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.184 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.185 -if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
3.186 -else error "biegelinie.sml: Bsp 7.27 #9";
3.187 -
3.188 -(*val nxt = (+, Subproblem ("Biegelinie", ["normalise", ..lin..sys]))*)
3.189 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.190 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.191 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.192 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.193 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.194 -case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
3.195 - | _ => error "biegelinie.sml: Bsp 7.27 #10";
3.196 -
3.197 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.198 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.199 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.200 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.201 -(*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
3.202 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.203 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.204 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.205 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.206 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.207 -case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
3.208 - | _ => error "biegelinie.sml: Bsp 7.27 #11";
3.209 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.210 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.211 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.212 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.213 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.214 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.215 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.216 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.217 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.218 -case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
3.219 - | _ => error "biegelinie.sml: Bsp 7.27 #12";
3.220 -
3.221 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.222 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.223 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.224 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.225 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.226 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.227 -case nxt of
3.228 - (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
3.229 - | _ => error "biegelinie.sml: Bsp 7.27 #13";
3.230 -
3.231 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.232 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.233 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.234 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.235 -case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
3.236 - | _ => error "biegelinie.sml: Bsp 7.27 #14";
3.237 -
3.238 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.239 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.240 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.241 -case nxt of
3.242 - (_, Check_Postcond ["named", "integrate", "function"]) => ()
3.243 - | _ => error "biegelinie.sml: Bsp 7.27 #15";
3.244 -
3.245 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.246 -if f2str f =
3.247 - "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
3.248 -then () else error "biegelinie.sml: Bsp 7.27 #16 f";
3.249 -case nxt of
3.250 - (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
3.251 - | _ => error "biegelinie.sml: Bsp 7.27 #16";
3.252 -
3.253 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.254 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.255 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.256 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.257 -case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
3.258 - | _ => error "biegelinie.sml: Bsp 7.27 #17";
3.259 -
3.260 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.261 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.262 -if f2str f =
3.263 - "y x =\nc_2 + c * x +\n\
3.264 - \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
3.265 -then () else error "biegelinie.sml: Bsp 7.27 #18 f";
3.266 -case nxt of
3.267 - (_, Check_Postcond ["named", "integrate", "function"]) => ()
3.268 - | _ => error "biegelinie.sml: Bsp 7.27 #18";
3.269 -
3.270 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.271 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.272 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.273 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.274 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.275 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.276 -case nxt of
3.277 - (_, Subproblem
3.278 - ("Biegelinie", ["normalise", "2x2", "LINEAR", "system"])) => ()
3.279 - | _ => error "biegelinie.sml: Bsp 7.27 #19";
3.280 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.281 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.282 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.283 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.284 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.285 -case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
3.286 - | _ => error "biegelinie.sml: Bsp 7.27 #20";
3.287 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.288 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.289 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.290 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.291 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.292 -if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
3.293 -else error "biegelinie.sml: Bsp 7.27 #21 f";
3.294 -case nxt of
3.295 - (_, Subproblem
3.296 - ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
3.297 - | _ => error "biegelinie.sml: Bsp 7.27 #21";
3.298 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.299 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.300 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.301 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.302 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.303 -case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
3.304 - | _ => error "biegelinie.sml: Bsp 7.27 #22";
3.305 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.306 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.307 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.308 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.309 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.310 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.311 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.312 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.313 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.314 -case nxt of (_, Check_Postcond ["normalise", "2x2", "LINEAR", "system"]) => ()
3.315 - | _ => error "biegelinie.sml: Bsp 7.27 #23";
3.316 -
3.317 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.318 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.319 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.320 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.321 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.322 -if f2str f =
3.323 - "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
3.324 - "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
3.325 -then () else error "biegelinie.sml: Bsp 7.27 #24 f";
3.326 -case nxt of ("End_Proof'", End_Proof') => ()
3.327 - | _ => error "biegelinie.sml: Bsp 7.27 #24";
3.328 -
3.329 -show_pt pt;
3.330 -(*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
3.331 -(([1], Frm), q_ x = q_0),
3.332 -(([1], Res), - q_ x = - q_0),
3.333 -(([2], Res), Q' x = - q_0),
3.334 -(([3], Pbl), Integrate (- q_0, x)),
3.335 -(([3,1], Frm), Q x = Integral - q_0 D x),
3.336 -(([3,1], Res), Q x = -1 * q_0 * x + c),
3.337 -(([3], Res), Q x = -1 * q_0 * x + c),
3.338 -(([4], Res), M_b' x = -1 * q_0 * x + c),
3.339 -(([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
3.340 -(([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
3.341 -(([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
3.342 -(([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
3.343 -(([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
3.344 -(([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
3.345 -(([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
3.346 -(([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
3.347 -(([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
3.348 -(([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
3.349 - 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
3.350 -(([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
3.351 -(([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
3.352 -(([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
3.353 -(([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
3.354 -(([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
3.355 -(([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
3.356 -(([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
3.357 -(([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
3.358 -(([10,4,4], Res), c = L * q_0 / 2),
3.359 -(([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
3.360 -(([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
3.361 -(([10], Res), [c = L * q_0 / 2, c_2 = 0]),
3.362 -(([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
3.363 -(([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
3.364 -(([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
3.365 -(([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
3.366 -(([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
3.367 -(([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
3.368 -(([15,1], Res), y' x =
3.369 -(Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
3.370 -c)]*)
3.371 -
3.372 -"----------- Bsp 7.27 autoCalculate ------------------------------";
3.373 -"----------- Bsp 7.27 autoCalculate ------------------------------";
3.374 -"----------- Bsp 7.27 autoCalculate ------------------------------";
3.375 - reset_states ();
3.376 - CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.377 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
3.378 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
3.379 - "FunktionsVariable x"],
3.380 - ("Biegelinie",
3.381 - ["MomentBestimmte","Biegelinien"],
3.382 - ["IntegrierenUndKonstanteBestimmen"]))];
3.383 - moveActiveRoot 1;
3.384 - autoCalculate 1 CompleteCalcHead;
3.385 -
3.386 - fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
3.387 -(*
3.388 -> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
3.389 -val it = true : bool
3.390 -*)
3.391 - autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
3.392 - val ((pt,_),_) = get_calc 1;
3.393 - case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
3.394 - | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
3.395 -
3.396 - autoCalculate 1 CompleteCalc;
3.397 -val ((pt,p),_) = get_calc 1;
3.398 -if p = ([], Res) andalso length (children pt) = 23 andalso
3.399 -term2str (get_obj g_res pt (fst p)) =
3.400 -"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)"
3.401 -then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
3.402 -
3.403 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
3.404 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
3.405 - show_pt pt;
3.406 -
3.407 -(*check all formulae for getTactic*)
3.408 - getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
3.409 - getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
3.410 - getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
3.411 - getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
3.412 - getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
3.413 - getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
3.414 -
3.415 -
3.416 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
3.417 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
3.418 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
3.419 -val fmz =
3.420 - ["Streckenlast q_0","FunktionsVariable x",
3.421 - "Funktionen [Q x = c + -1 * q_0 * x, \
3.422 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
3.423 - \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
3.424 - \ 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)]"];
3.425 -val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
3.426 - ["Biegelinien","ausBelastung"]);
3.427 -val p = e_pos'; val c = [];
3.428 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.429 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.430 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.431 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.432 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.433 -case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
3.434 -| _ => error "biegelinie.sml met2 b";
3.435 -
3.436 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
3.437 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
3.438 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
3.439 -case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
3.440 -| _ => error "biegelinie.sml met2 c";
3.441 -
3.442 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.443 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.444 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.445 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.446 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.447 -
3.448 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
3.449 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
3.450 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
3.451 -case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
3.452 -| _ => error "biegelinie.sml met2 d";
3.453 -
3.454 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.455 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.456 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.457 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.458 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.459 - "M_b x = Integral c + -1 * q_0 * x D x";
3.460 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.461 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
3.462 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.463 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
3.464 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.465 - "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
3.466 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.467 - "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
3.468 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.469 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.470 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.471 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.472 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.473 - "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
3.474 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.475 -"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
3.476 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.477 -"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
3.478 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.479 -"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
3.480 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.481 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.482 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.483 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.484 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.485 -"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";
3.486 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.487 -"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)";
3.488 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.489 - "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)";
3.490 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.491 -if f2str f =
3.492 - "[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)]"
3.493 -then case nxt of ("End_Proof'", End_Proof') => ()
3.494 - | _ => error "biegelinie.sml met2 e 1"
3.495 -else error "biegelinie.sml met2 e 2";
3.496 -
3.497 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
3.498 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
3.499 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
3.500 -val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
3.501 - "substitution (M_b L = 0)",
3.502 - "equality equ_equ"];
3.503 -val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
3.504 - ["Equation","fromFunction"]);
3.505 -val p = e_pos'; val c = [];
3.506 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.507 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.508 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.509 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.510 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.511 -
3.512 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.513 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
3.514 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.515 - "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
3.516 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.517 - "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
3.518 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.519 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.520 -if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
3.521 - f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
3.522 -then case nxt of ("End_Proof'", End_Proof') => ()
3.523 - | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
3.524 -else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
3.525 -
3.526 -
3.527 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
3.528 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
3.529 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
3.530 -"----- check the scripts syntax";
3.531 -"----- execute script by interpreter: setzeRandbedingungenEin";
3.532 -val fmz = ["Funktionen [Q x = c + -1 * q_0 * x," ^
3.533 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2," ^
3.534 - "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)," ^
3.535 - "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)]",
3.536 - "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
3.537 - "Gleichungen equ_s"];
3.538 -val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
3.539 - ["Biegelinien","setzeRandbedingungenEin"]);
3.540 -val p = e_pos'; val c = [];
3.541 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.542 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.543 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.544 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.545 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.546 -
3.547 -"--- before 1.subpbl [Equation, fromFunction]";
3.548 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.549 -case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
3.550 -| _ => error "biegelinie.sml: met setzeRandbed*Ein aa";
3.551 -"----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
3.552 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.553 -if (#1 o (get_obj g_fmz pt)) (fst p) =
3.554 - ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *" ^
3.555 - "\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
3.556 - "substitution (y 0 = 0)", "equality equ'''"] then ()
3.557 -else error "biegelinie.sml met setzeRandbed*Ein bb";
3.558 -(writeln o istate2str) (get_istate pt p);
3.559 -"--- after 1.subpbl [Equation, fromFunction]";
3.560 -
3.561 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.562 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.563 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.564 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.565 -case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
3.566 -| _ => error "biegelinie.sml met2 ff";
3.567 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.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)";
3.569 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.570 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.571 -case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
3.572 -| _ => error "biegelinie.sml met2 gg";
3.573 -
3.574 -"--- before 2.subpbl [Equation, fromFunction]";
3.575 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)" ;
3.576 -case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
3.577 -| _ => error "biegelinie.sml met2 hh";
3.578 -"--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
3.579 -
3.580 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.581 -if (#1 o (get_obj g_fmz pt)) (fst p) =
3.582 - ["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))",
3.583 - "substitution (y L = 0)", "equality equ'''"] then ()
3.584 -else error "biegelinie.sml metsetzeRandbed*Ein bb ";
3.585 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.586 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.587 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.588 -
3.589 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.590 -case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
3.591 -| _ => error "biegelinie.sml met2 ii";
3.592 -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)";
3.593 -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)";
3.594 -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)";
3.595 -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)" ;
3.596 -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)";
3.597 -case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
3.598 -| _ => error "biegelinie.sml met2 jj";
3.599 -
3.600 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.601 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.602 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.603 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.604 -case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
3.605 -| _ => error "biegelinie.sml met2 kk";
3.606 -
3.607 -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*);
3.608 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2";
3.609 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
3.610 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
3.611 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.612 -(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
3.613 -
3.614 -case nxt of (_, Subproblem (_, ["makeFunctionTo", "equation"])) => ()
3.615 -| _ => error "biegelinie.sml met2 ll";
3.616 -
3.617 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.618 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.619 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.620 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.621 -case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
3.622 -| _ => error "biegelinie.sml met2 mm";
3.623 -
3.624 -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";
3.625 -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";
3.626 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
3.627 -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";
3.628 -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";
3.629 -case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
3.630 -| _ => error "biegelinie.sml met2 nn";
3.631 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.632 -if nxt = ("End_Proof'", End_Proof') andalso f2str f =
3.633 -(* "[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]" *)
3.634 -"[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]"
3.635 -then () else error "biegelinie.sml met2 oo";
3.636 -============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
3.637 -
3.638 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
3.639 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
3.640 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
3.641 -"----- Bsp 7.70 with me";
3.642 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.643 - "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
3.644 - "FunktionsVariable x"];
3.645 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
3.646 - ["IntegrierenUndKonstanteBestimmen2"]);
3.647 -val p = e_pos'; val c = [];
3.648 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.649 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.650 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.651 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.652 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.653 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.654 -(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
3.655 -if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
3.656 -then () else error "biegelinie.sml met2 a";
3.657 -
3.658 -(*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
3.659 -... THIS MEANS:
3.660 -#a# "Script Biegelinie2Script ..
3.661 -" ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
3.662 -" [Biegelinien,ausBelastung]) " ^
3.663 -" [REAL q__, REAL v_]); "
3.664 -
3.665 -#b# prep_met ... (["Biegelinien","ausBelastung"],
3.666 - ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
3.667 - "Script Belastung2BiegelScript (q__::real) (v_v::real) = "
3.668 -
3.669 -#a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK
3.670 -##########################################################################
3.671 -BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
3.672 -##########################################################################*)
3.673 -"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------" ^
3.674 -" ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
3.675 -
3.676 -DEconstrCalcTree 1;
3.677 -"----- Bsp 7.70 with autoCalculate";
3.678 -CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.679 - "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
3.680 - "FunktionsVariable x"],
3.681 - ("Biegelinie", ["Biegelinien"],
3.682 - ["IntegrierenUndKonstanteBestimmen2"]))];
3.683 -moveActiveRoot 1;
3.684 -autoCalculate 1 CompleteCalc;
3.685 -val ((pt,p),_) = get_calc 1; show_pt pt;
3.686 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
3.687 -"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 ()
3.688 -else error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
3.689 -
3.690 -val is = get_istate pt ([],Res); writeln (istate2str is);
3.691 -val t = str2term (" last " ^
3.692 -"[Q x = L * q_0 + -1 * q_0 * x, " ^
3.693 -" M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2," ^
3.694 -" y' x = " ^
3.695 -" -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +" ^
3.696 -" -1 * q_0 / (-6 * EI) * x ^^^ 3, " ^
3.697 -" y x = " ^
3.698 -" -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + " ^
3.699 -" 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + " ^
3.700 -" -1 * q_0 / (-24 * EI) * x ^^^ 4]");
3.701 -val srls = append_rls "erls_IntegrierenUndK.." e_rls
3.702 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.703 - Calc ("Atools.ident",eval_ident "#ident_"),
3.704 - Thm ("last_thmI",num_str @{thm last_thmI}),
3.705 - Thm ("if_True",num_str @{thm if_True}),
3.706 - Thm ("if_False",num_str @{thm if_False})
3.707 - ]
3.708 - ;
3.709 -val t = str2term "last [1,2,3,4]";
3.710 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
3.711 -val SOME (e1__,_) = rewrite_set_ thy false srls t;
3.712 -trace_rewrite := false;
3.713 -term2str e1__;
3.714 -============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
3.715 -
3.716 -"----------- investigate normalforms in biegelinien --------------";
3.717 -"----------- investigate normalforms in biegelinien --------------";
3.718 -"----------- investigate normalforms in biegelinien --------------";
3.719 -"----- coming from integration:";
3.720 -val Q = str2term "Q x = c + -1 * q_0 * x";
3.721 -val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
3.722 -val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
3.723 -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)";
3.724 -(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
3.725 -
3.726 -"----- functions comming from:";
3.727 -
3.728 -
4.1 --- a/test/Tools/isac/Test_Isac.thy Wed Feb 14 08:05:37 2018 +0100
4.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Feb 14 10:50:12 2018 +0100
4.3 @@ -104,8 +104,6 @@
4.4 open Model; (* NONE *)
4.5 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.6 *}
4.7 -(*---------------------- check test file by testfile -------------------------------------------
4.8 - ---------------------- check test file by testfile -------------------------------------------*)
4.9
4.10 ML {*
4.11 "~~~~~ fun xxx, args:"; val () = ();
4.12 @@ -118,6 +116,8 @@
4.13 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
4.14 *}
4.15
4.16 +(*---------------------- check test file by testfile -------------------------------------------
4.17 + ---------------------- check test file by testfile -------------------------------------------*)
4.18 section {* trials with Isabelle's functions *}
4.19 ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
4.20 ML_file "~~/test/Pure/General/alist.ML"
4.21 @@ -204,16 +204,7 @@
4.22 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
4.23 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
4.24 ML_file "Knowledge/rootrat.sml"
4.25 -
4.26 -ML {*
4.27 -"~~~~~ fun xxx, args:"; val () = ();
4.28 -*} ML {*
4.29 -
4.30 -*} ML {*
4.31 -*}
4.32 -
4.33 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
4.34 -(*---------------------- check test file by testfile -------------------------------------------
4.35 ML_file "Knowledge/partial_fractions.sml"
4.36 ML_file "Knowledge/polyeq.sml"
4.37 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
4.38 @@ -227,7 +218,8 @@
4.39 ML_file "Knowledge/polyminus.sml"
4.40 ML_file "Knowledge/vect.sml"
4.41 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
4.42 - ML_file "Knowledge/biegelinie.sml"
4.43 + ML_file "Knowledge/biegelinie-1.sml"
4.44 +(*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)
4.45 ML_file "Knowledge/algein.sml"
4.46 ML_file "Knowledge/diophanteq.sml"
4.47 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
4.48 @@ -239,7 +231,6 @@
4.49 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
4.50 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
4.51 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
4.52 - ---------------------- check test file by testfile -------------------------------------------*)
4.53
4.54 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
4.55 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}