106 "----------- all systems from Biegelinie -------------------------"; |
106 "----------- all systems from Biegelinie -------------------------"; |
107 "----------- all systems from Biegelinie -------------------------"; |
107 "----------- all systems from Biegelinie -------------------------"; |
108 "----------- all systems from Biegelinie -------------------------"; |
108 "----------- all systems from Biegelinie -------------------------"; |
109 val thy = @{theory Isac_Knowledge} |
109 val thy = @{theory Isac_Knowledge} |
110 val subst = |
110 val subst = |
111 [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"), |
111 [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"), (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"), |
112 (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")]; |
112 (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"), (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")]; |
113 |
113 |
114 "------- Bsp 7.27"; |
114 "------- Bsp 7.27"; |
115 States.reset (); |
115 States.reset (); |
116 CalcTree [( |
116 CalcTree [( |
117 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", |
117 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", |
123 ##7.27## ordered substs |
123 ##7.27## ordered substs |
124 c_4 c_2 |
124 c_4 c_2 |
125 c c_2 c_3 c_4 c c_2 1->2: c |
125 c c_2 c_3 c_4 c c_2 1->2: c |
126 c_2 c_4 |
126 c_2 c_4 |
127 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*) |
127 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*) |
128 val t = TermC.str2term |
128 val t = TermC.parse_test @{context} |
129 ("[0 = c_4, " ^ |
129 ("[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), " ^ |
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), " ^ |
131 "0 = c_2, " ^ |
131 "0 = c_2, " ^ |
132 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"); |
132 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"); |
133 val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t; |
133 val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t; |
134 if UnparseC.term t = |
134 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]" |
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]" |
136 then () else error "Bsp 7.27"; |
136 then () else error "Bsp 7.27"; |
137 |
137 |
138 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
138 "----- 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"; |
139 val t = TermC.parse_test @{context} "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2"; |
140 val NONE = rewrite_set_ ctxt false norm_Rational t; |
140 val NONE = rewrite_set_ ctxt false norm_Rational t; |
141 val SOME (t,_) = |
141 val SOME (t,_) = |
142 rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t; |
142 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)" |
143 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"; |
144 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
179 ##7.69## ordered subst 2x2 |
179 ##7.69## ordered subst 2x2 |
180 c_4 c_3 |
180 c_4 c_3 |
181 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2 |
181 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2 |
182 c_3 c_4 |
182 c_3 c_4 |
183 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*) |
183 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*) |
184 val t = TermC.str2term |
184 val t = TermC.parse_test @{context} |
185 ("[0 = c_4 + 0 / (- 1 * EI), " ^ |
185 ("[0 = c_4 + 0 / (- 1 * EI), " ^ |
186 "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), " ^ |
186 "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), " ^ |
187 "0 = c_3 + 0 / (- 1 * EI), " ^ |
187 "0 = c_3 + 0 / (- 1 * EI), " ^ |
188 "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]"); |
188 "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]"); |
189 |
189 |
201 c c_2 |1:c -> 2:c_2 |
201 c c_2 |1:c -> 2:c_2 |
202 c_3 | |
202 c_3 | |
203 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*) |
203 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*) |
204 |
204 |
205 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4"; |
205 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4"; |
206 val t = TermC.str2term |
206 val t = TermC.parse_test @{context} |
207 ("[L * q_0 = c, " ^ |
207 ("[L * q_0 = c, " ^ |
208 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
208 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
209 "0 = c_4, " ^ |
209 "0 = c_4, " ^ |
210 "0 = c_3]"); |
210 "0 = c_3]"); |
211 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t; |
211 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t; |
319 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal |
319 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal |
320 c c_2 |c c_2 |1' |1': c c_2 | |
320 c c_2 |c c_2 |1' |1': c c_2 | |
321 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | | |
321 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | | |
322 c c_2 c_3 c_4 | c_4 |3' | | |
322 c c_2 c_3 c_4 | c_4 |3' | | |
323 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *) |
323 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *) |
324 val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \ |
324 val t = TermC.parse_test @{context}"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \ |
325 \ 0 = c_4 + 0 / (- 1 * EI), \ |
325 \ 0 = c_4 + 0 / (- 1 * EI), \ |
326 \ 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),\ |
326 \ 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),\ |
327 \ 0 = c_3 + 0 / (- 1 * EI)]"; |
327 \ 0 = c_3 + 0 / (- 1 * EI)]"; |
328 |
328 |
329 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
329 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
354 ##7.72b## |ord. |subst.singles |ord.triang. |
354 ##7.72b## |ord. |subst.singles |ord.triang. |
355 c_2 | | |c_2 |
355 c_2 | | |c_2 |
356 c c_2 | |1:c_2 -> 2':c |c_2 c |
356 c c_2 | |1:c_2 -> 2':c |c_2 c |
357 c_4 | | | |
357 c_4 | | | |
358 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*) |
358 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*) |
359 val t = TermC.str2term"[0 = c_2, \ |
359 val t = TermC.parse_test @{context}"[0 = c_2, \ |
360 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \ |
360 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \ |
361 \ 0 = c_4 + 0 / (- 1 * EI), \ |
361 \ 0 = c_4 + 0 / (- 1 * EI), \ |
362 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]"; |
362 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]"; |
363 |
363 |
364 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
364 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |