122 "----------- rewrite-order ord_simplify_System -------------------"; |
122 "----------- rewrite-order ord_simplify_System -------------------"; |
123 "----------- rewrite-order ord_simplify_System -------------------"; |
123 "----------- rewrite-order ord_simplify_System -------------------"; |
124 "----------- rewrite-order ord_simplify_System -------------------"; |
124 "----------- rewrite-order ord_simplify_System -------------------"; |
125 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2"; |
125 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2"; |
126 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *) |
126 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *) |
127 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", |
127 if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", |
128 TermC.parse_test @{context}"c * x") then () |
128 TermC.parse_test @{context}"c * x") then () |
129 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1"; |
129 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1"; |
130 |
130 |
131 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", |
131 if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", |
132 TermC.parse_test @{context}"c_2") then () |
132 TermC.parse_test @{context}"c_2") then () |
133 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2"; |
133 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2"; |
134 |
134 |
135 if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x", |
135 if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x", |
136 TermC.parse_test @{context}"c_2") then () |
136 TermC.parse_test @{context}"c_2") then () |
137 else error "integrate.sml, (c * x) < (c_2) not#3"; |
137 else error "integrate.sml, (c * x) < (c_2) not#3"; |
138 |
138 |
139 "--- mult.commute ---"; |
139 "--- mult.commute ---"; |
140 if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c", |
140 if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c", |
141 TermC.parse_test @{context}"c * x") then () |
141 TermC.parse_test @{context}"c * x") then () |
142 else error "integrate.sml, (x * c) < (c * x) not#4"; |
142 else error "integrate.sml, (x * c) < (c * x) not#4"; |
143 |
143 |
144 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", |
144 if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", |
145 TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") |
145 TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") |
146 then () else error "integrate.sml, (. * .) < (. * .) not#5"; |
146 then () else error "integrate.sml, (. * .) < (. * .) not#5"; |
147 |
147 |
148 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", |
148 if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", |
149 TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") |
149 TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") |
150 then () else error "integrate.sml, (. * .) < (. * .) not#6"; |
150 then () else error "integrate.sml, (. * .) < (. * .) not#6"; |
151 |
151 |
152 |
152 |
153 "----------- rewrite in [EqSystem,normalise,2x2] -----------------"; |
153 "----------- rewrite in [EqSystem,normalise,2x2] -----------------"; |
238 val SOME (t,_) = rewrite_set_ ctxt true order_system t; |
238 val SOME (t,_) = rewrite_set_ ctxt true order_system t; |
239 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then () |
239 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then () |
240 else error "eqsystem.sml top_down_substitution,2x2] order_system"; |
240 else error "eqsystem.sml top_down_substitution,2x2] order_system"; |
241 |
241 |
242 if not (ord_simplify_System |
242 if not (ord_simplify_System |
243 false thy [] |
243 false ctxt [] |
244 (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", |
244 (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", |
245 TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) |
245 TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) |
246 then () else error "eqsystem.sml, order_result rew_ord"; |
246 then () else error "eqsystem.sml, order_result rew_ord"; |
247 |
247 |
248 |
248 |