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