1 (* Title: Knowledge/biegelinie-1.sml
2 Author: Walther Neuper 050826
3 (c) due to copyright terms
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "------ biegelinie-1.sml -----------------------------------------";
9 "----------- the rules -------------------------------------------";
10 "----------- simplify_leaf for this script -----------------------";
11 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
12 "----------- investigate normalforms in biegelinien --------------";
13 "-----------------------------------------------------------------";
14 "------ biegelinie-2.sml -----------------------------------------";
15 "----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";
16 "----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";
17 "-----------------------------------------------------------------";
18 "------ biegelinie-3.sml -----------------------------------------";
19 "----------- auto method [Biegelinien,setzeRandbedingungenEin]--------------------------------";
20 "----------- me method [Biegelinien,setzeRandbedingungenEin]----------------------------------";
21 "-----------------------------------------------------------------";
22 "------ biegelinie-4.sml -----------------------------------------";
23 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
24 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
25 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
26 "-----------------------------------------------------------------";
27 "-----------------------------------------------------------------";
28 "-----------------------------------------------------------------";
30 val thy = @{theory "Biegelinie"};
31 val ctxt = ThyC.id_to_ctxt "Biegelinie";
32 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
33 fun rewrit thm str = fst (the (rewrite_ ctxt tless_true Rule_Set.empty true thm str));
35 "----------- the rules -------------------------------------------";
36 "----------- the rules -------------------------------------------";
37 "----------- the rules -------------------------------------------";
38 val t = rewrit @{thm Belastung_Querkraft} (TermC.parse_test @{context} "- qq x = - q_0"); term2s t;
39 if term2s t = "Q' x = - q_0" then ()
40 else error "/biegelinie.sml: Belastung_Querkraft";
42 val t = rewrit @{thm Querkraft_Moment} (TermC.parse_test @{context} "Q x = - q_0 * x + c"); term2s t;
43 if term2s t = "?M_b' x = - q_0 * x + c" then ()
44 (*if term2s t = "M_b' x = - q_0 * x + c" then () cf.fbe1652b0df8 new handling of quotes in mixfix*)
45 else error "/biegelinie.sml: Querkraft_Moment";
47 val t = rewrit @{thm Moment_Neigung} (TermC.parse_test @{context} "M_b x = -q_0 * x \<up> 2/2 + q_0/2 *L*x");
49 if term2s t = "- EI * y'' x = - q_0 * x \<up> 2 / 2 + q_0 / 2 * L * x" then ()
50 else error "biegelinie.sml: Moment_Neigung";
52 "----------- simplify_leaf for this script -----------------------";
53 "----------- simplify_leaf for this script -----------------------";
54 "----------- simplify_leaf for this script -----------------------";
55 val srls = Rule_Set.Repeat {id="srls_IntegrierenUnd..",
57 rew_ord = ("termlessI",termlessI),
58 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
59 [(*for asm in NTH_CONS ...*)
60 Eval ("Orderings.ord_class.less",eval_equ "#less_"),
61 (*2nd NTH_CONS pushes n+- 1 into asms*)
62 Eval("Groups.plus_class.plus", Calc_Binop.numeric "#add_")
64 srls = Rule_Set.Empty, calc = [], errpatts = [],
65 rules = [Thm ("NTH_CONS", @{thm NTH_CONS}),
66 Eval("Groups.plus_class.plus", Calc_Binop.numeric "#add_"),
67 Thm ("NTH_NIL", @{thm NTH_NIL}),
68 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"),
69 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"),
70 Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in")
73 val rm_ = TermC.parse_test @{context}"[M_b 0 = 0, M_b L = 0]";
74 val M__ = TermC.parse_test @{context}"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2";
75 val SOME (e1__,_) = rewrite_set_ ctxt false srls
76 (TermC.parse_test @{context} "(NTH::[real,bool list]=>bool) 1 " $ rm_);
77 if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
79 val SOME (x1__,_) = rewrite_set_ ctxt false srls (TermC.parse_test @{context} "argument_in (lhs (M_b 0 = 0))");
80 if UnparseC.term x1__ = "0" then ()
81 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
84 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
85 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
86 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
87 val fmz = ["functionEq (M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)",
88 "substitution (M_b L = 0)",
90 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo", "equation"],
91 ["Equation", "fromFunction"]);
92 val p = e_pos'; val c = [];
93 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
97 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
100 "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
101 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
102 "M_b L = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2";
103 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
104 "0 = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2";
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
106 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
107 if (* f2str f = "0 = c_2 + L * c + - 1 * q_0 / 2 * L \<up> 2" CHANGE NOT considered, already on leave*)
108 f2str f = "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2"
109 then case nxt of End_Proof' => ()
110 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
111 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
113 "----------- investigate normalforms in biegelinien --------------";
114 "----------- investigate normalforms in biegelinien --------------";
115 "----------- investigate normalforms in biegelinien --------------";
116 "----- coming from integration, kept for later improvements:";
117 val Q = TermC.parse_test @{context} "Q x = c + - 1 * q_0 * x";
118 val M_b = TermC.parse_test @{context} "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
119 val y' = TermC.parse_test @{context} "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";
120 val y = TermC.parse_test @{context} "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)";
121 (* \<up> 1 / (- 1 * EI) NOT distributed - ok! \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^^*)