(* Title:  Knowledge/biegelinie-1.sml

   Author: Walther Neuper 050826

   (c) due to copyright terms

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"------ biegelinie-1.sml -----------------------------------------";

"----------- the rules -------------------------------------------";

"----------- simplify_leaf for this script -----------------------";

"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

"----------- investigate normalforms in biegelinien --------------";

"-----------------------------------------------------------------";

"------ biegelinie-2.sml -----------------------------------------";

"----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";

"----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";

"-----------------------------------------------------------------";

"------ biegelinie-3.sml -----------------------------------------";

"----------- auto method [Biegelinien,setzeRandbedingungenEin]--------------------------------";

"----------- me method [Biegelinien,setzeRandbedingungenEin]----------------------------------";

"-----------------------------------------------------------------";

"------ biegelinie-4.sml -----------------------------------------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

val thy = @{theory "Biegelinie"};

val ctxt = ThyC.id_to_ctxt "Biegelinie";

fun str2term str = (Thm.term_of o the o (TermC.parse thy)) str;

fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;

fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));

"----------- the rules -------------------------------------------";

"----------- the rules -------------------------------------------";

"----------- the rules -------------------------------------------";

val t = rewrit @{thm Belastung_Querkraft} (TermC.str2term "- qq x = - q_0"); term2s t;

if term2s t = "Q' x = - q_0" then ()

else error  "/biegelinie.sml: Belastung_Querkraft";

val t = rewrit @{thm Querkraft_Moment} (TermC.str2term "Q x = - q_0 * x + c"); term2s t;

if term2s t = "?M_b' x = - q_0 * x + c" then ()

(*if term2s t = "M_b' x = - q_0 * x + c" then ()  cf.fbe1652b0df8 new handling of quotes in mixfix*)

else error  "/biegelinie.sml: Querkraft_Moment";

val t = rewrit @{thm Moment_Neigung} (TermC.str2term "M_b x = -q_0 * x \<up> 2/2 + q_0/2 *L*x");

    term2s t;

if term2s t = "- EI * y'' x = - q_0 * x \<up> 2 / 2 + q_0 / 2 * L * x" then ()

else error  "biegelinie.sml: Moment_Neigung";

"----------- simplify_leaf for this script -----------------------";

"----------- simplify_leaf for this script -----------------------";

"----------- simplify_leaf for this script -----------------------";

val srls = Rule_Set.Repeat {id="srls_IntegrierenUnd..", 

		preconds = [], 

		rew_ord = ("termlessI",termlessI), 

		erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty

				  [(*for asm in NTH_CONS ...*)

				   Eval ("Orderings.ord_class.less",eval_equ "#less_"),

				   (*2nd NTH_CONS pushes n+- 1 into asms*)

				   Eval("Groups.plus_class.plus", eval_binop "#add_")

				   ], 

		srls = Rule_Set.Empty, calc = [], errpatts = [],

		rules = [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),

			 Eval("Groups.plus_class.plus", eval_binop "#add_"),

			 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),

			 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"),

			 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"),

			 Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in")

			 ],

		scr = Empty_Prog};

val rm_ = TermC.str2term"[M_b 0 = 0, M_b L = 0]";

val M__ = TermC.str2term"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2";

val SOME (e1__,_) = rewrite_set_ thy false srls 

  (TermC.str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);

if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";

val SOME (x1__,_) = 

    rewrite_set_ thy false srls 

		 (TermC.str2term"argument_in (lhs (M_b 0 = 0))");

if UnparseC.term x1__ = "0" then ()

else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";

Rewrite.trace_on := false; (*true false*)

"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

val fmz = ["functionEq (M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)", 

	   "substitution (M_b L = 0)", 

	   "equality equ_equ"];

val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo", "equation"],

		     ["Equation", "fromFunction"]);

val p = e_pos'; val c = [];

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = 

			"M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = 

                        "M_b L = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2";

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = 

			"0 = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2";

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

if (* f2str f = "0 = c_2 + L * c + - 1 * q_0 / 2 * L \<up> 2" CHANGE NOT considered, already on leave*)

   f2str f = "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2"

then case nxt of End_Proof' => ()

  | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"

else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";

"----------- investigate normalforms in biegelinien --------------";

"----------- investigate normalforms in biegelinien --------------";

"----------- investigate normalforms in biegelinien --------------";

"----- coming from integration, kept for later improvements:";

val Q = TermC.str2term "Q x = c + - 1 * q_0 * x";

val M_b = TermC.str2term "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

val y' = TermC.str2term "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";

val y = TermC.str2term "y x = c_4 + c_3 * x +\n1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";

(* \<up>   1 / (- 1 * EI) NOT distributed - ok! \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)