1 (* Title: Knowledge/eqsystem-2.sml |
1 (* Title: Knowledge/eqsystem-2.sml |
2 author: Walther Neuper 050826, |
2 author: Walther Neuper 050826, |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 |
5 |
6 Rewrite.trace_on := false; (*true false*) |
|
7 "-----------------------------------------------------------------"; |
6 "-----------------------------------------------------------------"; |
8 "table of contents -----------------------------------------------"; |
7 "table of contents -----------------------------------------------"; |
9 "-----------------------------------------------------------------"; |
8 "-----------------------------------------------------------------"; |
10 "----------- occur_exactly_in ------------------------------------"; |
9 "----------- occur_exactly_in ------------------------------------"; |
11 "----------- problems --------------------------------------------"; |
10 "----------- problems --------------------------------------------"; |
128 val t = TermC.str2term |
127 val t = TermC.str2term |
129 ("[0 = c_4, " ^ |
128 ("[0 = c_4, " ^ |
130 "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^ |
129 "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^ |
131 "0 = c_2, " ^ |
130 "0 = c_2, " ^ |
132 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"); |
131 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"); |
133 val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t; |
132 val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t; |
134 if UnparseC.term t = |
133 if UnparseC.term t = |
135 "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]" |
134 "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]" |
136 then () else error "Bsp 7.27"; |
135 then () else error "Bsp 7.27"; |
137 |
136 |
138 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
137 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
139 val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2"; |
138 val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2"; |
140 val NONE = rewrite_set_ thy false norm_Rational t; |
139 val NONE = rewrite_set_ ctxt false norm_Rational t; |
141 val SOME (t,_) = |
140 val SOME (t,_) = |
142 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
141 rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t; |
143 if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)" |
142 if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)" |
144 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
143 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
145 |
144 |
146 "--- isolate_bdvs_4x4"; |
145 "--- isolate_bdvs_4x4"; |
147 (* |
146 (* |
148 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
147 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t; |
149 UnparseC.term t; |
148 UnparseC.term t; |
150 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t; |
149 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t; |
151 UnparseC.term t; |
150 UnparseC.term t; |
152 val SOME (t,_) = rewrite_set_ thy false order_system t; |
151 val SOME (t,_) = rewrite_set_ ctxt false order_system t; |
153 UnparseC.term t; |
152 UnparseC.term t; |
154 *) |
153 *) |
155 |
154 |
156 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
155 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
157 reset_states (); |
156 reset_states (); |
206 val t = TermC.str2term |
205 val t = TermC.str2term |
207 ("[L * q_0 = c, " ^ |
206 ("[L * q_0 = c, " ^ |
208 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
207 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
209 "0 = c_4, " ^ |
208 "0 = c_4, " ^ |
210 "0 = c_3]"); |
209 "0 = c_3]"); |
211 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
210 val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
212 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
211 val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
213 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
212 val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
214 if UnparseC.term t = |
213 if UnparseC.term t = |
215 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" |
214 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" |
216 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
215 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
217 |
216 |
218 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
217 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t; |
219 if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]" |
218 if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]" |
220 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2"; |
219 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2"; |
221 |
220 |
222 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
221 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t; |
223 if UnparseC.term t = |
222 if UnparseC.term t = |
224 "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^ |
223 "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^ |
225 " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]" |
224 " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]" |
226 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3"; |
225 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3"; |
227 |
226 |
228 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
227 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t; |
229 if UnparseC.term t = |
228 if UnparseC.term t = |
230 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]" |
229 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]" |
231 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4"; |
230 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4"; |
232 |
231 |
233 val SOME (t, _) = rewrite_set_ thy false order_system t; |
232 val SOME (t, _) = rewrite_set_ ctxt false order_system t; |
234 if UnparseC.term t = |
233 if UnparseC.term t = |
235 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]" |
234 "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]" |
236 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed"; |
235 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed"; |
237 |
236 |
238 "----- 7.70 with met normalise: "; |
237 "----- 7.70 with met normalise: "; |