1.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -28,23 +28,23 @@
1.4
1.5 val thy = @{theory "Biegelinie"};
1.6 val ctxt = ThyC.id_to_ctxt "Biegelinie";
1.7 -fun str2term str = (Thm.term_of o the o (parse thy)) str;
1.8 +fun TermC.str2term str = (Thm.term_of o the o (TermC.parse thy)) str;
1.9 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
1.10 fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));
1.11
1.12 "----------- the rules -------------------------------------------";
1.13 "----------- the rules -------------------------------------------";
1.14 "----------- the rules -------------------------------------------";
1.15 -val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
1.16 +val t = rewrit @{thm Belastung_Querkraft} (TermC.str2term "- qq x = - q_0"); term2s t;
1.17 if term2s t = "Q' x = - q_0" then ()
1.18 else error "/biegelinie.sml: Belastung_Querkraft";
1.19
1.20 -val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
1.21 +val t = rewrit @{thm Querkraft_Moment} (TermC.str2term "Q x = - q_0 * x + c"); term2s t;
1.22 if term2s t = "?M_b' x = - q_0 * x + c" then ()
1.23 (*if term2s t = "M_b' x = - q_0 * x + c" then () cf.fbe1652b0df8 new handling of quotes in mixfix*)
1.24 else error "/biegelinie.sml: Querkraft_Moment";
1.25
1.26 -val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.27 +val t = rewrit @{thm Moment_Neigung} (TermC.str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.28 term2s t;
1.29 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
1.30 else error "biegelinie.sml: Moment_Neigung";
1.31 @@ -70,15 +70,15 @@
1.32 Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in")
1.33 ],
1.34 scr = Empty_Prog};
1.35 -val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
1.36 -val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
1.37 +val rm_ = TermC.str2term"[M_b 0 = 0, M_b L = 0]";
1.38 +val M__ = TermC.str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
1.39 val SOME (e1__,_) = rewrite_set_ thy false srls
1.40 - (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
1.41 + (TermC.str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
1.42 if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
1.43
1.44 val SOME (x1__,_) =
1.45 rewrite_set_ thy false srls
1.46 - (str2term"argument_in (lhs (M_b 0 = 0))");
1.47 + (TermC.str2term"argument_in (lhs (M_b 0 = 0))");
1.48 if UnparseC.term x1__ = "0" then ()
1.49 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
1.50
1.51 @@ -118,8 +118,8 @@
1.52 "----------- investigate normalforms in biegelinien --------------";
1.53 "----------- investigate normalforms in biegelinien --------------";
1.54 "----- coming from integration, kept for later improvements:";
1.55 -val Q = str2term "Q x = c + -1 * q_0 * x";
1.56 -val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.57 -val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.58 -val y = str2term "y x = c_4 + c_3 * x +\n1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
1.59 +val Q = TermC.str2term "Q x = c + -1 * q_0 * x";
1.60 +val M_b = TermC.str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.61 +val y' = TermC.str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.62 +val y = TermC.str2term "y x = c_4 + c_3 * x +\n1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
1.63 (*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)