1 (* tools for systems of equations over the reals |
|
2 author: Walther Neuper 050905, 08:51 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"Knowledge/EqSystem.ML"; |
|
6 use"EqSystem.ML"; |
|
7 |
|
8 remove_thy"EqSystem"; |
|
9 use_thy"Knowledge/Isac"; |
|
10 *) |
|
11 |
|
12 (** interface isabelle -- isac **) |
|
13 |
|
14 theory' := overwritel (!theory', [("EqSystem.thy",EqSystem.thy)]); |
|
15 |
|
16 (** eval functions **) |
|
17 |
|
18 (*certain variables of a given list occur _all_ in a term |
|
19 args: all: ..variables, which are under consideration (eg. the bound vars) |
|
20 vs: variables which must be in t, |
|
21 and none of the others in all must be in t |
|
22 t: the term under consideration |
|
23 *) |
|
24 fun occur_exactly_in vs all t = |
|
25 let fun occurs_in' a b = occurs_in b a |
|
26 in foldl and_ (true, map (occurs_in' t) vs) |
|
27 andalso not (foldl or_ (false, map (occurs_in' t) |
|
28 (subtract op = vs all))) |
|
29 end; |
|
30 |
|
31 (*("occur_exactly_in", ("EqSystem.occur'_exactly'_in", |
|
32 eval_occur_exactly_in "#eval_occur_exactly_in_"))*) |
|
33 fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in" |
|
34 (p as (Const ("EqSystem.occur'_exactly'_in",_) |
|
35 $ vs $ all $ t)) _ = |
|
36 if occur_exactly_in (isalist2list vs) (isalist2list all) t |
|
37 then SOME ((term2str p) ^ " = True", |
|
38 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
39 else SOME ((term2str p) ^ " = False", |
|
40 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
41 | eval_occur_exactly_in _ _ _ _ = NONE; |
|
42 |
|
43 calclist':= |
|
44 overwritel (!calclist', |
|
45 [("occur_exactly_in", |
|
46 ("EqSystem.occur'_exactly'_in", |
|
47 eval_occur_exactly_in "#eval_occur_exactly_in_")) |
|
48 ]); |
|
49 |
|
50 |
|
51 (** rewrite order 'ord_simplify_System' **) |
|
52 |
|
53 (* order wrt. several linear (i.e. without exponents) variables "c","c_2",.. |
|
54 which leaves the monomials containing c, c_2,... at the end of an Integral |
|
55 and puts the c, c_2,... rightmost within a monomial. |
|
56 |
|
57 WN050906 this is a quick and dirty adaption of ord_make_polynomial_in, |
|
58 which was most adequate, because it uses size_of_term*) |
|
59 (**) |
|
60 local (*. for simplify_System .*) |
|
61 (**) |
|
62 open Term; (* for type order = EQUAL | LESS | GREATER *) |
|
63 |
|
64 fun pr_ord EQUAL = "EQUAL" |
|
65 | pr_ord LESS = "LESS" |
|
66 | pr_ord GREATER = "GREATER"; |
|
67 |
|
68 fun dest_hd' (Const (a, T)) = (((a, 0), T), 0) |
|
69 | dest_hd' (Free (ccc, T)) = |
|
70 (case explode ccc of |
|
71 "c"::[] => ((("|||||||||||||||||||||", 0), T), 1)(*greatest string WN*) |
|
72 | "c"::"_"::_ => ((("|||||||||||||||||||||", 0), T), 1) |
|
73 | _ => (((ccc, 0), T), 1)) |
|
74 | dest_hd' (Var v) = (v, 2) |
|
75 | dest_hd' (Bound i) = ((("", i), dummyT), 3) |
|
76 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); |
|
77 |
|
78 fun size_of_term' (Free (ccc, _)) = |
|
79 (case explode ccc of (*WN0510 hack for the bound variables*) |
|
80 "c"::[] => 1000 |
|
81 | "c"::"_"::is => 1000 * ((str2int o implode) is) |
|
82 | _ => 1) |
|
83 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body |
|
84 | size_of_term' (f$t) = size_of_term' f + size_of_term' t |
|
85 | size_of_term' _ = 1; |
|
86 |
|
87 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) |
|
88 (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord) |
|
89 | term_ord' pr thy (t, u) = |
|
90 (if pr then |
|
91 let |
|
92 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
|
93 val _=writeln("t= f@ts= \""^ |
|
94 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
|
95 (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\""); |
|
96 val _=writeln("u= g@us= \""^ |
|
97 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
|
98 (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\""); |
|
99 val _=writeln("size_of_term(t,u)= ("^ |
|
100 (string_of_int(size_of_term' t))^", "^ |
|
101 (string_of_int(size_of_term' u))^")"); |
|
102 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
|
103 val _=writeln("terms_ord(ts,us) = "^ |
|
104 ((pr_ord o terms_ord str false)(ts,us))); |
|
105 val _=writeln("-------"); |
|
106 in () end |
|
107 else (); |
|
108 case int_ord (size_of_term' t, size_of_term' u) of |
|
109 EQUAL => |
|
110 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in |
|
111 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) |
|
112 | ord => ord) |
|
113 end |
|
114 | ord => ord) |
|
115 and hd_ord (f, g) = (* ~ term.ML *) |
|
116 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, |
|
117 dest_hd' g) |
|
118 and terms_ord str pr (ts, us) = |
|
119 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); |
|
120 (**) |
|
121 in |
|
122 (**) |
|
123 (*WN0510 for preliminary use in eval_order_system, see case-study mat-eng.tex |
|
124 fun ord_simplify_System_rev (pr:bool) thy subst tu = |
|
125 (term_ord' pr thy (Library.swap tu) = LESS);*) |
|
126 |
|
127 (*for the rls's*) |
|
128 fun ord_simplify_System (pr:bool) thy subst tu = |
|
129 (term_ord' pr thy tu = LESS); |
|
130 (**) |
|
131 end; |
|
132 (**) |
|
133 rew_ord' := overwritel (!rew_ord', |
|
134 [("ord_simplify_System", ord_simplify_System false thy) |
|
135 ]); |
|
136 |
|
137 |
|
138 (** rulesets **) |
|
139 |
|
140 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*) |
|
141 val order_add_mult_System = |
|
142 Rls{id = "order_add_mult_System", preconds = [], |
|
143 rew_ord = ("ord_simplify_System", |
|
144 ord_simplify_System false (theory "Integrate")), |
|
145 erls = e_rls,srls = Erls, calc = [], |
|
146 rules = [Thm ("real_mult_commute",num_str real_mult_commute), |
|
147 (* z * w = w * z *) |
|
148 Thm ("real_mult_left_commute",num_str real_mult_left_commute), |
|
149 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
|
150 Thm ("real_mult_assoc",num_str real_mult_assoc), |
|
151 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) |
|
152 Thm ("real_add_commute",num_str real_add_commute), |
|
153 (*z + w = w + z*) |
|
154 Thm ("real_add_left_commute",num_str real_add_left_commute), |
|
155 (*x + (y + z) = y + (x + z)*) |
|
156 Thm ("real_add_assoc",num_str real_add_assoc) |
|
157 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) |
|
158 ], |
|
159 scr = EmptyScr}:rls; |
|
160 |
|
161 (*.adapted from 'norm_Rational' by |
|
162 #1 using 'ord_simplify_System' in 'order_add_mult_System' |
|
163 #2 NOT using common_nominator_p .*) |
|
164 val norm_System_noadd_fractions = |
|
165 Rls {id = "norm_System_noadd_fractions", preconds = [], |
|
166 rew_ord = ("dummy_ord",dummy_ord), |
|
167 erls = norm_rat_erls, srls = Erls, calc = [], |
|
168 rules = [(*sequence given by operator precedence*) |
|
169 Rls_ discard_minus, |
|
170 Rls_ powers, |
|
171 Rls_ rat_mult_divide, |
|
172 Rls_ expand, |
|
173 Rls_ reduce_0_1_2, |
|
174 Rls_ (*order_add_mult #1*) order_add_mult_System, |
|
175 Rls_ collect_numerals, |
|
176 (*Rls_ add_fractions_p, #2*) |
|
177 Rls_ cancel_p |
|
178 ], |
|
179 scr = Script ((term_of o the o (parse thy)) |
|
180 "empty_script") |
|
181 }:rls; |
|
182 (*.adapted from 'norm_Rational' by |
|
183 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*) |
|
184 val norm_System = |
|
185 Rls {id = "norm_System", preconds = [], |
|
186 rew_ord = ("dummy_ord",dummy_ord), |
|
187 erls = norm_rat_erls, srls = Erls, calc = [], |
|
188 rules = [(*sequence given by operator precedence*) |
|
189 Rls_ discard_minus, |
|
190 Rls_ powers, |
|
191 Rls_ rat_mult_divide, |
|
192 Rls_ expand, |
|
193 Rls_ reduce_0_1_2, |
|
194 Rls_ (*order_add_mult *1*) order_add_mult_System, |
|
195 Rls_ collect_numerals, |
|
196 Rls_ add_fractions_p, |
|
197 Rls_ cancel_p |
|
198 ], |
|
199 scr = Script ((term_of o the o (parse thy)) |
|
200 "empty_script") |
|
201 }:rls; |
|
202 |
|
203 (*.simplify an equational system BEFORE solving it such that parentheses are |
|
204 ( ((u0*v0)*w0) + ( ((u1*v1)*w1) * c + ... +((u4*v4)*w4) * c_4 ) ) |
|
205 ATTENTION: works ONLY for bound variables c, c_1, c_2, c_3, c_4 :ATTENTION |
|
206 This is a copy from 'make_ratpoly_in' with respective reductions: |
|
207 *0* expand the term, ie. distribute * and / over + |
|
208 *1* ord_simplify_System instead of termlessI |
|
209 *2* no add_fractions_p (= common_nominator_p_rls !) |
|
210 *3* discard_parentheses only for (.*(.*.)) |
|
211 analoguous to simplify_Integral .*) |
|
212 val simplify_System_parenthesized = |
|
213 Seq {id = "simplify_System_parenthesized", preconds = []:term list, |
|
214 rew_ord = ("dummy_ord", dummy_ord), |
|
215 erls = Atools_erls, srls = Erls, calc = [], |
|
216 rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib), |
|
217 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
|
218 Thm ("real_add_divide_distrib",num_str real_add_divide_distrib), |
|
219 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
|
220 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
|
221 Rls_ norm_Rational_noadd_fractions(**2**), |
|
222 Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**), |
|
223 Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)) |
|
224 (*Rls_ discard_parentheses *3**), |
|
225 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) |
|
226 Rls_ separate_bdv2, |
|
227 Calc ("HOL.divide" ,eval_cancel "#divide_") |
|
228 ], |
|
229 scr = EmptyScr}:rls; |
|
230 |
|
231 (*.simplify an equational system AFTER solving it; |
|
232 This is a copy of 'make_ratpoly_in' with the differences |
|
233 *1* ord_simplify_System instead of termlessI .*) |
|
234 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *) |
|
235 val simplify_System = |
|
236 Seq {id = "simplify_System", preconds = []:term list, |
|
237 rew_ord = ("dummy_ord", dummy_ord), |
|
238 erls = Atools_erls, srls = Erls, calc = [], |
|
239 rules = [Rls_ norm_Rational, |
|
240 Rls_ (*order_add_mult_in*) norm_System (**1**), |
|
241 Rls_ discard_parentheses, |
|
242 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) |
|
243 Rls_ separate_bdv2, |
|
244 Calc ("HOL.divide" ,eval_cancel "#divide_") |
|
245 ], |
|
246 scr = EmptyScr}:rls; |
|
247 (* |
|
248 val simplify_System = |
|
249 append_rls "simplify_System" simplify_System_parenthesized |
|
250 [Thm ("sym_real_add_assoc", num_str (real_add_assoc RS sym))]; |
|
251 *) |
|
252 |
|
253 val isolate_bdvs = |
|
254 Rls {id="isolate_bdvs", preconds = [], |
|
255 rew_ord = ("e_rew_ord", e_rew_ord), |
|
256 erls = append_rls "erls_isolate_bdvs" e_rls |
|
257 [(Calc ("EqSystem.occur'_exactly'_in", |
|
258 eval_occur_exactly_in |
|
259 "#eval_occur_exactly_in_")) |
|
260 ], |
|
261 srls = Erls, calc = [], |
|
262 rules = [Thm ("commute_0_equality", |
|
263 num_str commute_0_equality), |
|
264 Thm ("separate_bdvs_add", num_str separate_bdvs_add), |
|
265 Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)], |
|
266 scr = EmptyScr}; |
|
267 val isolate_bdvs_4x4 = |
|
268 Rls {id="isolate_bdvs_4x4", preconds = [], |
|
269 rew_ord = ("e_rew_ord", e_rew_ord), |
|
270 erls = append_rls |
|
271 "erls_isolate_bdvs_4x4" e_rls |
|
272 [Calc ("EqSystem.occur'_exactly'_in", |
|
273 eval_occur_exactly_in "#eval_occur_exactly_in_"), |
|
274 Calc ("Atools.ident",eval_ident "#ident_"), |
|
275 Calc ("Atools.some'_occur'_in", |
|
276 eval_some_occur_in "#some_occur_in_"), |
|
277 Thm ("not_true",num_str not_true), |
|
278 Thm ("not_false",num_str not_false) |
|
279 ], |
|
280 srls = Erls, calc = [], |
|
281 rules = [Thm ("commute_0_equality", |
|
282 num_str commute_0_equality), |
|
283 Thm ("separate_bdvs0", num_str separate_bdvs0), |
|
284 Thm ("separate_bdvs_add1", num_str separate_bdvs_add1), |
|
285 Thm ("separate_bdvs_add1", num_str separate_bdvs_add2), |
|
286 Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)], |
|
287 scr = EmptyScr}; |
|
288 |
|
289 (*.order the equations in a system such, that a triangular system (if any) |
|
290 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*) |
|
291 val order_system = |
|
292 Rls {id="order_system", preconds = [], |
|
293 rew_ord = ("ord_simplify_System", |
|
294 ord_simplify_System false thy), |
|
295 erls = Erls, srls = Erls, calc = [], |
|
296 rules = [Thm ("order_system_NxN", num_str order_system_NxN) |
|
297 ], |
|
298 scr = EmptyScr}; |
|
299 |
|
300 val prls_triangular = |
|
301 Rls {id="prls_triangular", preconds = [], |
|
302 rew_ord = ("e_rew_ord", e_rew_ord), |
|
303 erls = Rls {id="erls_prls_triangular", preconds = [], |
|
304 rew_ord = ("e_rew_ord", e_rew_ord), |
|
305 erls = Erls, srls = Erls, calc = [], |
|
306 rules = [(*for precond nth_Cons_ ...*) |
|
307 Calc ("op <",eval_equ "#less_"), |
|
308 Calc ("op +", eval_binop "#add_") |
|
309 (*immediately repeated rewrite pushes |
|
310 '+' into precondition !*) |
|
311 ], |
|
312 scr = EmptyScr}, |
|
313 srls = Erls, calc = [], |
|
314 rules = [Thm ("nth_Cons_",num_str nth_Cons_), |
|
315 Calc ("op +", eval_binop "#add_"), |
|
316 Thm ("nth_Nil_",num_str nth_Nil_), |
|
317 Thm ("tl_Cons",num_str tl_Cons), |
|
318 Thm ("tl_Nil",num_str tl_Nil), |
|
319 Calc ("EqSystem.occur'_exactly'_in", |
|
320 eval_occur_exactly_in |
|
321 "#eval_occur_exactly_in_") |
|
322 ], |
|
323 scr = EmptyScr}; |
|
324 |
|
325 (*WN060914 quickly created for 4x4; |
|
326 more similarity to prls_triangular desirable*) |
|
327 val prls_triangular4 = |
|
328 Rls {id="prls_triangular4", preconds = [], |
|
329 rew_ord = ("e_rew_ord", e_rew_ord), |
|
330 erls = Rls {id="erls_prls_triangular4", preconds = [], |
|
331 rew_ord = ("e_rew_ord", e_rew_ord), |
|
332 erls = Erls, srls = Erls, calc = [], |
|
333 rules = [(*for precond nth_Cons_ ...*) |
|
334 Calc ("op <",eval_equ "#less_"), |
|
335 Calc ("op +", eval_binop "#add_") |
|
336 (*immediately repeated rewrite pushes |
|
337 '+' into precondition !*) |
|
338 ], |
|
339 scr = EmptyScr}, |
|
340 srls = Erls, calc = [], |
|
341 rules = [Thm ("nth_Cons_",num_str nth_Cons_), |
|
342 Calc ("op +", eval_binop "#add_"), |
|
343 Thm ("nth_Nil_",num_str nth_Nil_), |
|
344 Thm ("tl_Cons",num_str tl_Cons), |
|
345 Thm ("tl_Nil",num_str tl_Nil), |
|
346 Calc ("EqSystem.occur'_exactly'_in", |
|
347 eval_occur_exactly_in |
|
348 "#eval_occur_exactly_in_") |
|
349 ], |
|
350 scr = EmptyScr}; |
|
351 |
|
352 ruleset' := |
|
353 overwritelthy thy |
|
354 (!ruleset', |
|
355 [("simplify_System_parenthesized", prep_rls simplify_System_parenthesized), |
|
356 ("simplify_System", prep_rls simplify_System), |
|
357 ("isolate_bdvs", prep_rls isolate_bdvs), |
|
358 ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4), |
|
359 ("order_system", prep_rls order_system), |
|
360 ("order_add_mult_System", prep_rls order_add_mult_System), |
|
361 ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions), |
|
362 ("norm_System", prep_rls norm_System) |
|
363 ]); |
|
364 |
|
365 |
|
366 (** problems **) |
|
367 |
|
368 store_pbt |
|
369 (prep_pbt EqSystem.thy "pbl_equsys" [] e_pblID |
|
370 (["system"], |
|
371 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
372 ("#Find" ,["solution ss___"](*___ is copy-named*)) |
|
373 ], |
|
374 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
375 SOME "solveSystem es_ vs_", |
|
376 [])); |
|
377 store_pbt |
|
378 (prep_pbt EqSystem.thy "pbl_equsys_lin" [] e_pblID |
|
379 (["linear", "system"], |
|
380 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
381 (*TODO.WN050929 check linearity*) |
|
382 ("#Find" ,["solution ss___"]) |
|
383 ], |
|
384 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
385 SOME "solveSystem es_ vs_", |
|
386 [])); |
|
387 store_pbt |
|
388 (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2" [] e_pblID |
|
389 (["2x2", "linear", "system"], |
|
390 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
|
391 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
392 ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]), |
|
393 ("#Find" ,["solution ss___"]) |
|
394 ], |
|
395 append_rls "prls_2x2_linear_system" e_rls |
|
396 [Thm ("length_Cons_",num_str length_Cons_), |
|
397 Thm ("length_Nil_",num_str length_Nil_), |
|
398 Calc ("op +", eval_binop "#add_"), |
|
399 Calc ("op =",eval_equal "#equal_") |
|
400 ], |
|
401 SOME "solveSystem es_ vs_", |
|
402 [])); |
|
403 store_pbt |
|
404 (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2_tri" [] e_pblID |
|
405 (["triangular", "2x2", "linear", "system"], |
|
406 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
407 ("#Where" , |
|
408 ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", |
|
409 " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), |
|
410 ("#Find" ,["solution ss___"]) |
|
411 ], |
|
412 prls_triangular, |
|
413 SOME "solveSystem es_ vs_", |
|
414 [["EqSystem","top_down_substitution","2x2"]])); |
|
415 store_pbt |
|
416 (prep_pbt EqSystem.thy "pbl_equsys_lin_2x2_norm" [] e_pblID |
|
417 (["normalize", "2x2", "linear", "system"], |
|
418 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
419 ("#Find" ,["solution ss___"]) |
|
420 ], |
|
421 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
422 SOME "solveSystem es_ vs_", |
|
423 [["EqSystem","normalize","2x2"]])); |
|
424 store_pbt |
|
425 (prep_pbt EqSystem.thy "pbl_equsys_lin_3x3" [] e_pblID |
|
426 (["3x3", "linear", "system"], |
|
427 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
|
428 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
429 ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]), |
|
430 ("#Find" ,["solution ss___"]) |
|
431 ], |
|
432 append_rls "prls_3x3_linear_system" e_rls |
|
433 [Thm ("length_Cons_",num_str length_Cons_), |
|
434 Thm ("length_Nil_",num_str length_Nil_), |
|
435 Calc ("op +", eval_binop "#add_"), |
|
436 Calc ("op =",eval_equal "#equal_") |
|
437 ], |
|
438 SOME "solveSystem es_ vs_", |
|
439 [])); |
|
440 store_pbt |
|
441 (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4" [] e_pblID |
|
442 (["4x4", "linear", "system"], |
|
443 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
|
444 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
445 ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]), |
|
446 ("#Find" ,["solution ss___"]) |
|
447 ], |
|
448 append_rls "prls_4x4_linear_system" e_rls |
|
449 [Thm ("length_Cons_",num_str length_Cons_), |
|
450 Thm ("length_Nil_",num_str length_Nil_), |
|
451 Calc ("op +", eval_binop "#add_"), |
|
452 Calc ("op =",eval_equal "#equal_") |
|
453 ], |
|
454 SOME "solveSystem es_ vs_", |
|
455 [])); |
|
456 store_pbt |
|
457 (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID |
|
458 (["triangular", "4x4", "linear", "system"], |
|
459 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
460 ("#Where" , (*accepts missing variables up to diagional form*) |
|
461 ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", |
|
462 "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", |
|
463 "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", |
|
464 "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" |
|
465 ]), |
|
466 ("#Find" ,["solution ss___"]) |
|
467 ], |
|
468 append_rls "prls_tri_4x4_lin_sys" prls_triangular |
|
469 [Calc ("Atools.occurs'_in",eval_occurs_in "")], |
|
470 SOME "solveSystem es_ vs_", |
|
471 [["EqSystem","top_down_substitution","4x4"]])); |
|
472 |
|
473 store_pbt |
|
474 (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_norm" [] e_pblID |
|
475 (["normalize", "4x4", "linear", "system"], |
|
476 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
477 (*length_ is checked 1 level above*) |
|
478 ("#Find" ,["solution ss___"]) |
|
479 ], |
|
480 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
481 SOME "solveSystem es_ vs_", |
|
482 [["EqSystem","normalize","4x4"]])); |
|
483 |
|
484 |
|
485 (* show_ptyps(); |
|
486 *) |
|
487 |
|
488 (** methods **) |
|
489 |
|
490 store_met |
|
491 (prep_met EqSystem.thy "met_eqsys" [] e_metID |
|
492 (["EqSystem"], |
|
493 [], |
|
494 {rew_ord'="tless_true", rls' = Erls, calc = [], |
|
495 srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, |
|
496 "empty_script" |
|
497 )); |
|
498 store_met |
|
499 (prep_met EqSystem.thy "met_eqsys_topdown" [] e_metID |
|
500 (["EqSystem","top_down_substitution"], |
|
501 [], |
|
502 {rew_ord'="tless_true", rls' = Erls, calc = [], |
|
503 srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, |
|
504 "empty_script" |
|
505 )); |
|
506 store_met |
|
507 (prep_met EqSystem.thy "met_eqsys_topdown_2x2" [] e_metID |
|
508 (["EqSystem","top_down_substitution","2x2"], |
|
509 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
510 ("#Where" , |
|
511 ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", |
|
512 " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), |
|
513 ("#Find" ,["solution ss___"]) |
|
514 ], |
|
515 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], |
|
516 srls = append_rls "srls_top_down_2x2" e_rls |
|
517 [Thm ("hd_thm",num_str hd_thm), |
|
518 Thm ("tl_Cons",num_str tl_Cons), |
|
519 Thm ("tl_Nil",num_str tl_Nil) |
|
520 ], |
|
521 prls = prls_triangular, crls = Erls, nrls = Erls}, |
|
522 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
|
523 " (let e1__ = Take (hd es_); " ^ |
|
524 " e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
525 " isolate_bdvs False)) @@ " ^ |
|
526 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
527 " simplify_System False))) e1__; " ^ |
|
528 " e2__ = Take (hd (tl es_)); " ^ |
|
529 " e2__ = ((Substitute [e1__]) @@ " ^ |
|
530 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
531 " simplify_System_parenthesized False)) @@ " ^ |
|
532 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
533 " isolate_bdvs False)) @@ " ^ |
|
534 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
535 " simplify_System False))) e2__; " ^ |
|
536 " es__ = Take [e1__, e2__] " ^ |
|
537 " in (Try (Rewrite_Set order_system False)) es__)" |
|
538 (*--------------------------------------------------------------------------- |
|
539 this script does NOT separate the equations as abolve, |
|
540 but it does not yet work due to preliminary script-interpreter, |
|
541 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' |
|
542 |
|
543 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
|
544 " (let es__ = Take es_; " ^ |
|
545 " e1__ = hd es__; " ^ |
|
546 " e2__ = hd (tl es__); " ^ |
|
547 " es__ = [e1__, Substitute [e1__] e2__] " ^ |
|
548 " in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
549 " simplify_System_parenthesized False)) @@ " ^ |
|
550 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] " ^ |
|
551 " isolate_bdvs False)) @@ " ^ |
|
552 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
553 " simplify_System False))) es__)" |
|
554 ---------------------------------------------------------------------------*) |
|
555 )); |
|
556 store_met |
|
557 (prep_met EqSystem.thy "met_eqsys_norm" [] e_metID |
|
558 (["EqSystem","normalize"], |
|
559 [], |
|
560 {rew_ord'="tless_true", rls' = Erls, calc = [], |
|
561 srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, |
|
562 "empty_script" |
|
563 )); |
|
564 store_met |
|
565 (prep_met EqSystem.thy "met_eqsys_norm_2x2" [] e_metID |
|
566 (["EqSystem","normalize","2x2"], |
|
567 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
568 ("#Find" ,["solution ss___"])], |
|
569 {rew_ord'="tless_true", rls' = Erls, calc = [], |
|
570 srls = append_rls "srls_normalize_2x2" e_rls |
|
571 [Thm ("hd_thm",num_str hd_thm), |
|
572 Thm ("tl_Cons",num_str tl_Cons), |
|
573 Thm ("tl_Nil",num_str tl_Nil) |
|
574 ], |
|
575 prls = Erls, crls = Erls, nrls = Erls}, |
|
576 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
|
577 " (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
|
578 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
579 " simplify_System_parenthesized False)) @@ " ^ |
|
580 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
581 " isolate_bdvs False)) @@ " ^ |
|
582 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
|
583 " simplify_System_parenthesized False)) @@ " ^ |
|
584 " (Try (Rewrite_Set order_system False))) es_ " ^ |
|
585 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
|
586 " [bool_list_ es__, real_list_ vs_]))" |
|
587 )); |
|
588 |
|
589 (*this is for nth_ only*) |
|
590 val srls = Rls {id="srls_normalize_4x4", |
|
591 preconds = [], |
|
592 rew_ord = ("termlessI",termlessI), |
|
593 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
|
594 [(*for asm in nth_Cons_ ...*) |
|
595 Calc ("op <",eval_equ "#less_"), |
|
596 (*2nd nth_Cons_ pushes n+-1 into asms*) |
|
597 Calc("op +", eval_binop "#add_") |
|
598 ], |
|
599 srls = Erls, calc = [], |
|
600 rules = [Thm ("nth_Cons_",num_str nth_Cons_), |
|
601 Calc("op +", eval_binop "#add_"), |
|
602 Thm ("nth_Nil_",num_str nth_Nil_)], |
|
603 scr = EmptyScr}; |
|
604 store_met |
|
605 (prep_met EqSystem.thy "met_eqsys_norm_4x4" [] e_metID |
|
606 (["EqSystem","normalize","4x4"], |
|
607 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
608 ("#Find" ,["solution ss___"])], |
|
609 {rew_ord'="tless_true", rls' = Erls, calc = [], |
|
610 srls = append_rls "srls_normalize_4x4" srls |
|
611 [Thm ("hd_thm",num_str hd_thm), |
|
612 Thm ("tl_Cons",num_str tl_Cons), |
|
613 Thm ("tl_Nil",num_str tl_Nil) |
|
614 ], |
|
615 prls = Erls, crls = Erls, nrls = Erls}, |
|
616 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
617 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
|
618 " (let es__ = " ^ |
|
619 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
|
620 " (Repeat (Rewrite commute_0_equality False)) @@ " ^ |
|
621 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
|
622 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
|
623 " simplify_System_parenthesized False)) @@ " ^ |
|
624 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
|
625 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
|
626 " isolate_bdvs_4x4 False)) @@ " ^ |
|
627 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
|
628 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
|
629 " simplify_System_parenthesized False)) @@ " ^ |
|
630 " (Try (Rewrite_Set order_system False))) es_ " ^ |
|
631 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
|
632 " [bool_list_ es__, real_list_ vs_]))" |
|
633 )); |
|
634 store_met |
|
635 (prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID |
|
636 (["EqSystem","top_down_substitution","4x4"], |
|
637 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
638 ("#Where" , (*accepts missing variables up to diagonal form*) |
|
639 ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", |
|
640 "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", |
|
641 "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", |
|
642 "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" |
|
643 ]), |
|
644 ("#Find" ,["solution ss___"]) |
|
645 ], |
|
646 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], |
|
647 srls = append_rls "srls_top_down_4x4" srls [], |
|
648 prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular |
|
649 [Calc ("Atools.occurs'_in",eval_occurs_in "")], |
|
650 crls = Erls, nrls = Erls}, |
|
651 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
|
652 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
|
653 " (let e1_ = nth_ 1 es_; " ^ |
|
654 " e2_ = Take (nth_ 2 es_); " ^ |
|
655 " e2_ = ((Substitute [e1_]) @@ " ^ |
|
656 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ |
|
657 " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ |
|
658 " simplify_System_parenthesized False)) @@ " ^ |
|
659 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ |
|
660 " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ |
|
661 " isolate_bdvs False)) @@ " ^ |
|
662 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ |
|
663 " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ |
|
664 " norm_Rational False))) e2_ " ^ |
|
665 " in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])" |
|
666 )); |
|
667 |
|
668 (* show_mets(); |
|
669 *) |
|