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 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 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 (_,[]))) = [strip_thy s]
64 | varids (Free (s, Type (_,[]))) = [strip_thy s]
65 | varids (Var((s, _),Type (_,[]))) = [strip_thy 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=strip_thy s then 1 else 0
90 | deg _ _ v (Free (s, Type (_, []))) = if v=strip_thy s then 1 else 0
91 | deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy 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 t)
100 if polynomial (addl @ [mul]) t bdVar
101 then SOME (deg addl mul (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 = strip_thy 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 = strip_thy s then true else false)
128 | is bool [v] _ (Free (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
129 | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = strip_thy 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) (strip_thy 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_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
154 "m is_const ==> (n::real) + m * n = (1 + m) * n" and
155 rcollect_one_left_assoc:
156 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
157 rcollect_one_left_assoc_p:
158 "m is_const ==> 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_const; b is_const |] ==> 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_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
183 "[| a is_const; b is_const; c is_const; d is_const |] ==> 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)) thy =
257 if member op = (ids_of arg) "sqrt"
258 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
259 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
260 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy 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)) thy =
266 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy 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)) thy =
272 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy 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>powr\<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>powr\<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 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 _ (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 _ 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) (ts, us) =
349 (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = 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 = [],
366 \<^rule_thm>\<open>refl\<close>,
367 \<^rule_thm>\<open>order_refl\<close>,
368 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
369 \<^rule_thm>\<open>not_true\<close>,
370 \<^rule_thm>\<open>not_false\<close>,
371 \<^rule_thm>\<open>and_true\<close>,
372 \<^rule_thm>\<open>and_false\<close>,
373 \<^rule_thm>\<open>or_true\<close>,
374 \<^rule_thm>\<open>or_false\<close>,
375 \<^rule_thm>\<open>and_commute\<close>,
376 \<^rule_thm>\<open>or_commute\<close>,
378 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
379 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
381 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
382 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
383 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
385 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
386 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
388 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
389 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 = [],
400 \<^rule_thm>\<open>refl\<close>,
401 \<^rule_thm>\<open>order_refl\<close>,
402 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
403 \<^rule_thm>\<open>not_true\<close>,
404 \<^rule_thm>\<open>not_false\<close>,
405 \<^rule_thm>\<open>and_true\<close>,
406 \<^rule_thm>\<open>and_false\<close>,
407 \<^rule_thm>\<open>or_true\<close>,
408 \<^rule_thm>\<open>or_false\<close>,
409 \<^rule_thm>\<open>and_commute\<close>,
410 \<^rule_thm>\<open>or_commute\<close>,
412 \<^rule_thm>\<open>real_diff_minus\<close>,
414 \<^rule_thm>\<open>root_ge0\<close>,
415 \<^rule_thm>\<open>root_add_ge0\<close>,
416 \<^rule_thm>\<open>root_ge0_1\<close>,
417 \<^rule_thm>\<open>root_ge0_2\<close>,
419 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
420 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),
421 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
422 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
424 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
425 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
426 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
427 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
429 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
430 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
432 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
433 scr = Rule.Empty_Prog};
435 rule_set_knowledge testerls = \<open>prep_rls' testerls\<close>
438 (*make () dissappear*)
439 val rearrange_assoc =
441 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>\<open>add.assoc\<close>,
446 \<^rule_thm_sym>\<open>rmult_assoc\<close>],
447 scr = Rule.Empty_Prog};
451 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>\<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 scr = Rule.Empty_Prog};
462 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
464 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
465 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
467 \<^rule_thm>\<open>rnorm_equation_add\<close>],
468 scr = Rule.Empty_Prog};
471 (* expects * distributed over + *)
474 id = "Test_simplify", preconds = [],
475 rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}),
476 erls = tval_rls, srls = 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 calc *)
497 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
498 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
499 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
500 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#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 scr = Rule.Empty_Prog};
526 (*isolate the root in a root-equation*)
528 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
529 erls=tval_rls,srls = 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 scr = Rule.Empty_Prog};
539 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
542 id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
543 erls=tval_rls,srls = 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 scr = 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>assoc_rls' @{theory} "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>assoc_rls' @{theory} "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>assoc_rls' @{theory} "matches"\<close>
584 Method: "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'"
593 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
594 [("termlessI", termlessI),
595 ("ord_make_polytest", ord_make_polytest false \<^theory>)
599 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
600 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
601 erls = testerls, srls = Rule_Set.Empty,
603 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
604 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
605 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
608 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
609 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
610 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
611 \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
612 \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
613 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
614 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
615 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
617 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
618 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
619 \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
620 \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*)
621 \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
622 \<^rule_thm>\<open>add.assoc\<close>, (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
624 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
625 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
626 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
627 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
629 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
630 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
631 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
632 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
634 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
635 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
636 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
637 scr = Rule.Empty_Prog};
639 val expand_binomtest =
640 Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
641 rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,
643 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
644 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
645 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))
649 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
650 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
651 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
652 \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)
653 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
654 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
656 \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
657 \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
658 \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
659 \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
660 \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
661 \<^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 *)
662 \<^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 *)
664 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
665 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
666 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
668 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
669 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
670 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
672 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
673 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
674 (*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)
675 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
677 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
678 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
679 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
680 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
682 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
683 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
684 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
685 scr = Rule.Empty_Prog};
688 make_polytest = \<open>prep_rls' make_polytest\<close> and
689 expand_binomtest = \<open>prep_rls' expand_binomtest\<close>
691 norm_equation = \<open>prep_rls' norm_equation\<close> and
692 ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and
693 rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>
695 section \<open>problems\<close>
697 problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
698 \<open>assoc_rls' @{theory} "matches"\<close>
699 Method: "Test/solve_plain_square"
700 CAS: "solve (e_e::bool, v_v)"
701 Given: "equality e_e" "solveFor v_v"
703 "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |
704 (matches ( ?b*v_v \<up> 2 = 0) e_e) |
705 (matches (?a + v_v \<up> 2 = 0) e_e) |
706 (matches ( v_v \<up> 2 = 0) e_e)"
707 Find: "solutions v_v'i'"
709 problem pbl_test_uni_poly : "polynomial/univariate/equation/test" =
710 \<open>Rule_Set.empty\<close>
711 CAS: "solve (e_e::bool, v_v)"
712 Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
714 Find: "solutions v_v'i'"
716 problem pbl_test_uni_poly_deg2 : "degree_two/polynomial/univariate/equation/test" =
717 \<open>Rule_Set.empty\<close>
718 CAS: "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)"
719 Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
720 Find: "solutions v_v'i'"
722 problem pbl_test_uni_poly_deg2_pq : "pq_formula/degree_two/polynomial/univariate/equation/test" =
723 \<open>Rule_Set.empty\<close>
724 CAS: "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)"
725 Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
726 Find: "solutions v_v'i'"
728 problem pbl_test_uni_poly_deg2_abc : "abc_formula/degree_two/polynomial/univariate/equation/test" =
729 \<open>Rule_Set.empty\<close>
730 CAS: "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)"
731 Given: "equality (a_a * x \<up> 2 + b_b * x + c_c = 0)" "solveFor v_v"
732 Find: "solutions v_v'i'"
734 problem pbl_test_uni_root : "squareroot/univariate/equation/test" =
735 \<open>Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
736 (eval_contains_root "#contains_root_")]\<close>
737 Method: "Test/square_equation"
738 CAS: "solve (e_e::bool, v_v)"
739 Given: "equality e_e" "solveFor v_v"
740 Where: "precond_rootpbl v_v"
741 Find: "solutions v_v'i'"
743 problem pbl_test_uni_norm : "normalise/univariate/equation/test" =
744 \<open>Rule_Set.empty\<close>
745 Method: "Test/norm_univar_equation"
746 CAS: "solve (e_e::bool, v_v)"
747 Given: "equality e_e" "solveFor v_v"
749 Find: "solutions v_v'i'"
751 problem pbl_test_uni_roottest : "sqroot-test/univariate/equation/test" =
752 \<open>Rule_Set.empty\<close>
753 CAS: "solve (e_e::bool, v_v)"
754 Given: "equality e_e" "solveFor v_v"
755 Where: "precond_rootpbl v_v"
756 Find: "solutions v_v'i'"
758 problem pbl_test_intsimp : "inttype/test" =
759 \<open>Rule_Set.empty\<close>
760 Method: "Test/intsimp"
761 Given: "intTestGiven t_t"
763 Find: "intTestFind s_s"
765 section \<open>methods\<close>
766 subsection \<open>differentiate\<close>
767 method "met_test" : "Test" =
768 \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
769 crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
771 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
773 "solve_linear e_e v_v = (
776 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>
777 (Rewrite_Set ''Test_simplify'')) e_e
780 method met_test_solvelin : "Test/solve_linear" =
781 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
782 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
783 nrls = Test_simplify}\<close>
784 Program: solve_linear.simps
785 Given: "equality e_e" "solveFor v_v"
786 Where: "matches (?a = ?b) e_e"
787 Find: "solutions v_v'i'"
789 subsection \<open>root equation\<close>
791 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
793 "solve_root_equ e_e v_v = (
796 (While (contains_root e_e) Do (
797 (Rewrite ''square_equation_left'' ) #>
798 (Try (Rewrite_Set ''Test_simplify'' )) #>
799 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
800 (Try (Rewrite_Set ''isolate_root'' )) #>
801 (Try (Rewrite_Set ''Test_simplify'' )))) #>
802 (Try (Rewrite_Set ''norm_equation'' )) #>
803 (Try (Rewrite_Set ''Test_simplify'' )) #>
804 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>
805 (Try (Rewrite_Set ''Test_simplify'' ))
810 method met_test_sqrt : "Test/sqrt-equ-test" =
811 (*root-equation, version for tests before 8.01.01*)
812 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
813 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
814 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
815 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
816 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
817 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
818 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close>
819 Program: solve_root_equ.simps
820 Given: "equality e_e" "solveFor v_v"
821 Where: "contains_root (e_e::bool)"
822 Find: "solutions v_v'i'"
824 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
826 "minisubpbl e_e v_v = (
829 (Try (Rewrite_Set ''norm_equation'' )) #>
830 (Try (Rewrite_Set ''Test_simplify'' ))) e_e;
831 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
832 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
834 Check_elementwise L_L {(v_v::real). Assumptions})"
836 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
837 (*tests subproblem fixed linear*)
838 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
839 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
840 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
841 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
842 Program: minisubpbl.simps
843 Given: "equality e_e" "solveFor v_v"
844 Where: "precond_rootmet v_v"
845 Find: "solutions v_v'i'"
847 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
849 "solve_root_equ2 e_e v_v = (
852 (While (contains_root e_e) Do (
853 (Rewrite ''square_equation_left'' ) #>
854 (Try (Rewrite_Set ''Test_simplify'' )) #>
855 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
856 (Try (Rewrite_Set ''isolate_root'' )) #>
857 (Try (Rewrite_Set ''Test_simplify'' )))) #>
858 (Try (Rewrite_Set ''norm_equation'' )) #>
859 (Try (Rewrite_Set ''Test_simplify'' ))
861 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
862 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
864 Check_elementwise L_L {(v_v::real). Assumptions}) "
866 method met_test_eq1 : "Test/square_equation1" =
868 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
869 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
870 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
871 prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
872 Program: solve_root_equ2.simps
873 Given: "equality e_e" "solveFor v_v"
874 Find: "solutions v_v'i'"
876 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
878 "solve_root_equ3 e_e v_v = (
881 (While (contains_root e_e) Do ((
882 (Rewrite ''square_equation_left'' ) Or
883 (Rewrite ''square_equation_right'' )) #>
884 (Try (Rewrite_Set ''Test_simplify'' )) #>
885 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
886 (Try (Rewrite_Set ''isolate_root'' )) #>
887 (Try (Rewrite_Set ''Test_simplify'' )))) #>
888 (Try (Rewrite_Set ''norm_equation'' )) #>
889 (Try (Rewrite_Set ''Test_simplify'' ))
891 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
892 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
894 Check_elementwise L_L {(v_v::real). Assumptions})"
896 method met_test_squ2 : "Test/square_equation2" =
898 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
899 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
900 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
901 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
902 Program: solve_root_equ3.simps
903 Given: "equality e_e" "solveFor v_v"
904 Find: "solutions v_v'i'"
906 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
908 "solve_root_equ4 e_e v_v = (
911 (While (contains_root e_e) Do ((
912 (Rewrite ''square_equation_left'' ) Or
913 (Rewrite ''square_equation_right'' )) #>
914 (Try (Rewrite_Set ''Test_simplify'' )) #>
915 (Try (Rewrite_Set ''rearrange_assoc'' )) #>
916 (Try (Rewrite_Set ''isolate_root'' )) #>
917 (Try (Rewrite_Set ''Test_simplify'' )))) #>
918 (Try (Rewrite_Set ''norm_equation'' )) #>
919 (Try (Rewrite_Set ''Test_simplify'' ))
921 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
922 [''no_met'']) [BOOL e_e, REAL v_v]
924 Check_elementwise L_L {(v_v::real). Assumptions})"
926 method met_test_squeq : "Test/square_equation" =
928 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
929 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
930 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
931 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
932 Program: solve_root_equ4.simps
933 Given: "equality e_e" "solveFor v_v"
934 Find: "solutions v_v'i'"
936 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
938 "solve_plain_square e_e v_v = (
941 (Try (Rewrite_Set ''isolate_bdv'' )) #>
942 (Try (Rewrite_Set ''Test_simplify'' )) #>
943 ((Rewrite ''square_equality_0'' ) Or
944 (Rewrite ''square_equality'' )) #>
945 (Try (Rewrite_Set ''tval_rls'' ))) e_e
949 method met_test_eq_plain : "Test/solve_plain_square" =
950 (*solve_plain_square*)
951 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
952 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
953 asm_rls=[],asm_thm=[]*)}\<close>
954 Program: solve_plain_square.simps
955 Given: "equality e_e" "solveFor v_v"
957 "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |
958 (matches ( ?b*v_v \<up> 2 = 0) e_e) |
959 (matches (?a + v_v \<up> 2 = 0) e_e) |
960 (matches ( v_v \<up> 2 = 0) e_e)"
961 Find: "solutions v_v'i'"
964 subsection \<open>polynomial equation\<close>
966 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
968 "norm_univariate_equ e_e v_v = (
971 (Try (Rewrite ''rnorm_equation_add'' )) #>
972 (Try (Rewrite_Set ''Test_simplify'' )) ) e_e
974 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
975 [''no_met'']) [BOOL e_e, REAL v_v])"
977 method met_test_norm_univ : "Test/norm_univar_equation" =
978 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
979 errpats = [], nrls = Rule_Set.empty}\<close>
980 Program: norm_univariate_equ.simps
981 Given: "equality e_e" "solveFor v_v"
983 Find: "solutions v_v'i'"
986 subsection \<open>diophantine equation\<close>
988 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
990 "test_simplify t_t = (
992 (Try (Calculate ''PLUS'')) #>
993 (Try (Calculate ''TIMES''))) t_t)"
995 method met_test_intsimp : "Test/intsimp" =
996 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
997 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
998 Program: test_simplify.simps
999 Given: "intTestGiven t_t"
1001 Find: "intTestFind s_s"