test/Tools/isac/Knowledge/biegelinie-1.sml
changeset 60230 0ca0f9363ad3
parent 60083 6285d1b216ae
child 60237 e534316f9e07
     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! ^^^^^^^^^^^^^^^^^^^^^^^*)