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 (*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------* )
12 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
13 ( *-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
14 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
15 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
16 "----------- investigate normalforms in biegelinien --------------";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
21 val thy = @{theory "Biegelinie"};
22 val ctxt = thy2ctxt' "Biegelinie";
23 fun str2term str = (Thm.term_of o the o (parse thy)) str;
24 fun term2s t = term_to_string'' "Biegelinie" t;
26 fst (the (rewrite_ thy tless_true e_rls true thm str));
28 "----------- the rules -------------------------------------------";
29 "----------- the rules -------------------------------------------";
30 "----------- the rules -------------------------------------------";
31 val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
32 if term2s t = "Q' x = - q_0" then ()
33 else error "/biegelinie.sml: Belastung_Querkraft";
35 val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
36 if term2s t = "M_b' x = - q_0 * x + c" then ()
37 else error "/biegelinie.sml: Querkraft_Moment";
39 val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
41 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
42 else error "biegelinie.sml: Moment_Neigung";
44 "----------- simplify_leaf for this script -----------------------";
45 "----------- simplify_leaf for this script -----------------------";
46 "----------- simplify_leaf for this script -----------------------";
47 val srls = Rls {id="srls_IntegrierenUnd..",
49 rew_ord = ("termlessI",termlessI),
50 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
51 [(*for asm in NTH_CONS ...*)
52 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
53 (*2nd NTH_CONS pushes n+-1 into asms*)
54 Calc("Groups.plus_class.plus", eval_binop "#add_")
56 srls = Erls, calc = [], errpatts = [],
57 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
58 Calc("Groups.plus_class.plus", eval_binop "#add_"),
59 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
60 Calc("Prog_Expr.lhs", eval_lhs "eval_lhs_"),
61 Calc("Prog_Expr.rhs", eval_rhs "eval_rhs_"),
62 Calc("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in")
65 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
66 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
67 val SOME (e1__,_) = rewrite_set_ thy false srls
68 (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
69 if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
72 rewrite_set_ thy false srls
73 (str2term"argument_in (lhs (M_b 0 = 0))");
74 if term2str x1__ = "0" then ()
75 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
77 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
80 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
81 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
82 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
84 ["Streckenlast q_0","FunktionsVariable x",
85 "Funktionen [Q x = c + -1 * q_0 * x, \
86 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
87 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
88 \ 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)]",
89 "AbleitungBiegelinie dy"];
90 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
91 ["Biegelinien","ausBelastung"]);
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
98 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
100 | _ => error "biegelinie.sml met2 b";
102 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
103 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
104 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
105 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
106 | _ => error "biegelinie.sml met2 c";
108 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
109 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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
111 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
112 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
114 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
115 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
116 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
117 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
118 | _ => error "biegelinie.sml met2 d";
120 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
121 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
122 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
123 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
124 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
125 "M_b x = Integral c + -1 * q_0 * x D x";
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
127 "M_b 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 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
130 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
131 "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
133 "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
134 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
135 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
139 "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
140 (*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------* )
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
142 "y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
143 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
144 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
145 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
146 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
147 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
148 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
149 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
150 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
151 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
152 "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";
153 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
154 "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)";
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
156 "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)";
157 val (p,_,f,nxt,_,pt) = me nxt p c pt;
159 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n dy 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)]"
160 then case nxt of ("End_Proof'", End_Proof') => ()
161 | _ => error "biegelinie.sml met2 e 1"
162 else error "biegelinie.sml met2 e 2";
163 ( *-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
165 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
166 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
167 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
168 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
169 "substitution (M_b L = 0)",
171 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
172 ["Equation","fromFunction"]);
173 val p = e_pos'; val c = [];
174 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
175 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
176 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
177 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
178 val (p,_,f,nxt,_,pt) = me nxt p c pt;
180 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
181 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
182 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
183 "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
184 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
185 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
186 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
188 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
189 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
190 then case nxt of ("End_Proof'", End_Proof') => ()
191 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
192 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";