1 (* Knowledge for tests, specifically simplified or bound to a fixed state
2 for the purpose of simplifying tests.
3 Author: Walther Neuper 2003
4 (c) due to copyright terms
7 (0) revert import Test -- DiophantEq, this raises issues related to (1..4)
8 (1) transfer methods to respective theories, if only test, then hierarchy at ["...", "Test"]:
9 differentiate, root equatioh, polynomial equation, diophantine equation
10 (2) transfer problems accordingly
11 (3) rearrange rls according to (1..2)
12 (4) rearrange axiomatizations according to (3)
15 theory Test imports Base_Tools Poly Rational Root Diff begin
17 section \<open>consts for problems\<close>
19 "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
20 "contains'_root" :: "'a => bool" ("contains'_root _" 10)
22 "precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
23 "precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
24 "precond'_submet" :: "'a => bool" ("precond'_submet _" 10)
25 "precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
28 section \<open>functions\<close>
30 fun bin_o (Const (op_, (Type ("fun", [Type (s2, []), Type ("fun", [Type (s4, _),Type (s5, _)])]))))
31 = if s2 = s4 andalso s4 = s5 then [op_] else []
34 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
36 fun is_bin_op t = (bin_op t <> []);
38 fun bin_op_arg1 ((Const (_,
39 (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) $ arg1 $ _) = arg1
40 | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);
41 fun bin_op_arg2 ((Const (_,
42 (Type ("fun", [Type (_, []),Type ("fun", [Type _, Type _])]))))$ _ $ arg2) = arg2
43 | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);
45 exception NO_EQUATION_TERM;
46 fun is_equation ((Const ("HOL.eq",
47 (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ _ $ _) = true
48 | is_equation _ = false;
49 fun equ_lhs ((Const ("HOL.eq",
50 (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ l $ _) = l
51 | equ_lhs _ = raise NO_EQUATION_TERM;
52 fun equ_rhs ((Const ("HOL.eq", (Type ("fun",
53 [Type (_, []), Type ("fun", [Type (_, []), Type ("bool",[])])])))) $ _ $ r) = r
54 | equ_rhs _ = raise NO_EQUATION_TERM;
56 fun atom (Const (_, Type (_,[]))) = true
57 | atom (Free (_, Type (_,[]))) = true
58 | atom (Var (_, Type (_,[]))) = true
59 | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
62 fun varids (Const (s, Type (_,[]))) = [strip_thy s]
63 | varids (Free (s, Type (_,[]))) = if TermC.is_num' s then [] else [strip_thy s]
64 | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
65 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
66 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
67 | varids (Abs (a, _, t)) = union op = [a] (varids t)
68 | varids (t1 $ t2) = union op = (varids t1) (varids t2)
71 fun bin_ops_only ((Const op_) $ t1 $ t2) =
72 if is_bin_op (Const op_) then bin_ops_only t1 andalso bin_ops_only t2 else false
73 | bin_ops_only t = if atom t then true else bin_ops_only t;
75 fun polynomial opl t _(* bdVar TODO *) =
76 subset op = (bin_op t, opl) andalso (bin_ops_only t);
78 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
79 andalso polynomial opl (equ_lhs t) bdVar
80 andalso polynomial opl (equ_rhs t) bdVar
81 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
82 subset op = (varids bdVar, varids (equ_lhs t)));
84 fun max (a,b) = if a < b then b else a;
86 fun degree addl mul bdVar t =
88 fun deg _ _ v (Const (s, Type (_, []))) = if v=strip_thy s then 1 else 0
89 | deg _ _ v (Free (s, Type (_, []))) = if v=strip_thy s then 1 else 0
90 | deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy s then 1 else 0
91 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
92 | deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0
93 | deg addl mul v (h $ t1 $ t2) =
94 if subset op = (bin_op h, addl)
95 then max (deg addl mul v t1 , deg addl mul v t2)
96 else (*mul!*)(deg addl mul v t1) + (deg addl mul v t2)
97 | deg _ _ _ t = raise ERROR ("deg: t = " ^ UnparseC.term t)
99 if polynomial (addl @ [mul]) t bdVar
100 then SOME (deg addl mul (id_of bdVar) t)
101 else (NONE:int option)
103 fun degree_ addl mul bdVar t = (* do not export *)
107 in opt (degree addl mul bdVar t) end;
109 fun linear addl mul t bdVar = (degree_ addl mul bdVar t) < 2;
111 fun linear_equ addl mul bdVar t =
115 val degl = degree_ addl mul bdVar (equ_lhs t);
116 val degr = degree_ addl mul bdVar (equ_rhs t)
117 in if (degl>0 orelse degr>0)andalso max(degl,degr) < 2 then true else false end
119 (* strip_thy op_ before *)
120 fun is_div_op (dv, (Const (op_,
121 (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) ) = (dv = strip_thy op_)
122 | is_div_op _ = false;
124 fun is_denom bdVar div_op t =
125 let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
126 | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
127 | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
128 | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
129 | is bool[v]dv (h$n$d) =
131 then (is false[v]dv n)orelse(is true[v]dv d)
132 else (is bool [v]dv n)orelse(is bool[v]dv d)
133 in is false (varids bdVar) (strip_thy div_op) t end;
136 fun rational t div_op bdVar =
137 is_denom bdVar div_op t andalso bin_ops_only t;
141 section \<open>axiomatizations\<close>
142 axiomatization where (*TODO: prove as theorems*)
144 radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
145 rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
146 rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
147 rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
149 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
151 "m is_const ==> (n::real) + m * n = (1 + m) * n" and
152 rcollect_one_left_assoc:
153 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
154 rcollect_one_left_assoc_p:
155 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
157 rtwo_of_the_same: "a + a = 2 * a" and
158 rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
159 rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
161 rcancel_den: "not(a=0) ==> a * (b / a) = b" and
162 rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
163 rshift_nominator: "(a::real) * b / c = a / c * b" and
165 exp_pow: "(a \<up> b) \<up> c = a \<up> (b * c)" and
166 rsqare: "(a::real) * a = a \<up> 2" and
167 power_1: "(a::real) \<up> 1 = a" and
168 rbinom_power_2: "((a::real) + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and
170 rmult_1: "1 * k = (k::real)" and
171 rmult_1_right: "k * 1 = (k::real)" and
172 rmult_0: "0 * k = (0::real)" and
173 rmult_0_right: "k * 0 = (0::real)" and
174 radd_0: "0 + k = (k::real)" and
175 radd_0_right: "k + 0 = (k::real)" and
178 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
180 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
183 radd_commute: "(m::real) + (n::real) = n + m" and
184 radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
185 radd_assoc: "(m::real) + n + k = m + (n + k)" and
186 rmult_commute: "(m::real) * n = n * m" and
187 rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
188 rmult_assoc: "(m::real) * n * k = m * (n * k)" and
190 (*for equations: 'bdv' is a meta-constant*)
191 risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
192 risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
193 risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
196 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
198 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
199 root_ge0: "0 <= a ==> 0 <= sqrt a = True" and
200 (*should be dropped with better simplification in eval_rls ...*)
202 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
204 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
206 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
209 rroot_square_inv: "(sqrt a) \<up> 2 = a" and
210 rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
211 rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
212 rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
215 (*for root-equations*)
216 square_equation_left:
217 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b \<up> 2)))" and
218 square_equation_right:
219 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a \<up> 2)=b))" and
220 (*causes frequently non-termination:*)
222 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a \<up> 2)=b \<up> 2))" and
224 risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
225 risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
226 risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
228 (*for polynomial equations of degree 2; linear case in RatArith*)
229 mult_square: "(a*bdv \<up> 2 = b) = (bdv \<up> 2 = b / a)" and
230 constant_square: "(a + bdv \<up> 2 = b) = (bdv \<up> 2 = b + -1*a)" and
231 constant_mult_square: "(a + b*bdv \<up> 2 = c) = (b*bdv \<up> 2 = c + -1*a)" and
234 "0 <= a ==> (x \<up> 2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
236 "(x \<up> 2 = 0) = (x = 0)" and
238 (*isolate root on the LEFT hand side of the equation
239 otherwise shuffling from left to right would not terminate*)
242 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
244 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
245 rroot_to_lhs_add_mult:
246 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
247 (*17.9.02 aus SqRoot.thy------------------------------ \<up> ---*)
249 section \<open>eval functions\<close>
253 (** evaluation of numerals and predicates **)
255 (*does a term contain a root ?*)
256 fun eval_contains_root (thmid:string) _
257 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
258 if member op = (ids_of arg) "sqrt"
259 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
260 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
261 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
262 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
263 | eval_contains_root _ _ _ _ = NONE;
265 (*dummy precondition for root-met of x+1=2*)
266 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
267 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
268 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
269 | eval_precond_rootmet _ _ _ _ = NONE;
271 (*dummy precondition for root-pbl of x+1=2*)
272 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
273 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
274 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
275 | eval_precond_rootpbl _ _ _ _ = NONE;
277 setup \<open>KEStore_Elems.add_calcs
278 [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
279 ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
280 ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
281 eval_precond_rootpbl"#Test.precond_rootpbl_"))]
284 (*8.4.03 aus Poly.ML--------------------------------vvv---
285 make_polynomial ---> make_poly
286 ^-- for user ^-- for systest _ONLY_*)
288 local (*. for make_polytest .*)
290 open Term; (* for type order = EQUAL | LESS | GREATER *)
292 fun pr_ord EQUAL = "EQUAL"
293 | pr_ord LESS = "LESS"
294 | pr_ord GREATER = "GREATER";
296 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
298 "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
299 | _ => (((a, 0), T), 0))
300 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
301 | dest_hd' (Var v) = (v, 2)
302 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
303 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
305 fun get_order_pow (t $ (Free(order,_))) =
306 (case TermC.int_opt_of_string order of
309 | get_order_pow _ = 0;
311 fun size_of_term' (Const(str,_) $ t) =
312 if "Prog_Expr.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
313 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
314 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
315 | size_of_term' _ = 1;
316 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
317 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
319 | term_ord' pr thy (t, u) =
321 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
322 val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
323 commas(map UnparseC.term ts) ^ "]\"")
324 val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
325 commas(map UnparseC.term us) ^"]\"")
326 val _ = tracing ("size_of_term(t,u)= (" ^
327 string_of_int (size_of_term' t) ^ ", " ^
328 string_of_int (size_of_term' u) ^ ")")
329 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
330 val _ = tracing ("terms_ord(ts,us) = " ^
331 (pr_ord o terms_ord str false) (ts,us));
332 val _ = tracing "-------"
335 case int_ord (size_of_term' t, size_of_term' u) of
337 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
338 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
342 and hd_ord (f, g) = (* ~ term.ML *)
343 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
344 and terms_ord str pr (ts, us) =
345 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
348 fun ord_make_polytest (pr:bool) thy (_: subst) tu =
349 (term_ord' pr thy(***) tu = LESS );
354 section \<open>term order\<close>
356 fun term_order (_: subst) tu = (term_ordI [] tu = LESS);
359 section \<open>rulesets\<close>
362 Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
363 erls = Rule_Set.empty, srls = Rule_Set.Empty,
364 calc = [], errpatts = [],
365 rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),
366 Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),
367 Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
368 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
369 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
370 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
371 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
372 Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
373 Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),
374 Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
375 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
377 Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
378 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
380 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
381 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
382 Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
384 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
385 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
387 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")],
388 scr = Rule.Empty_Prog
392 (*.for evaluation of conditions in rewrite rules.*)
393 (*FIXXXXXXME 10.8.02: handle like _simplify*)
395 Rule_Def.Repeat{id = "tval_rls", preconds = [],
396 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
397 erls=testerls,srls = Rule_Set.empty,
398 calc=[], errpatts = [],
399 rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),
400 Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),
401 Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
402 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
403 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
404 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
405 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
406 Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
407 Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),
408 Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
409 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
411 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
413 Rule.Thm ("root_ge0",ThmC.numerals_to_Free @{thm root_ge0}),
414 Rule.Thm ("root_add_ge0",ThmC.numerals_to_Free @{thm root_add_ge0}),
415 Rule.Thm ("root_ge0_1",ThmC.numerals_to_Free @{thm root_ge0_1}),
416 Rule.Thm ("root_ge0_2",ThmC.numerals_to_Free @{thm root_ge0_2}),
418 Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
419 Rule.Eval ("Test.contains'_root", eval_contains_root "#eval_contains_root"),
420 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
421 Rule.Eval ("Test.contains'_root",
422 eval_contains_root"#contains_root_"),
424 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
425 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
426 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
427 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
429 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
430 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
432 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")],
433 scr = Rule.Empty_Prog
436 setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close>
439 (*make () dissappear*)
440 val rearrange_assoc =
441 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [],
442 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
443 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
445 [Rule.Thm ("sym_add.assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
446 Rule.Thm ("sym_rmult_assoc",ThmC.numerals_to_Free (@{thm rmult_assoc} RS @{thm sym}))],
447 scr = Rule.Empty_Prog
451 Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
452 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
454 [Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
455 Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
456 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
457 Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
458 Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
459 Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc})],
460 scr = Rule.Empty_Prog
463 (*todo: replace by Rewrite("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add)*)
465 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
466 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
467 rules = [Rule.Thm ("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add})
469 scr = Rule.Empty_Prog
473 (* expects * distributed over + *)
475 Rule_Def.Repeat{id = "Test_simplify", preconds = [],
476 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
477 erls = tval_rls, srls = Rule_Set.empty,
478 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
480 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
481 Rule.Thm ("radd_mult_distrib2",ThmC.numerals_to_Free @{thm radd_mult_distrib2}),
482 Rule.Thm ("rdistr_right_assoc",ThmC.numerals_to_Free @{thm rdistr_right_assoc}),
483 Rule.Thm ("rdistr_right_assoc_p",ThmC.numerals_to_Free @{thm rdistr_right_assoc_p}),
484 Rule.Thm ("rdistr_div_right",ThmC.numerals_to_Free @{thm rdistr_div_right}),
485 Rule.Thm ("rbinom_power_2",ThmC.numerals_to_Free @{thm rbinom_power_2}),
487 Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
488 Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
489 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
490 Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
491 Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
492 Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc}),
494 Rule.Thm ("radd_real_const_eq",ThmC.numerals_to_Free @{thm radd_real_const_eq}),
495 Rule.Thm ("radd_real_const",ThmC.numerals_to_Free @{thm radd_real_const}),
496 (* these 2 rules are invers to distr_div_right wrt. termination.
497 thus they MUST be done IMMEDIATELY before calc *)
498 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
499 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
500 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
501 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
503 Rule.Thm ("rcollect_right",ThmC.numerals_to_Free @{thm rcollect_right}),
504 Rule.Thm ("rcollect_one_left",ThmC.numerals_to_Free @{thm rcollect_one_left}),
505 Rule.Thm ("rcollect_one_left_assoc",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc}),
506 Rule.Thm ("rcollect_one_left_assoc_p",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc_p}),
508 Rule.Thm ("rshift_nominator",ThmC.numerals_to_Free @{thm rshift_nominator}),
509 Rule.Thm ("rcancel_den",ThmC.numerals_to_Free @{thm rcancel_den}),
510 Rule.Thm ("rroot_square_inv",ThmC.numerals_to_Free @{thm rroot_square_inv}),
511 Rule.Thm ("rroot_times_root",ThmC.numerals_to_Free @{thm rroot_times_root}),
512 Rule.Thm ("rroot_times_root_assoc_p",ThmC.numerals_to_Free @{thm rroot_times_root_assoc_p}),
513 Rule.Thm ("rsqare",ThmC.numerals_to_Free @{thm rsqare}),
514 Rule.Thm ("power_1",ThmC.numerals_to_Free @{thm power_1}),
515 Rule.Thm ("rtwo_of_the_same",ThmC.numerals_to_Free @{thm rtwo_of_the_same}),
516 Rule.Thm ("rtwo_of_the_same_assoc_p",ThmC.numerals_to_Free @{thm rtwo_of_the_same_assoc_p}),
518 Rule.Thm ("rmult_1",ThmC.numerals_to_Free @{thm rmult_1}),
519 Rule.Thm ("rmult_1_right",ThmC.numerals_to_Free @{thm rmult_1_right}),
520 Rule.Thm ("rmult_0",ThmC.numerals_to_Free @{thm rmult_0}),
521 Rule.Thm ("rmult_0_right",ThmC.numerals_to_Free @{thm rmult_0_right}),
522 Rule.Thm ("radd_0",ThmC.numerals_to_Free @{thm radd_0}),
523 Rule.Thm ("radd_0_right",ThmC.numerals_to_Free @{thm radd_0_right})
525 scr = Rule.Empty_Prog
526 (*since 040209 filled by prep_rls': STest_simplify*)
530 (*isolate the root in a root-equation*)
532 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
533 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
534 rules = [Rule.Thm ("rroot_to_lhs",ThmC.numerals_to_Free @{thm rroot_to_lhs}),
535 Rule.Thm ("rroot_to_lhs_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_mult}),
536 Rule.Thm ("rroot_to_lhs_add_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_add_mult}),
537 Rule.Thm ("risolate_root_add",ThmC.numerals_to_Free @{thm risolate_root_add}),
538 Rule.Thm ("risolate_root_mult",ThmC.numerals_to_Free @{thm risolate_root_mult}),
539 Rule.Thm ("risolate_root_div",ThmC.numerals_to_Free @{thm risolate_root_div}) ],
540 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy))
544 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
546 Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
547 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
549 [Rule.Thm ("risolate_bdv_add",ThmC.numerals_to_Free @{thm risolate_bdv_add}),
550 Rule.Thm ("risolate_bdv_mult_add",ThmC.numerals_to_Free @{thm risolate_bdv_mult_add}),
551 Rule.Thm ("risolate_bdv_mult",ThmC.numerals_to_Free @{thm risolate_bdv_mult}),
552 Rule.Thm ("mult_square",ThmC.numerals_to_Free @{thm mult_square}),
553 Rule.Thm ("constant_square",ThmC.numerals_to_Free @{thm constant_square}),
554 Rule.Thm ("constant_mult_square",ThmC.numerals_to_Free @{thm constant_mult_square})
556 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy))
560 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
561 setup \<open>KEStore_Elems.add_rlss
562 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)),
563 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)),
564 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
565 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
566 ("matches", (Context.theory_name @{theory}, prep_rls'
567 (Rule_Set.append_rules "matches" testerls [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])))]
570 subsection \<open>problems\<close>
571 (** problem types **)
572 setup \<open>KEStore_Elems.add_pbts
573 [(Problem.prep_input thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
574 (Problem.prep_input thy "pbl_test_equ" [] Problem.id_empty
575 (["equation", "test"],
576 [("#Given" ,["equality e_e", "solveFor v_v"]),
577 ("#Where" ,["matches (?a = ?b) e_e"]),
578 ("#Find" ,["solutions v_v'i'"])],
579 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
580 (Problem.prep_input thy "pbl_test_uni" [] Problem.id_empty
581 (["univariate", "equation", "test"],
582 [("#Given" ,["equality e_e", "solveFor v_v"]),
583 ("#Where" ,["matches (?a = ?b) e_e"]),
584 ("#Find" ,["solutions v_v'i'"])],
585 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
586 (Problem.prep_input thy "pbl_test_uni_lin" [] Problem.id_empty
587 (["LINEAR", "univariate", "equation", "test"],
588 [("#Given" ,["equality e_e", "solveFor v_v"]),
589 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
590 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
591 ("#Find" ,["solutions v_v'i'"])],
592 assoc_rls' @{theory} "matches",
593 SOME "solve (e_e::bool, v_v)", [["Test", "solve_linear"]]))]
596 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
597 [("termlessI", termlessI),
598 ("ord_make_polytest", ord_make_polytest false thy)
602 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
603 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
604 erls = testerls, srls = Rule_Set.Empty,
605 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
606 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
607 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
609 rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
610 (*"a - b = a + (-1) * b"*)
611 Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
612 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
613 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
614 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
615 Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
616 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
617 Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
618 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
619 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
621 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
623 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
627 Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
629 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
630 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
631 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
632 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
633 Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
635 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
636 (*x + (y + z) = y + (x + z)*)
637 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
638 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
640 Rule.Thm ("sym_realpow_twoI",
641 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
642 (*"r1 * r1 = r1 \<up> 2"*)
643 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
644 (*"r * r \<up> n = r \<up> (n + 1)"*)
645 Rule.Thm ("sym_real_mult_2",
646 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
647 (*"z1 + z1 = 2 * z1"*)
648 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
649 (*"z1 + (z1 + k) = 2 * z1 + k"*)
651 Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
652 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
653 Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
654 (*"[| l is_const; m is_const |] ==>
655 l * n + (m * n + k) = (l + m) * n + k"*)
656 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
657 (*"m is_const ==> n + m * n = (1 + m) * n"*)
658 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
659 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
661 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
662 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
663 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
665 scr = Rule.Empty_Prog(*Rule.Prog ((Thm.term_of o the o (parse thy))
669 val expand_binomtest =
670 Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
671 rew_ord = ("termlessI",termlessI),
672 erls = testerls, srls = Rule_Set.Empty,
673 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
674 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
675 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
678 [Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
679 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
680 Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
681 (*"(a + b)*(a + b) = ...*)
682 Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
683 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
684 Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),
685 (*"(a - b)*(a - b) = ...*)
686 Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
687 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
688 Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
689 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
691 Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
692 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
693 Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
694 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
695 Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
696 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
697 Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
698 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
699 Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
700 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
701 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
702 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
703 Rule.Thm ("real_minus_binom_pow3",ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
704 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
707 (* Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
708 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
709 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
710 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
711 Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
712 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
713 Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
714 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
717 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
719 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
721 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
724 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
725 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
726 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
728 Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
730 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
731 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
732 Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
733 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
734 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
737 Rule.Thm ("sym_realpow_twoI",
738 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
739 (*"r1 * r1 = r1 \<up> 2"*)
740 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
741 (*"r * r \<up> n = r \<up> (n + 1)"*)
742 (*Rule.Thm ("sym_real_mult_2",
743 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
744 (*"z1 + z1 = 2 * z1"*)*)
745 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
746 (*"z1 + (z1 + k) = 2 * z1 + k"*)
748 Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
749 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
750 Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
751 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
752 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
753 (*"m is_const ==> n + m * n = (1 + m) * n"*)
754 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
755 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
757 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
758 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
759 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
761 scr = Rule.Empty_Prog
762 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
765 setup \<open>KEStore_Elems.add_rlss
766 [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)),
767 ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\<close>
768 setup \<open>KEStore_Elems.add_rlss
769 [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)),
770 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)),
771 ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\<close>
773 section \<open>problems\<close>
774 setup \<open>KEStore_Elems.add_pbts
775 [(Problem.prep_input thy "pbl_test_uni_plain2" [] Problem.id_empty
776 (["plain_square", "univariate", "equation", "test"],
777 [("#Given" ,["equality e_e", "solveFor v_v"]),
778 ("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
779 "(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^
780 "(matches (?a + v_v \<up> 2 = 0) e_e) |" ^
781 "(matches ( v_v \<up> 2 = 0) e_e)"]),
782 ("#Find" ,["solutions v_v'i'"])],
783 assoc_rls' @{theory} "matches",
784 SOME "solve (e_e::bool, v_v)", [["Test", "solve_plain_square"]])),
785 (Problem.prep_input thy "pbl_test_uni_poly" [] Problem.id_empty
786 (["polynomial", "univariate", "equation", "test"],
787 [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
788 ("#Where" ,["HOL.False"]),
789 ("#Find" ,["solutions v_v'i'"])],
790 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
791 (Problem.prep_input thy "pbl_test_uni_poly_deg2" [] Problem.id_empty
792 (["degree_two", "polynomial", "univariate", "equation", "test"],
793 [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
794 ("#Find" ,["solutions v_v'i'"])],
795 Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
796 (Problem.prep_input thy "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
797 (["pq_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
798 [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
799 ("#Find" ,["solutions v_v'i'"])],
800 Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
801 (Problem.prep_input thy "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
802 (["abc_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
803 [("#Given" ,["equality (a_a * x \<up> 2 + b_b * x + c_c = 0)", "solveFor v_v"]),
804 ("#Find" ,["solutions v_v'i'"])],
805 Rule_Set.empty, SOME "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)", [])),
806 (Problem.prep_input thy "pbl_test_uni_root" [] Problem.id_empty
807 (["squareroot", "univariate", "equation", "test"],
808 [("#Given" ,["equality e_e", "solveFor v_v"]),
809 ("#Where" ,["precond_rootpbl v_v"]),
810 ("#Find" ,["solutions v_v'i'"])],
811 Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains'_root",
812 eval_contains_root "#contains_root_")],
813 SOME "solve (e_e::bool, v_v)", [["Test", "square_equation"]])),
814 (Problem.prep_input thy "pbl_test_uni_norm" [] Problem.id_empty
815 (["normalise", "univariate", "equation", "test"],
816 [("#Given" ,["equality e_e", "solveFor v_v"]),
818 ("#Find" ,["solutions v_v'i'"])],
819 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test", "norm_univar_equation"]])),
820 (Problem.prep_input thy "pbl_test_uni_roottest" [] Problem.id_empty
821 (["sqroot-test", "univariate", "equation", "test"],
822 [("#Given" ,["equality e_e", "solveFor v_v"]),
823 ("#Where" ,["precond_rootpbl v_v"]),
824 ("#Find" ,["solutions v_v'i'"])],
825 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
826 (Problem.prep_input thy "pbl_test_intsimp" [] Problem.id_empty
827 (["inttype", "test"],
828 [("#Given" ,["intTestGiven t_t"]),
830 ("#Find" ,["intTestFind s_s"])],
831 Rule_Set.empty, NONE, [["Test", "intsimp"]]))]\<close>
833 section \<open>methods\<close>
834 subsection \<open>differentiate\<close>
835 setup \<open>KEStore_Elems.add_mets
836 [MethodC.prep_input @{theory "Diff"} "met_test" [] MethodC.id_empty
838 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
839 crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
842 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
844 "solve_linear e_e v_v = (
847 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>
848 (Rewrite_Set ''Test_simplify'')) e_e
851 setup \<open>KEStore_Elems.add_mets
852 [MethodC.prep_input thy "met_test_solvelin" [] MethodC.id_empty
853 (["Test", "solve_linear"],
854 [("#Given" ,["equality e_e", "solveFor v_v"]),
855 ("#Where" ,["matches (?a = ?b) e_e"]),
856 ("#Find" ,["solutions v_v'i'"])],
857 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
858 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
859 nrls = Test_simplify},
860 @{thm solve_linear.simps})]
862 subsection \<open>root equation\<close>
864 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
866 "solve_root_equ e_e v_v = (
869 (While (contains_root e_e) Do (
870 (Rewrite ''square_equation_left'' ) #>
871 (Try (Rewrite_Set ''Test_simplify'' )) #>
872 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
873 (Try (Rewrite_Set ''isolate_root'' )) #>
874 (Try (Rewrite_Set ''Test_simplify'' )))) #>
875 (Try (Rewrite_Set ''norm_equation'' )) #>
876 (Try (Rewrite_Set ''Test_simplify'' )) #>
877 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>
878 (Try (Rewrite_Set ''Test_simplify'' ))
882 setup \<open>KEStore_Elems.add_mets
883 [MethodC.prep_input thy "met_test_sqrt" [] MethodC.id_empty
884 (*root-equation, version for tests before 8.01.01*)
885 (["Test", "sqrt-equ-test"],
886 [("#Given" ,["equality e_e", "solveFor v_v"]),
887 ("#Where" ,["contains_root (e_e::bool)"]),
888 ("#Find" ,["solutions v_v'i'"])],
889 {rew_ord'="e_rew_ord",rls'=tval_rls,
890 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
891 [Rule.Eval ("Test.contains'_root", eval_contains_root "")],
892 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
893 [Rule.Eval ("Test.contains'_root", eval_contains_root "")],
894 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
895 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
896 @{thm solve_root_equ.simps})]
899 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
901 "minisubpbl e_e v_v = (
904 (Try (Rewrite_Set ''norm_equation'' )) #>
905 (Try (Rewrite_Set ''Test_simplify'' ))) e_e;
906 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
907 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
909 Check_elementwise L_L {(v_v::real). Assumptions})"
910 setup \<open>KEStore_Elems.add_mets
911 [MethodC.prep_input thy "met_test_squ_sub" [] MethodC.id_empty
912 (*tests subproblem fixed linear*)
913 (["Test", "squ-equ-test-subpbl1"],
914 [("#Given" ,["equality e_e", "solveFor v_v"]),
915 ("#Where" ,["precond_rootmet v_v"]),
916 ("#Find" ,["solutions v_v'i'"])],
917 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
918 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
919 [Rule.Eval ("Test.precond'_rootmet", eval_precond_rootmet "")],
920 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
921 @{thm minisubpbl.simps})]
924 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
926 "solve_root_equ2 e_e v_v = (
929 (While (contains_root e_e) Do (
930 (Rewrite ''square_equation_left'' ) #>
931 (Try (Rewrite_Set ''Test_simplify'' )) #>
932 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
933 (Try (Rewrite_Set ''isolate_root'' )) #>
934 (Try (Rewrite_Set ''Test_simplify'' )))) #>
935 (Try (Rewrite_Set ''norm_equation'' )) #>
936 (Try (Rewrite_Set ''Test_simplify'' ))
938 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
939 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
941 Check_elementwise L_L {(v_v::real). Assumptions}) "
942 setup \<open>KEStore_Elems.add_mets
943 [MethodC.prep_input thy "met_test_eq1" [] MethodC.id_empty
945 (["Test", "square_equation1"],
946 [("#Given" ,["equality e_e", "solveFor v_v"]),
947 ("#Find" ,["solutions v_v'i'"])],
948 {rew_ord'="e_rew_ord",rls'=tval_rls,
949 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
950 [Rule.Eval ("Test.contains'_root", eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
951 errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),
952 ("square_equation_right", "")]*)},
953 @{thm solve_root_equ2.simps})]
956 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
958 "solve_root_equ3 e_e v_v = (
961 (While (contains_root e_e) Do ((
962 (Rewrite ''square_equation_left'' ) Or
963 (Rewrite ''square_equation_right'' )) #>
964 (Try (Rewrite_Set ''Test_simplify'' )) #>
965 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
966 (Try (Rewrite_Set ''isolate_root'' )) #>
967 (Try (Rewrite_Set ''Test_simplify'' )))) #>
968 (Try (Rewrite_Set ''norm_equation'' )) #>
969 (Try (Rewrite_Set ''Test_simplify'' ))
971 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
972 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
974 Check_elementwise L_L {(v_v::real). Assumptions})"
975 setup \<open>KEStore_Elems.add_mets
976 [MethodC.prep_input thy "met_test_squ2" [] MethodC.id_empty
978 (["Test", "square_equation2"],
979 [("#Given" ,["equality e_e", "solveFor v_v"]),
980 ("#Find" ,["solutions v_v'i'"])],
981 {rew_ord'="e_rew_ord",rls'=tval_rls,
982 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
983 [Rule.Eval ("Test.contains'_root", eval_contains_root"")],
984 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
985 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
986 @{thm solve_root_equ3.simps})]
989 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
991 "solve_root_equ4 e_e v_v = (
994 (While (contains_root e_e) Do ((
995 (Rewrite ''square_equation_left'' ) Or
996 (Rewrite ''square_equation_right'' )) #>
997 (Try (Rewrite_Set ''Test_simplify'' )) #>
998 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
999 (Try (Rewrite_Set ''isolate_root'' )) #>
1000 (Try (Rewrite_Set ''Test_simplify'' )))) #>
1001 (Try (Rewrite_Set ''norm_equation'' )) #>
1002 (Try (Rewrite_Set ''Test_simplify'' ))
1004 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
1005 [''no_met'']) [BOOL e_e, REAL v_v]
1007 Check_elementwise L_L {(v_v::real). Assumptions})"
1008 setup \<open>KEStore_Elems.add_mets
1009 [MethodC.prep_input thy "met_test_squeq" [] MethodC.id_empty
1011 (["Test", "square_equation"],
1012 [("#Given" ,["equality e_e", "solveFor v_v"]),
1013 ("#Find" ,["solutions v_v'i'"])],
1014 {rew_ord'="e_rew_ord",rls'=tval_rls,
1015 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
1016 [Rule.Eval ("Test.contains'_root", eval_contains_root"")],
1017 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
1018 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
1019 @{thm solve_root_equ4.simps})]
1022 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1024 "solve_plain_square e_e v_v = (
1027 (Try (Rewrite_Set ''isolate_bdv'' )) #>
1028 (Try (Rewrite_Set ''Test_simplify'' )) #>
1029 ((Rewrite ''square_equality_0'' ) Or
1030 (Rewrite ''square_equality'' )) #>
1031 (Try (Rewrite_Set ''tval_rls'' ))) e_e
1034 setup \<open>KEStore_Elems.add_mets
1035 [MethodC.prep_input thy "met_test_eq_plain" [] MethodC.id_empty
1036 (*solve_plain_square*)
1037 (["Test", "solve_plain_square"],
1038 [("#Given",["equality e_e", "solveFor v_v"]),
1039 ("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
1040 "(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^
1041 "(matches (?a + v_v \<up> 2 = 0) e_e) |" ^
1042 "(matches ( v_v \<up> 2 = 0) e_e)"]),
1043 ("#Find" ,["solutions v_v'i'"])],
1044 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
1045 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
1046 asm_rls=[],asm_thm=[]*)},
1047 @{thm solve_plain_square.simps})]
1049 subsection \<open>polynomial equation\<close>
1051 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1053 "norm_univariate_equ e_e v_v = (
1056 (Try (Rewrite ''rnorm_equation_add'' )) #>
1057 (Try (Rewrite_Set ''Test_simplify'' )) ) e_e
1059 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
1060 [''no_met'']) [BOOL e_e, REAL v_v])"
1061 setup \<open>KEStore_Elems.add_mets
1062 [MethodC.prep_input thy "met_test_norm_univ" [] MethodC.id_empty
1063 (["Test", "norm_univar_equation"],
1064 [("#Given",["equality e_e", "solveFor v_v"]),
1066 ("#Find" ,["solutions v_v'i'"])],
1067 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
1068 errpats = [], nrls = Rule_Set.empty},
1069 @{thm norm_univariate_equ.simps})]
1071 subsection \<open>diophantine equation\<close>
1073 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
1075 "test_simplify t_t = (
1077 (Try (Calculate ''PLUS'')) #>
1078 (Try (Calculate ''TIMES''))) t_t)"
1079 setup \<open>KEStore_Elems.add_mets
1080 [MethodC.prep_input thy "met_test_intsimp" [] MethodC.id_empty
1081 (["Test", "intsimp"],
1082 [("#Given" ,["intTestGiven t_t"]),
1084 ("#Find" ,["intTestFind s_s"])],
1085 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
1086 crls = tval_rls, errpats = [], nrls = Test_simplify},
1087 @{thm test_simplify.simps})]