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