2 author: Walther Neuper 050826
3 (c) due to copyright terms
5 trace_rewrite := false;
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "----------- the rules -------------------------------------------";
10 "----------- simplify_leaf for this script -----------------------";
11 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
12 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
13 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
14 "----------- investigate normalforms in biegelinien --------------";
15 "-----------------------------------------------------------------";
16 "-----------------------------------------------------------------";
17 "-----------------------------------------------------------------";
19 val thy = @{theory "Biegelinie"};
20 val ctxt = thy2ctxt' "Biegelinie";
21 fun str2term str = (Thm.term_of o the o (parse thy)) str;
22 fun term2s t = term_to_string'' "Biegelinie" t;
24 fst (the (rewrite_ thy tless_true e_rls true thm str));
26 "----------- the rules -------------------------------------------";
27 "----------- the rules -------------------------------------------";
28 "----------- the rules -------------------------------------------";
29 val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
30 if term2s t = "Q' x = - q_0" then ()
31 else error "/biegelinie.sml: Belastung_Querkraft";
33 val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
34 if term2s t = "M_b' x = - q_0 * x + c" then ()
35 else error "/biegelinie.sml: Querkraft_Moment";
37 val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
39 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
40 else error "biegelinie.sml: Moment_Neigung";
42 "----------- simplify_leaf for this script -----------------------";
43 "----------- simplify_leaf for this script -----------------------";
44 "----------- simplify_leaf for this script -----------------------";
45 val srls = Rls {id="srls_IntegrierenUnd..",
47 rew_ord = ("termlessI",termlessI),
48 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
49 [(*for asm in NTH_CONS ...*)
50 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
51 (*2nd NTH_CONS pushes n+-1 into asms*)
52 Calc("Groups.plus_class.plus", eval_binop "#add_")
54 srls = Erls, calc = [], errpatts = [],
55 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
56 Calc("Groups.plus_class.plus", eval_binop "#add_"),
57 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
58 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
59 Calc("Tools.rhs", eval_rhs "eval_rhs_"),
60 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
63 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
64 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
65 val SOME (e1__,_) = rewrite_set_ thy false srls
66 (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
67 if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
70 rewrite_set_ thy false srls
71 (str2term"argument_in (lhs (M_b 0 = 0))");
72 if term2str x1__ = "0" then ()
73 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
75 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
78 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
79 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
80 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
82 ["Streckenlast q_0","FunktionsVariable x",
83 "Funktionen [Q x = c + -1 * q_0 * x, \
84 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
85 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
86 \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"];
87 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
88 ["Biegelinien","ausBelastung"]);
89 val p = e_pos'; val c = [];
90 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
91 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
92 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
93 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
94 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
95 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
96 | _ => error "biegelinie.sml met2 b";
98 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
99 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
100 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
101 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
102 | _ => error "biegelinie.sml met2 c";
104 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
105 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
106 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
107 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
108 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
110 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
111 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
112 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
113 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
114 | _ => error "biegelinie.sml met2 d";
116 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
117 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
118 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
119 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
120 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
121 "M_b x = Integral c + -1 * q_0 * x D x";
122 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
123 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
124 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
125 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
127 "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
129 "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
130 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
131 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
132 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
133 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
134 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
135 "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
137 "y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
139 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
141 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
142 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
143 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
144 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
145 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
146 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
147 "y x =\nIntegral c_3 +\n 1 / (-1 * EI) *\n (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x";
148 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
149 "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
150 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
151 "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
152 val (p,_,f,nxt,_,pt) = me nxt p c pt;
154 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"
155 then case nxt of ("End_Proof'", End_Proof') => ()
156 | _ => error "biegelinie.sml met2 e 1"
157 else error "biegelinie.sml met2 e 2";
159 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
160 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
161 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
162 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
163 "substitution (M_b L = 0)",
165 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
166 ["Equation","fromFunction"]);
167 val p = e_pos'; val c = [];
168 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
169 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
170 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
171 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
172 val (p,_,f,nxt,_,pt) = me nxt p c pt;
174 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
175 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
177 "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
178 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
179 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
180 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
181 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
182 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
183 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
184 then case nxt of ("End_Proof'", End_Proof') => ()
185 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
186 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";