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 (\<^type_name>\<open>fun\<close>, [Type (s2, []), Type (\<^type_name>\<open>fun\<close>, [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 (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) $ arg1 $ _) = arg1
40 | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term @{context} t);
41 fun bin_op_arg2 ((Const (_,
42 (Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])]))))$ _ $ arg2) = arg2
43 | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term @{context} t);
45 exception NO_EQUATION_TERM;
46 fun is_equation ((Const (\<^const_name>\<open>HOL.eq\<close>,
47 (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ _) = true
48 | is_equation _ = false;
49 fun equ_lhs ((Const (\<^const_name>\<open>HOL.eq\<close>,
50 (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ l $ _) = l
51 | equ_lhs _ = raise NO_EQUATION_TERM;
52 fun equ_rhs ((Const (\<^const_name>\<open>HOL.eq\<close>, (Type (\<^type_name>\<open>fun\<close>,
53 [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ 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 (\<^const_name>\<open>numeral\<close>, _) $ _) = []
63 | varids (Const (s, Type (_,[]))) = [ThmC.cut_longid s]
64 | varids (Free (s, Type (_,[]))) = [ThmC.cut_longid s]
65 | varids (Var((s, _),Type (_,[]))) = [ThmC.cut_longid s]
66 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
67 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
68 | varids (Abs (a, _, t)) = union op = [a] (varids t)
69 | varids (t1 $ t2) = union op = (varids t1) (varids t2)
72 fun bin_ops_only ((Const op_) $ t1 $ t2) =
73 if is_bin_op (Const op_) then bin_ops_only t1 andalso bin_ops_only t2 else false
74 | bin_ops_only t = if atom t then true else bin_ops_only t;
76 fun polynomial opl t _(* bdVar TODO *) =
77 subset op = (bin_op t, opl) andalso (bin_ops_only t);
79 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
80 andalso polynomial opl (equ_lhs t) bdVar
81 andalso polynomial opl (equ_rhs t) bdVar
82 andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
83 subset op = (varids bdVar, varids (equ_lhs t)));
85 fun max (a,b) = if a < b then b else a;
87 fun degree addl mul bdVar t =
89 fun deg _ _ v (Const (s, Type (_, []))) = if v=ThmC.cut_longid s then 1 else 0
90 | deg _ _ v (Free (s, Type (_, []))) = if v=ThmC.cut_longid s then 1 else 0
91 | deg _ _ v (Var((s, _), Type (_, []))) = if v=ThmC.cut_longid s then 1 else 0
92 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
93 | deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0
94 | deg addl mul v (h $ t1 $ t2) =
95 if subset op = (bin_op h, addl)
96 then max (deg addl mul v t1 , deg addl mul v t2)
97 else (*mul!*)(deg addl mul v t1) + (deg addl mul v t2)
98 | deg _ _ _ t = raise ERROR ("deg: t = " ^ UnparseC.term @{context} t)
100 if polynomial (addl @ [mul]) t bdVar
101 then SOME (deg addl mul (TermC.id_of bdVar) t)
102 else (NONE:int option)
104 fun degree_ addl mul bdVar t = (* do not export *)
108 in opt (degree addl mul bdVar t) end;
110 fun linear addl mul t bdVar = (degree_ addl mul bdVar t) < 2;
112 fun linear_equ addl mul bdVar t =
116 val degl = degree_ addl mul bdVar (equ_lhs t);
117 val degr = degree_ addl mul bdVar (equ_rhs t)
118 in if (degl>0 orelse degr>0)andalso max(degl,degr) < 2 then true else false end
120 (* strip_thy op_ before *)
121 fun is_div_op (dv, (Const (op_,
122 (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) ) = (dv = ThmC.cut_longid op_)
123 | is_div_op _ = false;
125 fun is_denom bdVar div_op t =
127 fun is bool [v] _ (Const (s,Type(_,[])))= bool andalso(if v = ThmC.cut_longid s then true else false)
128 | is bool [v] _ (Free (s,Type(_,[])))= bool andalso(if v = ThmC.cut_longid s then true else false)
129 | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = ThmC.cut_longid s then true else false)
130 | is _ [_] _ ((Const ("Bin.integ_of_bin",_)) $ _) = false
131 | is bool [v] dv (h$n$d) =
133 then (is false [v] dv n) orelse(is true [v] dv d)
134 else (is bool [v] dv n) orelse(is bool [v] dv d)
135 | is _ _ _ _ = raise ERROR "is_denom: uncovered case in fun.def."
136 in is false (varids bdVar) (ThmC.cut_longid div_op) t end;
139 fun rational t div_op bdVar =
140 is_denom bdVar div_op t andalso bin_ops_only t;
144 section \<open>axiomatizations\<close>
145 axiomatization where (*TODO: prove as theorems*)
147 radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
148 rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
149 rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
150 rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
152 "[| l is_num; m is_num |] ==> (l::real)*n + m*n = (l + m) * n" and
154 "m is_num ==> (n::real) + m * n = (1 + m) * n" and
155 rcollect_one_left_assoc:
156 "m is_num ==> (k::real) + n + m * n = k + (1 + m) * n" and
157 rcollect_one_left_assoc_p:
158 "m is_num ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
160 rtwo_of_the_same: "a + a = 2 * a" and
161 rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
162 rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
164 rcancel_den: "a \<noteq> 0 ==> a * (b / a) = b" and
165 rcancel_const: "[| a is_num; b is_num |] ==> a*(x/b) = a/b*x" and
166 rshift_nominator: "(a::real) * b / c = a / c * b" and
168 exp_pow: "(a \<up> b) \<up> c = a \<up> (b * c)" and
169 rsqare: "(a::real) * a = a \<up> 2" and
170 power_1: "(a::real) \<up> 1 = a" and
171 rbinom_power_2: "((a::real) + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and
173 rmult_1: "1 * k = (k::real)" and
174 rmult_1_right: "k * 1 = (k::real)" and
175 rmult_0: "0 * k = (0::real)" and
176 rmult_0_right: "k * 0 = (0::real)" and
177 radd_0: "0 + k = (k::real)" and
178 radd_0_right: "k + 0 = (k::real)" and
181 "[| a is_num; c is_num; d is_num |] ==> a/d + c/d = (a+c)/(d::real)" and
183 "[| a is_num; b is_num; c is_num; d is_num |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
186 radd_commute: "(m::real) + (n::real) = n + m" and
187 radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
188 radd_assoc: "(m::real) + n + k = m + (n + k)" and
189 rmult_commute: "(m::real) * n = n * m" and
190 rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
191 rmult_assoc: "(m::real) * n * k = m * (n * k)" and
193 (*for equations: 'bdv' is a meta-constant*)
194 risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
195 risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
196 risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
199 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
201 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
202 root_ge0: "0 <= a ==> 0 <= sqrt a = True" and
203 (*should be dropped with better simplification in eval_rls ...*)
205 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
207 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
209 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
212 rroot_square_inv: "(sqrt a) \<up> 2 = a" and
213 rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
214 rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
215 rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
218 (*for root-equations*)
219 square_equation_left:
220 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b \<up> 2)))" and
221 square_equation_right:
222 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a \<up> 2)=b))" and
223 (*causes frequently non-termination:*)
225 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a \<up> 2)=b \<up> 2))" and
227 risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
228 risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
229 risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
231 (*for polynomial equations of degree 2; linear case in RatArith*)
232 mult_square: "(a*bdv \<up> 2 = b) = (bdv \<up> 2 = b / a)" and
233 constant_square: "(a + bdv \<up> 2 = b) = (bdv \<up> 2 = b + -1*a)" and
234 constant_mult_square: "(a + b*bdv \<up> 2 = c) = (b*bdv \<up> 2 = c + -1*a)" and
237 "0 <= a ==> (x \<up> 2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
239 "(x \<up> 2 = 0) = (x = 0)" and
241 (*isolate root on the LEFT hand side of the equation
242 otherwise shuffling from left to right would not terminate*)
244 (*Ambiguous input\<^here> produces 2 parse trees -----------------------------\\*)
245 rroot_to_lhs: "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
246 rroot_to_lhs_mult: "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
247 rroot_to_lhs_add_mult: "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
248 (*Ambiguous input\<^here> produces 2 parse trees -----------------------------//*)
250 section \<open>eval functions\<close>
252 (** evaluation of numerals and predicates **)
254 (*does a term contain a root ?*)
255 fun eval_contains_root (thmid:string) _
256 (t as (Const (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) ctxt =
257 if member op = (TermC.ids_of arg) "sqrt"
258 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg)"",
259 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
260 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg)"",
261 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
262 | eval_contains_root _ _ _ _ = NONE;
264 (*dummy precondition for root-met of x+1=2*)
265 fun eval_precond_rootmet (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)) ctxt =
266 SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg)"",
267 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
268 | eval_precond_rootmet _ _ _ _ = NONE;
270 (*dummy precondition for root-pbl of x+1=2*)
271 fun eval_precond_rootpbl (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootpbl\<close>, _) $ arg)) ctxt =
272 SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
273 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
274 | eval_precond_rootpbl _ _ _ _ = NONE;
276 calculation contains_root = \<open>eval_contains_root "#contains_root_"\<close>
277 calculation Test.precond_rootmet = \<open>eval_precond_rootmet "#Test.precond_rootmet_"\<close>
278 calculation Test.precond_rootpbl = \<open>eval_precond_rootpbl "#Test.precond_rootpbl_"\<close>
281 (*8.4.03 aus Poly.ML--------------------------------vvv---
282 make_polynomial ---> make_poly
283 ^-- for user ^-- for systest _ONLY_*)
285 local (*. for make_polytest .*)
287 open Term; (* for type order = EQUAL | LESS | GREATER *)
289 fun pr_ord EQUAL = "EQUAL"
290 | pr_ord LESS = "LESS"
291 | pr_ord GREATER = "GREATER";
293 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
295 \<^const_name>\<open>realpow\<close> => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
296 | _ => (((a, 0), T), 0))
297 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
298 | dest_hd' (Var v) = (v, 2)
299 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
300 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
301 | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
304 fun get_order_pow (t $ (Free(order,_))) =
305 (case TermC.int_opt_of_string order of
308 | get_order_pow _ = 0;
311 fun size_of_term' (Const(str,_) $ t) =
312 if \<^const_name>\<open>realpow\<close>=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 ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
317 (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
319 | term_ord' pr ctxt (t, u) =
321 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
322 val _ = tracing ("t= f@ts= \"" ^ UnparseC.term ctxt f ^ "\" @ \"[" ^
323 commas (map (UnparseC.term ctxt) ts) ^ "]\"")
324 val _ = tracing ("u= g@us= \"" ^ UnparseC.term ctxt g ^"\" @ \"[" ^
325 commas (map (UnparseC.term ctxt) 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 ctxt) (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 ctxt) (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 _ pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us);
347 fun ord_make_polytest (pr:bool) thy (_: subst) (ts, us) =
348 (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
353 section \<open>term order\<close>
355 val term_order = Rewrite_Ord.function_empty;
358 section \<open>rulesets\<close>
361 Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
362 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty,
363 calc = [], errpatts = [],
365 \<^rule_thm>\<open>refl\<close>,
366 \<^rule_thm>\<open>order_refl\<close>,
367 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
368 \<^rule_thm>\<open>not_true\<close>,
369 \<^rule_thm>\<open>not_false\<close>,
370 \<^rule_thm>\<open>and_true\<close>,
371 \<^rule_thm>\<open>and_false\<close>,
372 \<^rule_thm>\<open>or_true\<close>,
373 \<^rule_thm>\<open>or_false\<close>,
374 \<^rule_thm>\<open>and_commute\<close>,
375 \<^rule_thm>\<open>or_commute\<close>,
377 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
378 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
380 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
381 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
382 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
384 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
385 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
387 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
388 program = Rule.Empty_Prog};
391 (*.for evaluation of conditions in rewrite rules.*)
392 (*FIXXXXXXME 10.8.02: handle like _simplify*)
394 Rule_Def.Repeat{id = "tval_rls", preconds = [],
395 rew_ord = ("sqrt_right",sqrt_right false),
396 asm_rls=testerls,prog_rls = Rule_Set.empty,
397 calc=[], errpatts = [],
399 \<^rule_thm>\<open>refl\<close>,
400 \<^rule_thm>\<open>order_refl\<close>,
401 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
402 \<^rule_thm>\<open>not_true\<close>,
403 \<^rule_thm>\<open>not_false\<close>,
404 \<^rule_thm>\<open>and_true\<close>,
405 \<^rule_thm>\<open>and_false\<close>,
406 \<^rule_thm>\<open>or_true\<close>,
407 \<^rule_thm>\<open>or_false\<close>,
408 \<^rule_thm>\<open>and_commute\<close>,
409 \<^rule_thm>\<open>or_commute\<close>,
411 \<^rule_thm>\<open>real_diff_minus\<close>,
413 \<^rule_thm>\<open>root_ge0\<close>,
414 \<^rule_thm>\<open>root_add_ge0\<close>,
415 \<^rule_thm>\<open>root_ge0_1\<close>,
416 \<^rule_thm>\<open>root_ge0_2\<close>,
418 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
419 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),
420 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
421 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
423 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
424 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
425 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
426 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
428 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
429 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
431 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
432 program = Rule.Empty_Prog};
434 rule_set_knowledge testerls = \<open>prep_rls' testerls\<close>
437 (*make () dissappear*)
438 val rearrange_assoc =
440 id = "rearrange_assoc", preconds = [],
441 rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
442 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
444 \<^rule_thm_sym>\<open>add.assoc\<close>,
445 \<^rule_thm_sym>\<open>rmult_assoc\<close>],
446 program = Rule.Empty_Prog};
451 id = "ac_plus_times", preconds = [], rew_ord = ("term_order", term_order),
452 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
454 \<^rule_thm>\<open>radd_commute\<close>,
455 \<^rule_thm>\<open>radd_left_commute\<close>,
456 \<^rule_thm>\<open>add.assoc\<close>,
457 \<^rule_thm>\<open>rmult_commute\<close>,
458 \<^rule_thm>\<open>rmult_left_commute\<close>,
459 \<^rule_thm>\<open>rmult_assoc\<close>],
460 program = Rule.Empty_Prog};
463 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
465 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
466 asm_rls = tval_rls, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
468 \<^rule_thm>\<open>rnorm_equation_add\<close>],
469 program = Rule.Empty_Prog};
471 (* expects * distributed over + *)
474 id = "Test_simplify", preconds = [],
475 rew_ord = ("sqrt_right", sqrt_right false),
476 asm_rls = tval_rls, prog_rls = Rule_Set.empty,
477 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
479 \<^rule_thm>\<open>real_diff_minus\<close>,
480 \<^rule_thm>\<open>radd_mult_distrib2\<close>,
481 \<^rule_thm>\<open>rdistr_right_assoc\<close>,
482 \<^rule_thm>\<open>rdistr_right_assoc_p\<close>,
483 \<^rule_thm>\<open>rdistr_div_right\<close>,
484 \<^rule_thm>\<open>rbinom_power_2\<close>,
486 \<^rule_thm>\<open>radd_commute\<close>,
487 \<^rule_thm>\<open>radd_left_commute\<close>,
488 \<^rule_thm>\<open>add.assoc\<close>,
489 \<^rule_thm>\<open>rmult_commute\<close>,
490 \<^rule_thm>\<open>rmult_left_commute\<close>,
491 \<^rule_thm>\<open>rmult_assoc\<close>,
493 \<^rule_thm>\<open>radd_real_const_eq\<close>,
494 \<^rule_thm>\<open>radd_real_const\<close>,
495 (* these 2 rules are invers to distr_div_right wrt. termination.
496 thus they MUST be done IMMEDIATELY before prog_eval *)
497 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
498 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
499 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
500 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
502 \<^rule_thm>\<open>rcollect_right\<close>,
503 \<^rule_thm>\<open>rcollect_one_left\<close>,
504 \<^rule_thm>\<open>rcollect_one_left_assoc\<close>,
505 \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>,
507 \<^rule_thm>\<open>rshift_nominator\<close>,
508 \<^rule_thm>\<open>rcancel_den\<close>,
509 \<^rule_thm>\<open>rroot_square_inv\<close>,
510 \<^rule_thm>\<open>rroot_times_root\<close>,
511 \<^rule_thm>\<open>rroot_times_root_assoc_p\<close>,
512 \<^rule_thm>\<open>rsqare\<close>,
513 \<^rule_thm>\<open>power_1\<close>,
514 \<^rule_thm>\<open>rtwo_of_the_same\<close>,
515 \<^rule_thm>\<open>rtwo_of_the_same_assoc_p\<close>,
517 \<^rule_thm>\<open>rmult_1\<close>,
518 \<^rule_thm>\<open>rmult_1_right\<close>,
519 \<^rule_thm>\<open>rmult_0\<close>,
520 \<^rule_thm>\<open>rmult_0_right\<close>,
521 \<^rule_thm>\<open>radd_0\<close>,
522 \<^rule_thm>\<open>radd_0_right\<close>],
523 program = Rule.Empty_Prog};
526 (*isolate the root in a root-equation*)
528 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
529 asm_rls=tval_rls,prog_rls = Rule_Set.empty, calc=[], errpatts = [],
531 \<^rule_thm>\<open>rroot_to_lhs\<close>,
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>,
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>,
534 \<^rule_thm>\<open>risolate_root_add\<close>,
535 \<^rule_thm>\<open>risolate_root_mult\<close>,
536 \<^rule_thm>\<open>risolate_root_div\<close>],
537 program = Rule.Empty_Prog};
539 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
542 id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
543 asm_rls=tval_rls,prog_rls = Rule_Set.empty, calc= [], errpatts = [],
545 \<^rule_thm>\<open>risolate_bdv_add\<close>,
546 \<^rule_thm>\<open>risolate_bdv_mult_add\<close>,
547 \<^rule_thm>\<open>risolate_bdv_mult\<close>,
548 \<^rule_thm>\<open>mult_square\<close>,
549 \<^rule_thm>\<open>constant_square\<close>,
550 \<^rule_thm>\<open>constant_mult_square\<close>],
551 program = Rule.Empty_Prog};
553 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
555 Test_simplify = \<open>prep_rls' Test_simplify\<close> and
556 tval_rls = \<open>prep_rls' tval_rls\<close> and
557 isolate_root = \<open>prep_rls' isolate_root\<close> and
558 isolate_bdv = \<open>prep_rls' isolate_bdv\<close> and
559 matches = \<open>prep_rls'
560 (Rule_Set.append_rules "matches" testerls
561 [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "#matches_")])\<close>
564 subsection \<open>problems\<close>
566 problem pbl_test : "test" = \<open>Rule_Set.empty\<close>
568 problem pbl_test_equ : "equation/test" =
569 \<open>get_rls @{context} "matches"\<close>
570 CAS: "solve (e_e::bool, v_v)"
571 Given: "equality e_e" "solveFor v_v"
572 Where: "matches (?a = ?b) e_e"
573 Find: "solutions v_v'i'"
575 problem pbl_test_uni : "univariate/equation/test" =
576 \<open>get_rls @{context} "matches"\<close>
577 CAS: "solve (e_e::bool, v_v)"
578 Given: "equality e_e" "solveFor v_v"
579 Where: "matches (?a = ?b) e_e"
580 Find: "solutions v_v'i'"
582 problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =
583 \<open>get_rls @{context} "matches"\<close>
584 Method_Ref: "Test/solve_linear"
585 CAS: "solve (e_e::bool, v_v)"
586 Given: "equality e_e" "solveFor v_v"
588 "(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |
589 (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)"
590 Find: "solutions v_v'i'"
592 setup \<open>Know_Store.add_rew_ords [
593 ("termlessI", termlessI),
594 ("ord_make_polytest", ord_make_polytest false)]\<close>
598 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
599 rew_ord = ("ord_make_polytest", ord_make_polytest false),
600 asm_rls = testerls, prog_rls = Rule_Set.Empty,
602 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
603 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
604 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
607 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
608 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
609 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
610 \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
611 \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
612 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
613 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
614 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
616 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
617 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
618 \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
619 \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*)
620 \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
621 \<^rule_thm>\<open>add.assoc\<close>, (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
623 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
624 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
625 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
626 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
628 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
629 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
630 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
631 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
633 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
634 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
635 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
636 program = Rule.Empty_Prog};
638 val expand_binomtest =
639 Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
640 rew_ord = ("termlessI",termlessI), asm_rls = testerls, prog_rls = Rule_Set.Empty,
642 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
643 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
644 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))
648 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
649 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
650 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
651 \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)
652 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
653 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
655 \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
656 \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
657 \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
658 \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
659 \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
660 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
661 \<^rule_thm>\<open>real_minus_binom_pow3\<close>, (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
663 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
664 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
665 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
667 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
668 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
669 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
671 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
672 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
673 (*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)
674 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
676 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==> l * n + m * n = (l + m) * n"*)
677 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
678 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
679 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
681 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
682 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
683 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
684 program = Rule.Empty_Prog};
687 make_polytest = \<open>prep_rls' make_polytest\<close> and
688 expand_binomtest = \<open>prep_rls' expand_binomtest\<close>
690 norm_equation = \<open>prep_rls' norm_equation\<close> and
691 ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and
692 rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>
694 section \<open>problems\<close>
696 problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
697 \<open>get_rls @{context} "matches"\<close>
698 Method_Ref: "Test/solve_plain_square"
699 CAS: "solve (e_e::bool, v_v)"
700 Given: "equality e_e" "solveFor v_v"
702 "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |
703 (matches ( ?b*v_v \<up> 2 = 0) e_e) |
704 (matches (?a + v_v \<up> 2 = 0) e_e) |
705 (matches ( v_v \<up> 2 = 0) e_e)"
706 Find: "solutions v_v'i'"
708 problem pbl_test_uni_poly : "polynomial/univariate/equation/test" =
709 \<open>Rule_Set.empty\<close>
710 CAS: "solve (e_e::bool, v_v)"
711 Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
713 Find: "solutions v_v'i'"
715 problem pbl_test_uni_poly_deg2 : "degree_two/polynomial/univariate/equation/test" =
716 \<open>Rule_Set.empty\<close>
717 CAS: "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)"
718 Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
719 Find: "solutions v_v'i'"
721 problem pbl_test_uni_poly_deg2_pq : "pq_formula/degree_two/polynomial/univariate/equation/test" =
722 \<open>Rule_Set.empty\<close>
723 CAS: "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)"
724 Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
725 Find: "solutions v_v'i'"
727 problem pbl_test_uni_poly_deg2_abc : "abc_formula/degree_two/polynomial/univariate/equation/test" =
728 \<open>Rule_Set.empty\<close>
729 CAS: "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)"
730 Given: "equality (a_a * x \<up> 2 + b_b * x + c_c = 0)" "solveFor v_v"
731 Find: "solutions v_v'i'"
733 problem pbl_test_uni_root : "squareroot/univariate/equation/test" =
734 \<open>Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
735 (eval_contains_root "#contains_root_")]\<close>
736 Method_Ref: "Test/square_equation"
737 CAS: "solve (e_e::bool, v_v)"
738 Given: "equality e_e" "solveFor v_v"
739 Where: "precond_rootpbl v_v"
740 Find: "solutions v_v'i'"
742 problem pbl_test_uni_norm : "normalise/univariate/equation/test" =
743 \<open>Rule_Set.empty\<close>
744 Method_Ref: "Test/norm_univar_equation"
745 CAS: "solve (e_e::bool, v_v)"
746 Given: "equality e_e" "solveFor v_v"
748 Find: "solutions v_v'i'"
750 problem pbl_test_uni_roottest : "sqroot-test/univariate/equation/test" =
751 \<open>Rule_Set.empty\<close>
752 CAS: "solve (e_e::bool, v_v)"
753 Given: "equality e_e" "solveFor v_v"
754 Where: "precond_rootpbl v_v"
755 Find: "solutions v_v'i'"
757 problem pbl_test_intsimp : "inttype/test" =
758 \<open>Rule_Set.empty\<close>
759 Method_Ref: "Test/intsimp"
760 Given: "intTestGiven t_t"
762 Find: "intTestFind s_s"
764 section \<open>methods\<close>
765 subsection \<open>differentiate\<close>
766 method "met_test" : "Test" =
767 \<open>{rew_ord="tless_true",rls'=Atools_erls,calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
768 errpats = [], rew_rls = Rule_Set.empty}\<close>
770 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
772 "solve_linear e_e v_v = (
775 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>
776 (Rewrite_Set ''Test_simplify'')) e_e
779 method met_test_solvelin : "Test/solve_linear" =
780 \<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty,
781 where_rls = get_rls @{context} "matches", calc = [],errpats = [],
782 rew_rls = Test_simplify}\<close>
783 Program: solve_linear.simps
784 Given: "equality e_e" "solveFor v_v"
785 Where: "matches (?a = ?b) e_e"
786 Find: "solutions v_v'i'"
788 subsection \<open>root equation\<close>
790 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
792 "solve_root_equ e_e v_v = (
795 (While (contains_root e_e) Do (
796 (Rewrite ''square_equation_left'' ) #>
797 (Try (Rewrite_Set ''Test_simplify'' )) #>
798 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
799 (Try (Rewrite_Set ''isolate_root'' )) #>
800 (Try (Rewrite_Set ''Test_simplify'' )))) #>
801 (Try (Rewrite_Set ''norm_equation'' )) #>
802 (Try (Rewrite_Set ''Test_simplify'' )) #>
803 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>
804 (Try (Rewrite_Set ''Test_simplify'' ))
809 method met_test_sqrt : "Test/sqrt-equ-test" =
810 (*root-equation, version for tests before 8.01.01*)
811 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls,
812 prog_rls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
813 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
814 where_rls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
815 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
816 calc = [], errpats = [], rew_rls = Rule_Set.empty}\<close>
817 Program: solve_root_equ.simps
818 Given: "equality e_e" "solveFor v_v"
819 Where: "contains_root (e_e::bool)"
820 Find: "solutions v_v'i'"
822 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
824 "minisubpbl e_e v_v = (
827 (Try (Rewrite_Set ''norm_equation'' )) #>
828 (Try (Rewrite_Set ''Test_simplify'' ))) e_e;
829 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
830 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
832 Check_elementwise L_L {(v_v::real). Assumptions})"
834 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
835 (*tests subproblem fixed linear*)
836 \<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty,
837 where_rls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
838 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
839 calc=[],errpats = [], rew_rls = Test_simplify}\<close>
840 Program: minisubpbl.simps
841 Given: "equality e_e" "solveFor v_v"
842 Where: "precond_rootmet v_v"
843 Find: "solutions v_v'i'"
845 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
847 "solve_root_equ2 e_e v_v = (
850 (While (contains_root e_e) Do (
851 (Rewrite ''square_equation_left'' ) #>
852 (Try (Rewrite_Set ''Test_simplify'' )) #>
853 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
854 (Try (Rewrite_Set ''isolate_root'' )) #>
855 (Try (Rewrite_Set ''Test_simplify'' )))) #>
856 (Try (Rewrite_Set ''norm_equation'' )) #>
857 (Try (Rewrite_Set ''Test_simplify'' ))
859 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
860 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
862 Check_elementwise L_L {(v_v::real). Assumptions}) "
864 method met_test_eq1 : "Test/square_equation1" =
866 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls,
867 prog_rls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
868 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
869 where_rls=Rule_Set.empty, calc=[],errpats = [], rew_rls = Rule_Set.empty}\<close>
870 Program: solve_root_equ2.simps
871 Given: "equality e_e" "solveFor v_v"
872 Find: "solutions v_v'i'"
874 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
876 "solve_root_equ3 e_e v_v = (
879 (While (contains_root e_e) Do ((
880 (Rewrite ''square_equation_left'' ) Or
881 (Rewrite ''square_equation_right'' )) #>
882 (Try (Rewrite_Set ''Test_simplify'' )) #>
883 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
884 (Try (Rewrite_Set ''isolate_root'' )) #>
885 (Try (Rewrite_Set ''Test_simplify'' )))) #>
886 (Try (Rewrite_Set ''norm_equation'' )) #>
887 (Try (Rewrite_Set ''Test_simplify'' ))
889 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
890 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
892 Check_elementwise L_L {(v_v::real). Assumptions})"
894 method met_test_squ2 : "Test/square_equation2" =
896 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls,
897 prog_rls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
898 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
899 where_rls=Rule_Set.empty,calc=[],errpats = [], rew_rls = Rule_Set.empty}\<close>
900 Program: solve_root_equ3.simps
901 Given: "equality e_e" "solveFor v_v"
902 Find: "solutions v_v'i'"
904 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
906 "solve_root_equ4 e_e v_v = (
909 (While (contains_root e_e) Do ((
910 (Rewrite ''square_equation_left'' ) Or
911 (Rewrite ''square_equation_right'' )) #>
912 (Try (Rewrite_Set ''Test_simplify'' )) #>
913 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
914 (Try (Rewrite_Set ''isolate_root'' )) #>
915 (Try (Rewrite_Set ''Test_simplify'' )))) #>
916 (Try (Rewrite_Set ''norm_equation'' )) #>
917 (Try (Rewrite_Set ''Test_simplify'' ))
919 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
920 [''no_met'']) [BOOL e_e, REAL v_v]
922 Check_elementwise L_L {(v_v::real). Assumptions})"
924 method met_test_squeq : "Test/square_equation" =
926 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls,
927 prog_rls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
928 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
929 where_rls=Rule_Set.empty,calc=[],errpats = [], rew_rls = Rule_Set.empty}\<close>
930 Program: solve_root_equ4.simps
931 Given: "equality e_e" "solveFor v_v"
932 Find: "solutions v_v'i'"
934 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
936 "solve_plain_square e_e v_v = (
939 (Try (Rewrite_Set ''isolate_bdv'' )) #>
940 (Try (Rewrite_Set ''Test_simplify'' )) #>
941 ((Rewrite ''square_equality_0'' ) Or
942 (Rewrite ''square_equality'' )) #>
943 (Try (Rewrite_Set ''tval_rls'' ))) e_e
947 method met_test_eq_plain : "Test/solve_plain_square" =
948 (*solve_plain_square*)
949 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],prog_rls=Rule_Set.empty,
950 where_rls = get_rls @{context} "matches",errpats = [], rew_rls = Rule_Set.empty(*,
951 asm_rls=[],asm_thm=[]*)}\<close>
952 Program: solve_plain_square.simps
953 Given: "equality e_e" "solveFor v_v"
955 "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |
956 (matches ( ?b*v_v \<up> 2 = 0) e_e) |
957 (matches (?a + v_v \<up> 2 = 0) e_e) |
958 (matches ( v_v \<up> 2 = 0) e_e)"
959 Find: "solutions v_v'i'"
962 subsection \<open>polynomial equation\<close>
964 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
966 "norm_univariate_equ e_e v_v = (
969 (Try (Rewrite ''rnorm_equation_add'' )) #>
970 (Try (Rewrite_Set ''Test_simplify'' )) ) e_e
972 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
973 [''no_met'']) [BOOL e_e, REAL v_v])"
975 method met_test_norm_univ : "Test/norm_univar_equation" =
976 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls,prog_rls = Rule_Set.empty,where_rls=Rule_Set.empty, calc=[],
977 errpats = [], rew_rls = Rule_Set.empty}\<close>
978 Program: norm_univariate_equ.simps
979 Given: "equality e_e" "solveFor v_v"
981 Find: "solutions v_v'i'"
984 subsection \<open>diophantine equation\<close>
986 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
988 "test_simplify t_t = (
990 (Try (Calculate ''PLUS'')) #>
991 (Try (Calculate ''TIMES''))) t_t)"
993 method met_test_intsimp : "Test/intsimp" =
994 \<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, calc = [],
995 errpats = [], rew_rls = Test_simplify}\<close>
996 Program: test_simplify.simps
997 Given: "intTestGiven t_t"
999 Find: "intTestFind s_s"