wneuper@59430: (* Knowledge for tests, specifically simplified or bound to a fixed state
wneuper@59430:    for the purpose of simplifying tests.
neuper@37954:    Author: Walther Neuper 2003
neuper@37954:    (c) due to copyright terms
wneuper@59432: 
wneuper@59432: Notes on cleanup:
wneuper@59432: (0) revert import Test -- DiophantEq, this raises issues related to (1..4)
wneuper@59432: (1) transfer methods to respective theories, if only test, then hierarchy at ["...", "Test"]:
wneuper@59432:     differentiate, root equatioh, polynomial equation, diophantine equation
wneuper@59432: (2) transfer problems accordingly
wneuper@59432: (3) rearrange rls according to (1..2)
wneuper@59432: (4) rearrange axiomatizations according to (3)
neuper@37954: *) 
neuper@37906: 
wneuper@59424: theory Test imports Base_Tools Poly Rational Root Diff begin
neuper@37906:  
wneuper@59551: section \<open>consts for problems\<close>
wneuper@59430: consts
walther@60278:   "is_root_free"   :: "'a => bool"      ("is'_root'_free _" 10)
walther@60278:   "contains_root"   :: "'a => bool"      ("contains'_root _" 10)
neuper@42008: 
walther@60278:   "precond_rootmet" :: "'a => bool"      ("precond'_rootmet _" 10)
walther@60278:   "precond_rootpbl" :: "'a => bool"      ("precond'_rootpbl _" 10)
walther@60278:   "precond_submet"  :: "'a => bool"      ("precond'_submet _" 10)
walther@60278:   "precond_subpbl"  :: "'a => bool"      ("precond'_subpbl _" 10)
neuper@37906: 
neuper@37906: 
wneuper@59472: section \<open>functions\<close>
wneuper@59472: ML \<open>
wenzelm@60309: fun bin_o (Const (op_, (Type (\<^type_name>\<open>fun\<close>, [Type (s2, []), Type (\<^type_name>\<open>fun\<close>, [Type (s4, _),Type (s5, _)])]))))
wneuper@59430:       = if s2 = s4 andalso s4 = s5 then [op_] else []
wneuper@59430:     | bin_o _ = [];
neuper@37906: 
wneuper@59430: fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
wneuper@59430:   | bin_op t         =  bin_o t;
wneuper@59430: fun is_bin_op t = (bin_op t <> []);
neuper@37906: 
wneuper@59430: fun bin_op_arg1 ((Const (_,
wenzelm@60309:     (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) $ arg1 $ _) = arg1
walther@59868:   | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);
wneuper@59430: fun bin_op_arg2 ((Const (_,
wenzelm@60309:     (Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])]))))$ _ $ arg2) = arg2
walther@59868:   | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);
neuper@37906: 
wneuper@59430: exception NO_EQUATION_TERM;
wenzelm@60309: fun is_equation ((Const (\<^const_name>\<open>HOL.eq\<close>,
wenzelm@60310:     (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ _) = true
wneuper@59430:   | is_equation _ = false;
wenzelm@60309: fun equ_lhs ((Const (\<^const_name>\<open>HOL.eq\<close>,
wenzelm@60310:     (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ l $ _) = l
wneuper@59430:   | equ_lhs _ = raise NO_EQUATION_TERM;
wenzelm@60309: fun equ_rhs ((Const (\<^const_name>\<open>HOL.eq\<close>, (Type (\<^type_name>\<open>fun\<close>,
wenzelm@60310: 		 [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ r) = r
wneuper@59430:   | equ_rhs _ = raise NO_EQUATION_TERM;
neuper@37906: 
wneuper@59430: fun atom (Const (_, Type (_,[]))) = true
wneuper@59430:   | atom (Free (_, Type (_,[]))) = true
wneuper@59430:   | atom (Var (_, Type (_,[]))) = true
walther@60335:   | atom((Const ("Bin.integ_of_bin", _)) $ _) = true
wneuper@59430:   | atom _ = false;
wneuper@59430: 
walther@60335: fun varids (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = []
walther@60317:   | varids (Const (s, Type (_,[]))) = [strip_thy s]
walther@60317:   | varids (Free (s, Type (_,[]))) = [strip_thy s]  
wneuper@59430:   | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
wneuper@59430: (*| varids (_      (s,"?DUMMY"   )) =   ..ML-error *)
wneuper@59430:   | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
wneuper@59430:   | varids (Abs (a, _, t)) = union op = [a] (varids t)
wneuper@59430:   | varids (t1 $ t2) = union op = (varids t1) (varids t2)
wneuper@59430:   | varids _ = [];
wneuper@59430: 
wneuper@59430: fun bin_ops_only ((Const op_) $ t1 $ t2) =
wneuper@59430:     if is_bin_op (Const op_) then bin_ops_only t1 andalso bin_ops_only t2 else false
wneuper@59430:   | bin_ops_only t = if atom t then true else bin_ops_only t;
wneuper@59430: 
wneuper@59430: fun polynomial opl t _(* bdVar TODO *) =
wneuper@59430:     subset op = (bin_op t, opl) andalso (bin_ops_only t);
wneuper@59430: 
wneuper@59430: fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) 
wneuper@59430:     andalso polynomial opl (equ_lhs t) bdVar 
wneuper@59430:     andalso polynomial opl (equ_rhs t) bdVar
wneuper@59430:     andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
wneuper@59430:              subset op = (varids bdVar, varids (equ_lhs t)));
wneuper@59430: 
wneuper@59430: fun max (a,b) = if a < b then b else a;
wneuper@59430: 
wneuper@59430: fun degree addl mul bdVar t =
wneuper@59430: let
wneuper@59430: fun deg _ _ v (Const  (s, Type (_, []))) = if v=strip_thy s then 1 else 0
wneuper@59430:   | deg _ _ v (Free   (s, Type (_, []))) = if v=strip_thy s then 1 else 0
wneuper@59430:   | deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy s then 1 else 0
wneuper@59430: (*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *) 
wneuper@59430:   | deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0 
wneuper@59430:   | deg addl mul v (h $ t1 $ t2) =
wneuper@59430:     if subset op = (bin_op h, addl)
wneuper@59430:     then max (deg addl mul v t1  , deg addl mul v t2)
wneuper@59430:     else (*mul!*)(deg addl mul v t1) + (deg addl mul v t2)
walther@59868:   | deg _ _ _ t = raise ERROR ("deg: t = " ^ UnparseC.term t)
wneuper@59430: in
wneuper@59430:   if polynomial (addl @ [mul]) t bdVar
wneuper@59430:   then SOME (deg addl mul (id_of bdVar) t)
wneuper@59430:   else (NONE:int option)
wneuper@59430: end;
wneuper@59430: fun degree_ addl mul bdVar t = (* do not export *)
wneuper@59430: let
wneuper@59430:   fun opt (SOME i)= i
wneuper@59430: 	  | opt  NONE = 0
wneuper@59430: in opt (degree addl mul bdVar t) end;
wneuper@59430: 
wneuper@59430: fun linear addl mul t bdVar = (degree_ addl mul bdVar t) < 2;
wneuper@59430: 
wneuper@59430: fun linear_equ addl mul bdVar t =
wneuper@59430:   if is_equation t 
wneuper@59430:   then
wneuper@59430:     let
wneuper@59430:       val degl = degree_ addl mul bdVar (equ_lhs t);
wneuper@59430: 	    val degr = degree_ addl mul bdVar (equ_rhs t)
wneuper@59430: 	  in if (degl>0 orelse degr>0)andalso max(degl,degr) < 2 then true else false end
wneuper@59430:   else false;
wneuper@59430: (* strip_thy op_  before *)
wneuper@59430: fun is_div_op (dv, (Const (op_,
wenzelm@60309:     (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) ) = (dv = strip_thy op_)
wneuper@59430:   | is_div_op _ = false;
wneuper@59430: 
wneuper@59430: fun is_denom bdVar div_op t =
walther@60269:   let
walther@60269:     fun is bool [v] _ (Const  (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
walther@60269:   	  | is bool [v] _ (Free   (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false) 
walther@60269:   	  | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
walther@60269:   	  | is _ [_] _ ((Const ("Bin.integ_of_bin",_)) $ _) = false 
walther@60269:   	  | is bool [v] dv (h$n$d) = 
walther@60269: 	      if is_div_op (dv, h) 
walther@60269: 	      then (is false [v] dv n) orelse(is true [v] dv d)
walther@60269: 	      else (is bool [v] dv n) orelse(is bool [v] dv d)
walther@60269:   	  | is _ _ _ _ = raise ERROR "is_denom: uncovered case in fun.def."    
walther@60269:   in is false (varids bdVar) (strip_thy div_op) t end;
wneuper@59430: 
wneuper@59430: 
wneuper@59430: fun rational t div_op bdVar = 
wneuper@59430:     is_denom bdVar div_op t andalso bin_ops_only t;
wneuper@59430: 
wneuper@59472: \<close>
wneuper@59430: 
wneuper@59472: section \<open>axiomatizations\<close>
neuper@52148: axiomatization where (*TODO: prove as theorems*)
neuper@37906: 
neuper@52148:   radd_mult_distrib2:      "(k::real) * (m + n) = k * m + k * n" and
neuper@52148:   rdistr_right_assoc:      "(k::real) + l * n + m * n = k + (l + m) * n" and
neuper@52148:   rdistr_right_assoc_p:    "l * n + (m * n + (k::real)) = (l + m) * n + k" and
neuper@52148:   rdistr_div_right:        "((k::real) + l) / n = k / n + l / n" and
neuper@37983:   rcollect_right:
walther@60385:           "[| l is_num; m is_num |] ==> (l::real)*n + m*n = (l + m) * n" and
neuper@37983:   rcollect_one_left:
walther@60385:           "m is_num ==> (n::real) + m * n = (1 + m) * n" and
neuper@37983:   rcollect_one_left_assoc:
walther@60385:           "m is_num ==> (k::real) + n + m * n = k + (1 + m) * n" and
neuper@37983:   rcollect_one_left_assoc_p:
walther@60385:           "m is_num ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
neuper@37906: 
neuper@52148:   rtwo_of_the_same:        "a + a = 2 * a" and
neuper@52148:   rtwo_of_the_same_assoc:  "(x + a) + a = x + 2 * a" and
neuper@52148:   rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
neuper@37906: 
walther@60276:   rcancel_den:             "a \<noteq> 0 ==> a * (b / a) = b" and
walther@60385:   rcancel_const:           "[| a is_num; b is_num |] ==> a*(x/b) = a/b*x" and
neuper@52148:   rshift_nominator:        "(a::real) * b / c = a / c * b" and
neuper@37906: 
walther@60242:   exp_pow:                 "(a \<up> b) \<up> c = a \<up> (b * c)" and
walther@60242:   rsqare:                  "(a::real) * a = a \<up> 2" and
walther@60242:   power_1:                 "(a::real) \<up> 1 = a" and
walther@60242:   rbinom_power_2:          "((a::real) + b) \<up>  2 = a \<up>  2 + 2*a*b + b \<up>  2" and
neuper@37906: 
neuper@52148:   rmult_1:                 "1 * k = (k::real)" and
neuper@52148:   rmult_1_right:           "k * 1 = (k::real)" and
neuper@52148:   rmult_0:                 "0 * k = (0::real)" and
neuper@52148:   rmult_0_right:           "k * 0 = (0::real)" and
neuper@52148:   radd_0:                  "0 + k = (k::real)" and
neuper@52148:   radd_0_right:            "k + 0 = (k::real)" and
neuper@37906: 
neuper@37983:   radd_real_const_eq:
walther@60385:           "[| a is_num; c is_num; d is_num |] ==> a/d + c/d = (a+c)/(d::real)" and
neuper@37983:   radd_real_const:
walther@60385:           "[| a is_num; b is_num; c is_num; d is_num |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"  
neuper@52148:    and
neuper@37906: (*for AC-operators*)
neuper@52148:   radd_commute:            "(m::real) + (n::real) = n + m" and
neuper@52148:   radd_left_commute:       "(x::real) + (y + z) = y + (x + z)" and
neuper@52148:   radd_assoc:              "(m::real) + n + k = m + (n + k)" and
neuper@52148:   rmult_commute:           "(m::real) * n = n * m" and
neuper@52148:   rmult_left_commute:      "(x::real) * (y * z) = y * (x * z)" and
neuper@52148:   rmult_assoc:             "(m::real) * n * k = m * (n * k)" and
neuper@37906: 
neuper@37906: (*for equations: 'bdv' is a meta-constant*)
neuper@52148:   risolate_bdv_add:       "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
neuper@52148:   risolate_bdv_mult_add:  "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
neuper@52148:   risolate_bdv_mult:      "((n::real) * bdv = m) = (bdv = m / n)" and
neuper@37906: 
neuper@37983:   rnorm_equation_add:
neuper@52148:       "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
neuper@37906: 
neuper@37906: (*17.9.02 aus SqRoot.thy------------------------------vvv---*) 
walther@60262:   root_ge0:            "0 <= a ==> 0 <= sqrt a = True" and
neuper@37906:   (*should be dropped with better simplification in eval_rls ...*)
neuper@37983:   root_add_ge0:
neuper@52148: 	"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
neuper@37983:   root_ge0_1:
neuper@52148: 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
neuper@37983:   root_ge0_2:
neuper@52148: 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
neuper@37906: 
neuper@37906: 
walther@60242:   rroot_square_inv:         "(sqrt a) \<up>  2 = a" and
neuper@52148:   rroot_times_root:         "sqrt a * sqrt b = sqrt(a*b)" and
neuper@52148:   rroot_times_root_assoc:   "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
neuper@52148:   rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
neuper@37906: 
neuper@37906: 
neuper@37906: (*for root-equations*)
neuper@37983:   square_equation_left:
walther@60242:           "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b \<up>  2)))" and
neuper@37983:   square_equation_right:
walther@60242:           "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a \<up>  2)=b))" and
neuper@37906:   (*causes frequently non-termination:*)
neuper@37983:   square_equation:  
walther@60242:           "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a \<up>  2)=b \<up>  2))" and
neuper@37906:   
neuper@52148:   risolate_root_add:        "(a+  sqrt c = d) = (  sqrt c = d + (-1)*a)" and
neuper@52148:   risolate_root_mult:       "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
neuper@52148:   risolate_root_div:        "(a * sqrt c = d) = (  sqrt c = d / a)" and
neuper@37906: 
neuper@37906: (*for polynomial equations of degree 2; linear case in RatArith*)
walther@60242:   mult_square:		"(a*bdv \<up> 2 = b) = (bdv \<up> 2 = b / a)" and
walther@60242:   constant_square:       "(a + bdv \<up> 2 = b) = (bdv \<up> 2 = b + -1*a)" and
walther@60242:   constant_mult_square:  "(a + b*bdv \<up> 2 = c) = (b*bdv \<up> 2 = c + -1*a)" and
neuper@37906: 
neuper@37983:   square_equality: 
walther@60242: 	     "0 <= a ==> (x \<up> 2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
neuper@37983:   square_equality_0:
walther@60242: 	     "(x \<up> 2 = 0) = (x = 0)" and
neuper@37906: 
neuper@37906: (*isolate root on the LEFT hand side of the equation
neuper@37906:   otherwise shuffling from left to right would not terminate*)  
neuper@37906: 
walther@60269: (*Ambiguous input\<^here> produces 2 parse trees -----------------------------\\*)
walther@60269:   rroot_to_lhs: "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
walther@60269:   rroot_to_lhs_mult: "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
walther@60269:   rroot_to_lhs_add_mult: "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
walther@60269: (*Ambiguous input\<^here> produces 2 parse trees -----------------------------//*)
neuper@37906: 
wneuper@59472: section \<open>eval functions\<close>
wneuper@59472: ML \<open>
neuper@37954: (** evaluation of numerals and predicates **)
neuper@37954: 
neuper@37954: (*does a term contain a root ?*)
neuper@37954: fun eval_contains_root (thmid:string) _ 
Walther@60504: 		       (t as (Const (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) ctxt = 
neuper@38053:   if member op = (ids_of arg) "sqrt"
Walther@60504:   then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
Walther@60504:   else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@38053: | eval_contains_root _ _ _ _ = NONE; 
neuper@42008: 
neuper@42008: (*dummy precondition for root-met of x+1=2*)
Walther@60504: fun eval_precond_rootmet (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)) ctxt = 
Walther@60504:     SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",
wneuper@59390:       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
neuper@52070:   | eval_precond_rootmet _ _ _ _ = NONE; 
neuper@42008: 
neuper@42008: (*dummy precondition for root-pbl of x+1=2*)
Walther@60504: fun eval_precond_rootpbl (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootpbl\<close>, _) $ arg)) ctxt = 
Walther@60504:     SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
wneuper@59390: 	    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
s1210629013@52159: 	| eval_precond_rootpbl _ _ _ _ = NONE;
wneuper@59472: \<close>
wenzelm@60313: calculation contains_root = \<open>eval_contains_root "#contains_root_"\<close>
wenzelm@60313: calculation Test.precond_rootmet = \<open>eval_precond_rootmet "#Test.precond_rootmet_"\<close>
wenzelm@60313: calculation Test.precond_rootpbl = \<open>eval_precond_rootpbl "#Test.precond_rootpbl_"\<close>
wenzelm@60313: 
wneuper@59472: ML \<open>
wneuper@59430: (*8.4.03  aus Poly.ML--------------------------------vvv---
wneuper@59430:   make_polynomial  ---> make_poly
wneuper@59430:   ^-- for user          ^-- for systest _ONLY_*)  
wneuper@59430: 
wneuper@59430: local (*. for make_polytest .*)
wneuper@59430: 
wneuper@59430: open Term;  (* for type order = EQUAL | LESS | GREATER *)
wneuper@59430: 
wneuper@59430: fun pr_ord EQUAL = "EQUAL"
wneuper@59430:   | pr_ord LESS  = "LESS"
wneuper@59430:   | pr_ord GREATER = "GREATER";
wneuper@59430: 
wneuper@59430: fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)
walther@60269:     (case a of
wenzelm@60405:       \<^const_name>\<open>realpow\<close> => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)
walther@60269:   | _ => (((a, 0), T), 0))
walther@60317:   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
wneuper@59430:   | dest_hd' (Var v) = (v, 2)
wneuper@59430:   | dest_hd' (Bound i) = ((("", i), dummyT), 3)
walther@60269:   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
walther@60269:   | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
walther@60269: 
walther@60269: \<^isac_test>\<open>
walther@60269: fun get_order_pow (t $ (Free(order,_))) =
walther@59875:     	(case TermC.int_opt_of_string order of
wneuper@59430: 	             SOME d => d
wneuper@59430: 		   | NONE   => 0)
wneuper@59430:   | get_order_pow _ = 0;
walther@60269: \<close>
wneuper@59430: 
wneuper@59430: fun size_of_term' (Const(str,_) $ t) =
wenzelm@60405:   if \<^const_name>\<open>realpow\<close>=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
wneuper@59430:   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
wneuper@59430:   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
wneuper@59430:   | size_of_term' _ = 1;
wneuper@59430: fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
wneuper@59430:     (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) 
wneuper@59430:                                    | ord => ord)
walther@60269:   | term_ord' pr _ (t, u) =
wneuper@59430:     (if pr then 
wneuper@59430: 	 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
walther@59868: 	     val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
walther@59868: 	                      commas(map UnparseC.term ts) ^ "]\"")
walther@59868: 	     val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
walther@59868: 	                      commas(map UnparseC.term us) ^"]\"")
wneuper@59430: 	     val _ = tracing ("size_of_term(t,u)= (" ^
wneuper@59430: 	                      string_of_int (size_of_term' t) ^ ", " ^
wneuper@59430: 	                      string_of_int (size_of_term' u) ^ ")")
wneuper@59430: 	     val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o hd_ord) (f,g))
wneuper@59430: 	     val _ = tracing ("terms_ord(ts,us) = " ^
wneuper@59430: 			      (pr_ord o terms_ord str false) (ts,us));
wneuper@59430: 	     val _ = tracing "-------"
wneuper@59430: 	 in () end
wneuper@59430:        else ();
wneuper@59430: 	 case int_ord (size_of_term' t, size_of_term' u) of
wneuper@59430: 	   EQUAL =>
wneuper@59430: 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
wneuper@59430: 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 
wneuper@59430: 	     | ord => ord)
wneuper@59430: 	     end
wneuper@59430: 	 | ord => ord)
wneuper@59430: and hd_ord (f, g) =                                        (* ~ term.ML *)
wneuper@59430:   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
walther@60269: and terms_ord _ pr (ts, us) = 
walther@59881:     list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
wneuper@59430: in
wneuper@59430: 
walther@60324: fun ord_make_polytest (pr:bool) thy (_: subst) (ts, us) = 
walther@60324:     (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
wneuper@59430: 
wneuper@59430: end;(*local*)
wneuper@59472: \<close> 
wneuper@59430: 
wneuper@59472: section \<open>term order\<close>
wneuper@59472: ML \<open>
walther@59910: fun term_order (_: subst) tu = (term_ordI [] tu = LESS);
wneuper@59472: \<close>
s1210629013@52145: 
wneuper@59472: section \<open>rulesets\<close>
wneuper@59472: ML \<open>
neuper@37954: val testerls = 
walther@59851:   Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 
walther@60358:     erls = Rule_Set.empty, srls = Rule_Set.Empty, 
walther@60358:     calc = [], errpatts = [], 
walther@60358:     rules = [
walther@60358:        \<^rule_thm>\<open>refl\<close>,
walther@60358: 	     \<^rule_thm>\<open>order_refl\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_left_cancel_le\<close>,
walther@60358: 	     \<^rule_thm>\<open>not_true\<close>,
walther@60358: 	     \<^rule_thm>\<open>not_false\<close>,
walther@60358: 	     \<^rule_thm>\<open>and_true\<close>,
walther@60358: 	     \<^rule_thm>\<open>and_false\<close>,
walther@60358: 	     \<^rule_thm>\<open>or_true\<close>,
walther@60358: 	     \<^rule_thm>\<open>or_false\<close>,
walther@60358: 	     \<^rule_thm>\<open>and_commute\<close>,
walther@60358: 	     \<^rule_thm>\<open>or_commute\<close>,
walther@60358:     
walther@60385: 	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
walther@60358: 	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358: 	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
wenzelm@60405: 	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358: 	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
walther@60358:     scr = Rule.Empty_Prog};      
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37954: (*.for evaluation of conditions in rewrite rules.*)
neuper@37954: (*FIXXXXXXME 10.8.02: handle like _simplify*)
neuper@37954: val tval_rls =  
walther@59851:   Rule_Def.Repeat{id = "tval_rls", preconds = [], 
walther@60358:     rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), 
walther@60358:     erls=testerls,srls = Rule_Set.empty, 
walther@60358:     calc=[], errpatts = [],
walther@60358:     rules = [
walther@60358:        \<^rule_thm>\<open>refl\<close>,
walther@60358: 	     \<^rule_thm>\<open>order_refl\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_left_cancel_le\<close>,
walther@60358: 	     \<^rule_thm>\<open>not_true\<close>,
walther@60358: 	     \<^rule_thm>\<open>not_false\<close>,
walther@60358: 	     \<^rule_thm>\<open>and_true\<close>,
walther@60358: 	     \<^rule_thm>\<open>and_false\<close>,
walther@60358: 	     \<^rule_thm>\<open>or_true\<close>,
walther@60358: 	     \<^rule_thm>\<open>or_false\<close>,
walther@60358: 	     \<^rule_thm>\<open>and_commute\<close>,
walther@60358: 	     \<^rule_thm>\<open>or_commute\<close>,
walther@60358:     
walther@60358: 	     \<^rule_thm>\<open>real_diff_minus\<close>,
walther@60358:     
walther@60358: 	     \<^rule_thm>\<open>root_ge0\<close>,
walther@60358: 	     \<^rule_thm>\<open>root_add_ge0\<close>,
walther@60358: 	     \<^rule_thm>\<open>root_ge0_1\<close>,
walther@60358: 	     \<^rule_thm>\<open>root_ge0_2\<close>,
walther@60358:     
walther@60385: 	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
walther@60358: 	     \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),
walther@60358: 	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
walther@60358: 	     \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358: 	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
walther@60358: 	     \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
wenzelm@60405: 	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358: 	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
walther@60358:     scr = Rule.Empty_Prog};      
wneuper@59472: \<close>
wenzelm@60289: rule_set_knowledge testerls = \<open>prep_rls' testerls\<close>
neuper@52155: 
wneuper@59472: ML \<open>
neuper@37954: (*make () dissappear*)   
neuper@37954: val rearrange_assoc =
walther@60358:   Rule_Def.Repeat{
walther@60358:     id = "rearrange_assoc", preconds = [], 
Walther@60509:     rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 
walther@60358:     erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       \<^rule_thm_sym>\<open>add.assoc\<close>,
walther@60358:       \<^rule_thm_sym>\<open>rmult_assoc\<close>],
walther@60358:     scr = Rule.Empty_Prog};      
neuper@37954: 
neuper@37954: val ac_plus_times =
walther@60358:   Rule_Def.Repeat{
walther@60358:     id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
walther@60358:     erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       \<^rule_thm>\<open>radd_commute\<close>,
walther@60358:       \<^rule_thm>\<open>radd_left_commute\<close>,
walther@60358:       \<^rule_thm>\<open>add.assoc\<close>,
walther@60358:       \<^rule_thm>\<open>rmult_commute\<close>,
walther@60358:       \<^rule_thm>\<open>rmult_left_commute\<close>,
walther@60358:       \<^rule_thm>\<open>rmult_assoc\<close>],
walther@60358:     scr = Rule.Empty_Prog};      
neuper@37954: 
walther@60337: (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
neuper@37954: val norm_equation =
Walther@60509:   Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
walther@60358:     erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       \<^rule_thm>\<open>rnorm_equation_add\<close>],
walther@60358:     scr = Rule.Empty_Prog};      
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37954: (* expects * distributed over + *)
neuper@37954: val Test_simplify =
walther@60358:   Rule_Def.Repeat{
walther@60358:     id = "Test_simplify", preconds = [], 
walther@60358:     rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}),
walther@60358:     erls = tval_rls, srls = Rule_Set.empty, 
walther@60358:     calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
walther@60358:     rules = [
walther@60358: 	     \<^rule_thm>\<open>real_diff_minus\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_mult_distrib2\<close>,
walther@60358: 	     \<^rule_thm>\<open>rdistr_right_assoc\<close>,
walther@60358: 	     \<^rule_thm>\<open>rdistr_right_assoc_p\<close>,
walther@60358: 	     \<^rule_thm>\<open>rdistr_div_right\<close>,
walther@60358: 	     \<^rule_thm>\<open>rbinom_power_2\<close>,	       
neuper@37954: 
walther@60358:              \<^rule_thm>\<open>radd_commute\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_left_commute\<close>,
walther@60358: 	     \<^rule_thm>\<open>add.assoc\<close>,
walther@60358: 	     \<^rule_thm>\<open>rmult_commute\<close>,
walther@60358: 	     \<^rule_thm>\<open>rmult_left_commute\<close>,
walther@60358: 	     \<^rule_thm>\<open>rmult_assoc\<close>,
neuper@37954: 
walther@60358: 	     \<^rule_thm>\<open>radd_real_const_eq\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_real_const\<close>,
walther@60358: 	     (* these 2 rules are invers to distr_div_right wrt. termination.
walther@60358: 		     thus they MUST be done IMMEDIATELY before calc *)
walther@60358: 	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
walther@60358: 	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
walther@60358: 	     \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
wenzelm@60405: 	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
neuper@37954: 
walther@60358: 	     \<^rule_thm>\<open>rcollect_right\<close>,
walther@60358: 	     \<^rule_thm>\<open>rcollect_one_left\<close>,
walther@60358: 	     \<^rule_thm>\<open>rcollect_one_left_assoc\<close>,
walther@60358: 	     \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>,
neuper@37954: 
walther@60358: 	     \<^rule_thm>\<open>rshift_nominator\<close>,
walther@60358: 	     \<^rule_thm>\<open>rcancel_den\<close>,
walther@60358: 	     \<^rule_thm>\<open>rroot_square_inv\<close>,
walther@60358: 	     \<^rule_thm>\<open>rroot_times_root\<close>,
walther@60358: 	     \<^rule_thm>\<open>rroot_times_root_assoc_p\<close>,
walther@60358: 	     \<^rule_thm>\<open>rsqare\<close>,
walther@60358: 	     \<^rule_thm>\<open>power_1\<close>,
walther@60358: 	     \<^rule_thm>\<open>rtwo_of_the_same\<close>,
walther@60358: 	     \<^rule_thm>\<open>rtwo_of_the_same_assoc_p\<close>,
neuper@37954: 
walther@60358: 	     \<^rule_thm>\<open>rmult_1\<close>,
walther@60358: 	     \<^rule_thm>\<open>rmult_1_right\<close>,
walther@60358: 	     \<^rule_thm>\<open>rmult_0\<close>,
walther@60358: 	     \<^rule_thm>\<open>rmult_0_right\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_0\<close>,
walther@60358: 	     \<^rule_thm>\<open>radd_0_right\<close>],
walther@60358:     scr = Rule.Empty_Prog};      
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37954: (*isolate the root in a root-equation*)
neuper@37954: val isolate_root =
Walther@60509:   Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 
walther@60358:     erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
walther@60358:     rules = [
walther@60358:        \<^rule_thm>\<open>rroot_to_lhs\<close>,
walther@60358: 	     \<^rule_thm>\<open>rroot_to_lhs_mult\<close>,
walther@60358: 	     \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>,
walther@60358: 	     \<^rule_thm>\<open>risolate_root_add\<close>,
walther@60358: 	     \<^rule_thm>\<open>risolate_root_mult\<close>,
walther@60358: 	     \<^rule_thm>\<open>risolate_root_div\<close>],
walther@60358:     scr = Rule.Empty_Prog};      
neuper@37954: 
neuper@37954: (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
neuper@37954: val isolate_bdv =
walther@60358:   Rule_Def.Repeat{
Walther@60509:     id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
walther@60358:   	erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
walther@60358:   	rules = [
walther@60358:       \<^rule_thm>\<open>risolate_bdv_add\<close>,
walther@60358:       \<^rule_thm>\<open>risolate_bdv_mult_add\<close>,
walther@60358:       \<^rule_thm>\<open>risolate_bdv_mult\<close>,
walther@60358:       \<^rule_thm>\<open>mult_square\<close>,
walther@60358:       \<^rule_thm>\<open>constant_square\<close>,
walther@60358:       \<^rule_thm>\<open>constant_mult_square\<close>],
walther@60358:     scr = Rule.Empty_Prog};      
wneuper@59472: \<close>
walther@59618: ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
wenzelm@60289: rule_set_knowledge
wenzelm@60286:   Test_simplify = \<open>prep_rls' Test_simplify\<close> and
wenzelm@60286:   tval_rls = \<open>prep_rls' tval_rls\<close> and
wenzelm@60286:   isolate_root = \<open>prep_rls' isolate_root\<close> and
wenzelm@60286:   isolate_bdv = \<open>prep_rls' isolate_bdv\<close> and
wenzelm@60286:   matches = \<open>prep_rls'
wenzelm@60286:     (Rule_Set.append_rules "matches" testerls
wenzelm@60294:       [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "#matches_")])\<close>
wenzelm@60286: 
neuper@37954: 
wneuper@59472: subsection \<open>problems\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_test : "test" = \<open>Rule_Set.empty\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_test_equ : "equation/test" =
wenzelm@60306:   \<open>assoc_rls' @{theory} "matches"\<close>
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where: "matches (?a = ?b) e_e"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni : "univariate/equation/test" =
wenzelm@60306:   \<open>assoc_rls' @{theory} "matches"\<close>
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where: "matches (?a = ?b) e_e"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =
wenzelm@60306:   \<open>assoc_rls' @{theory} "matches"\<close>
Walther@60449:   Method_Ref: "Test/solve_linear"
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where:
wenzelm@60306:     "(matches (   v_v = 0) e_e) | (matches (   ?b*v_v = 0) e_e) |
wenzelm@60306:      (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
Walther@60506: setup \<open>KEStore_Elems.add_rew_ord [
Walther@60506:   ("termlessI", termlessI),
Walther@60506:   ("ord_make_polytest", ord_make_polytest false \<^theory>)]\<close>
Walther@60506: 
wneuper@59472: ML \<open>
neuper@37954: val make_polytest =
walther@59851:   Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, 
walther@60358:     rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
walther@60358:     erls = testerls, srls = Rule_Set.Empty,
walther@60358:     calc = [
walther@60358:       ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
walther@60358: 	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
wenzelm@60405: 	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
walther@60358:     errpatts = [],
walther@60358:     rules = [
walther@60358:        \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
walther@60358: 	     \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
walther@60358: 	     \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
walther@60358: 	     \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
walther@60358: 	     \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
walther@60358: 	     \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
walther@60358: 	     \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
walther@60358: 	     \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
walther@60358: 	     (*AC-rewriting*)
walther@60358: 	     \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
walther@60358: 	     \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
walther@60358: 	     \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
walther@60358: 	     \<^rule_thm>\<open>add.commute\<close>,	 (*z + w = w + z*)
walther@60358: 	     \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
walther@60358: 	     \<^rule_thm>\<open>add.assoc\<close>, (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
walther@60358:     
walther@60358: 	     \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
walther@60358: 	     \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
walther@60358: 	     \<^rule_thm_sym>\<open>real_mult_2\<close>,	 (*"z1 + z1 = 2 * z1"*)
walther@60358: 	     \<^rule_thm>\<open>real_mult_2_assoc\<close>,	 (*"z1 + (z1 + k) = 2 * z1 + k"*)
walther@60358:     
walther@60385: 	     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
walther@60385: 	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
walther@60385: 	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
walther@60385: 	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
walther@60358:     
walther@60358: 	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
walther@60358: 	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
wenzelm@60405: 	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
walther@60358:     scr = Rule.Empty_Prog}; 
neuper@37954: 
neuper@37954: val expand_binomtest =
walther@59851:   Rule_Def.Repeat{id = "expand_binomtest", preconds = [], 
walther@60358:     rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,
walther@60358:     calc = [
walther@60358:       ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
walther@60358: 	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
wenzelm@60405: 	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))
walther@60358: 	    ],
walther@60358:     errpatts = [],
walther@60358:     rules = [
walther@60358:       \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
walther@60358:       \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
walther@60358:       \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
walther@60358:       \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)
walther@60358:       \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
walther@60358:       \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
walther@60358:       (*RL 020915*)
walther@60358:       \<^rule_thm>\<open>real_pp_binom_times\<close>,  (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
walther@60358:       \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
walther@60358:       \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
walther@60358:       \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
walther@60358:       \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
walther@60358:       \<^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 *)
walther@60358:       \<^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 *)
neuper@37954: 
walther@60358:     	\<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
walther@60358:     	\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
walther@60358:     	\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
walther@60358:     
walther@60358:     	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
walther@60358:     	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
wenzelm@60405:     	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
walther@60358:     
walther@60358:     	\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
walther@60358:     	\<^rule_thm>\<open>realpow_plus_1\<close>,	 (*"r * r \<up> n = r \<up> (n + 1)"*)
walther@60358:     	(*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)
walther@60358:     	\<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
walther@60358:     
walther@60385:     	\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==> l * n + m * n = (l + m) * n"*)
walther@60385:     	\<^rule_thm>\<open>real_num_collect_assoc\<close>,	 (*"[| l is_num; m is_num |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
walther@60385:     	\<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)
walther@60385:     	\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
walther@60358:     
walther@60358:     	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
walther@60358:     	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
wenzelm@60405:     	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
walther@60358:     scr = Rule.Empty_Prog};      
wneuper@59472: \<close>
wenzelm@60289: rule_set_knowledge
wenzelm@60286:   make_polytest = \<open>prep_rls' make_polytest\<close> and
wenzelm@60286:   expand_binomtest = \<open>prep_rls' expand_binomtest\<close>
wenzelm@60289: rule_set_knowledge
wenzelm@60286:   norm_equation = \<open>prep_rls' norm_equation\<close> and
wenzelm@60286:   ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and
wenzelm@60286:   rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>
wneuper@59430: 
wneuper@59472: section \<open>problems\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
wenzelm@60306:   \<open>assoc_rls' @{theory} "matches"\<close>
Walther@60449:   Method_Ref: "Test/solve_plain_square"
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where:
wenzelm@60306:     "(matches (?a + ?b*v_v  \<up> 2 = 0) e_e) |
wenzelm@60306:      (matches (     ?b*v_v  \<up> 2 = 0) e_e) |
wenzelm@60306:      (matches (?a +    v_v  \<up> 2 = 0) e_e) |
wenzelm@60306:      (matches (        v_v  \<up> 2 = 0) e_e)"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_poly : "polynomial/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
wenzelm@60306:   Where: "HOL.False"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_poly_deg2 : "degree_two/polynomial/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
wenzelm@60306:   CAS: "solve (v_v  \<up> 2 + p_p * v_v + q__q = 0, v_v)"
wenzelm@60306:   Given: "equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_poly_deg2_pq : "pq_formula/degree_two/polynomial/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
wenzelm@60306:   CAS: "solve (v_v  \<up> 2 + p_p * v_v + q__q = 0, v_v)"
wenzelm@60306:   Given: "equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_poly_deg2_abc : "abc_formula/degree_two/polynomial/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
wenzelm@60306:   CAS: "solve (a_a * x  \<up> 2 + b_b * x + c_c = 0, v_v)"
wenzelm@60306:   Given: "equality (a_a * x  \<up> 2 + b_b * x + c_c = 0)" "solveFor v_v"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_root : "squareroot/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
wenzelm@60306:     (eval_contains_root "#contains_root_")]\<close>
Walther@60449:   Method_Ref: "Test/square_equation"
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where: "precond_rootpbl v_v"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_norm : "normalise/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
Walther@60449:   Method_Ref: "Test/norm_univar_equation"
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where:
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_uni_roottest : "sqroot-test/univariate/equation/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
wenzelm@60306:   CAS: "solve (e_e::bool, v_v)"
wenzelm@60306:   Given: "equality e_e" "solveFor v_v"
wenzelm@60306:   Where: "precond_rootpbl v_v"
wenzelm@60306:   Find: "solutions v_v'i'"
wenzelm@60306: 
wenzelm@60306: problem pbl_test_intsimp : "inttype/test" =
wenzelm@60306:   \<open>Rule_Set.empty\<close>
Walther@60449:   Method_Ref: "Test/intsimp"
wenzelm@60306:   Given: "intTestGiven t_t"
wenzelm@60306:   Where:
wenzelm@60306:   Find: "intTestFind s_s"
wneuper@59430: 
wneuper@59472: section \<open>methods\<close>
wneuper@59472: subsection \<open>differentiate\<close>
walther@60364: method "met_test" : "Test" =
walther@60364:  \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
walther@60364:   crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59504:   where
walther@59635: "solve_linear e_e v_v = (
walther@59635:   let e_e =
walther@59635:     Repeat (
walther@59637:       (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>
walther@59635:       (Rewrite_Set ''Test_simplify'')) e_e
walther@59635:   in
walther@59635:     [e_e])"
wenzelm@60303: method met_test_solvelin : "Test/solve_linear" =
Walther@60509:   \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
wenzelm@60303:     prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
wenzelm@60303:     nrls = Test_simplify}\<close>
wenzelm@60303:   Program: solve_linear.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Where: "matches (?a = ?b) e_e"
wenzelm@60303:   Find: "solutions v_v'i'"
wenzelm@60303: 
wneuper@59472: subsection \<open>root equation\<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59504:   where
walther@59635: "solve_root_equ e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59635:       (While (contains_root e_e) Do (
walther@59637:         (Rewrite ''square_equation_left'' ) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )) #>
walther@59637:         (Try (Rewrite_Set ''rearrange_assoc'' )) #>
walther@59637:         (Try (Rewrite_Set ''isolate_root'' )) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )))) #>
walther@59637:       (Try (Rewrite_Set ''norm_equation'' )) #>
walther@59637:       (Try (Rewrite_Set ''Test_simplify'' )) #>
walther@59637:       (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>
walther@59635:       (Try (Rewrite_Set ''Test_simplify'' ))
walther@59635:       ) e_e                                                                
walther@59635:   in
walther@59635:     [e_e])"
wenzelm@60303: 
wenzelm@60303: method met_test_sqrt : "Test/sqrt-equ-test" =
wenzelm@60303:   (*root-equation, version for tests before 8.01.01*)
Walther@60509:   \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
wenzelm@60303:     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
wenzelm@60303:         [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
wenzelm@60303:     prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty 
wenzelm@60303:         [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
wenzelm@60303:     calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
wenzelm@60303:     asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close>
wenzelm@60303:   Program: solve_root_equ.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Where: "contains_root (e_e::bool)"
wenzelm@60303:   Find: "solutions v_v'i'"
wneuper@59477: 
walther@59635: partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
walther@59635:   where
walther@59635: "minisubpbl e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59637:       (Try (Rewrite_Set ''norm_equation'' )) #>
walther@59635:       (Try (Rewrite_Set ''Test_simplify'' ))) e_e;
walther@59635:     L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
walther@59635:       [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
walther@59635:   in
walther@59635:     Check_elementwise L_L {(v_v::real). Assumptions})"
wenzelm@60303: 
wenzelm@60303: method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
wenzelm@60303:   (*tests subproblem fixed linear*)
Walther@60509:   \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
walther@60358:      prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
walther@60358:        [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
walther@60358:      calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
wenzelm@60303:   Program: minisubpbl.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Where: "precond_rootmet v_v"
wenzelm@60303:   Find: "solutions v_v'i'"
wneuper@59545: 
wneuper@59504: partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
walther@59635:   where
walther@59635: "solve_root_equ2 e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59635:       (While (contains_root e_e) Do (
walther@59637:         (Rewrite ''square_equation_left'' ) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )) #>
walther@59637:         (Try (Rewrite_Set ''rearrange_assoc'' )) #>
walther@59637:         (Try (Rewrite_Set ''isolate_root'' )) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )))) #>
walther@59637:       (Try (Rewrite_Set ''norm_equation'' )) #>
walther@59635:       (Try (Rewrite_Set ''Test_simplify'' ))
walther@59635:       ) e_e;
walther@59635:     L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
wneuper@59504:              [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
walther@59635:   in
walther@59635:     Check_elementwise L_L {(v_v::real). Assumptions})                                       "
wenzelm@60303: 
wenzelm@60303: method met_test_eq1 : "Test/square_equation1" =
wenzelm@60303:   (*root-equation1:*)
Walther@60509:   \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
wenzelm@60303:     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
walther@60358:       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
walther@60358:     prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303:   Program: solve_root_equ2.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Find: "solutions v_v'i'"
wneuper@59545: 
wneuper@59504: partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59504:   where
walther@59635: "solve_root_equ3 e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59635:       (While (contains_root e_e) Do ((
walther@59635:         (Rewrite ''square_equation_left'' ) Or
walther@59637:         (Rewrite ''square_equation_right'' )) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )) #>
walther@59637:         (Try (Rewrite_Set ''rearrange_assoc'' )) #>
walther@59637:         (Try (Rewrite_Set ''isolate_root'' )) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )))) #>
walther@59637:       (Try (Rewrite_Set ''norm_equation'' )) #>
walther@59635:       (Try (Rewrite_Set ''Test_simplify'' ))
walther@59635:       ) e_e;
walther@59635:     L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
walther@59635:       [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
walther@59635:   in
walther@59635:     Check_elementwise L_L {(v_v::real). Assumptions})"
wenzelm@60303: 
wenzelm@60303: method met_test_squ2 : "Test/square_equation2" =
wenzelm@60303:   (*root-equation2*)
Walther@60509:   \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
wenzelm@60303:     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
walther@60358:       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
walther@60358:     prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303:   Program: solve_root_equ3.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Find: "solutions v_v'i'"
wneuper@59545: 
wneuper@59504: partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59504:   where
walther@59635: "solve_root_equ4 e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59635:       (While (contains_root e_e) Do ((
walther@59635:         (Rewrite ''square_equation_left'' ) Or
walther@59637:         (Rewrite ''square_equation_right'' )) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )) #>
walther@59637:         (Try (Rewrite_Set ''rearrange_assoc'' )) #>
walther@59637:         (Try (Rewrite_Set ''isolate_root'' )) #>
walther@59637:         (Try (Rewrite_Set ''Test_simplify'' )))) #>
walther@59637:       (Try (Rewrite_Set ''norm_equation'' )) #>
walther@59635:       (Try (Rewrite_Set ''Test_simplify'' ))
walther@59635:       ) e_e;
walther@59635:     L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
walther@59635:       [''no_met'']) [BOOL e_e, REAL v_v]
walther@59635:   in
walther@59635:     Check_elementwise L_L {(v_v::real). Assumptions})"
wenzelm@60303: 
wenzelm@60303: method met_test_squeq : "Test/square_equation" =
wenzelm@60303:   (*root-equation*)
Walther@60509:   \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
wenzelm@60303:     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
walther@60358:       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
walther@60358:     prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303:   Program: solve_root_equ4.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Find: "solutions v_v'i'"
wneuper@59545: 
wneuper@59504: partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59504:   where
walther@59635: "solve_plain_square e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59637:       (Try (Rewrite_Set ''isolate_bdv'' )) #>
walther@59637:       (Try (Rewrite_Set ''Test_simplify'' )) #>
walther@59635:       ((Rewrite ''square_equality_0'' ) Or
walther@59637:        (Rewrite ''square_equality'' )) #>
walther@59635:       (Try (Rewrite_Set ''tval_rls'' ))) e_e
walther@59635:   in
walther@59635:     Or_to_List e_e)"
wenzelm@60303: 
wenzelm@60303: method met_test_eq_plain : "Test/solve_plain_square" =
wenzelm@60303:   (*solve_plain_square*)
Walther@60509:   \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
wenzelm@60303:     prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
wenzelm@60303:     asm_rls=[],asm_thm=[]*)}\<close>
wenzelm@60303:   Program: solve_plain_square.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Where:
wenzelm@60303:     "(matches (?a + ?b*v_v  \<up> 2 = 0) e_e) |
wenzelm@60303:      (matches (     ?b*v_v  \<up> 2 = 0) e_e) |
wenzelm@60303:      (matches (?a +    v_v  \<up> 2 = 0) e_e) |
wenzelm@60303:      (matches (        v_v  \<up> 2 = 0) e_e)"
wenzelm@60303:   Find: "solutions v_v'i'"
wenzelm@60303: 
wenzelm@60303: 
wneuper@59472: subsection \<open>polynomial equation\<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59504:   where
walther@59635: "norm_univariate_equ e_e v_v = (
walther@59635:   let
walther@59635:     e_e = (
walther@59637:       (Try (Rewrite ''rnorm_equation_add'' )) #>
walther@59635:       (Try (Rewrite_Set ''Test_simplify'' )) ) e_e
walther@59635:   in
walther@59635:     SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
wneuper@59504:         [''no_met'']) [BOOL e_e, REAL v_v])"
wenzelm@60303: 
wenzelm@60303: method met_test_norm_univ : "Test/norm_univar_equation" =
Walther@60509:   \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
wenzelm@60303:     errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303:   Program: norm_univariate_equ.simps
wenzelm@60303:   Given: "equality e_e" "solveFor v_v"
wenzelm@60303:   Where:
wenzelm@60303:   Find: "solutions v_v'i'"
wenzelm@60303: 
wenzelm@60303: 
wneuper@59472: subsection \<open>diophantine equation\<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
wneuper@59504:   where
walther@59635: "test_simplify t_t = (
walther@59635:   Repeat (
walther@59637:     (Try (Calculate ''PLUS'')) #>         
walther@59635:     (Try (Calculate ''TIMES''))) t_t)"
wenzelm@60303: 
wenzelm@60303: method met_test_intsimp : "Test/intsimp" =
Walther@60509:   \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,  prls = Rule_Set.empty, calc = [],
wenzelm@60303:     crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
wenzelm@60303:   Program: test_simplify.simps
wenzelm@60303:   Given: "intTestGiven t_t"
wenzelm@60303:   Where:
wenzelm@60303:   Find: "intTestFind s_s"
wenzelm@60303: 
wenzelm@60303: ML \<open>
wneuper@59472: \<close>
wneuper@59430: 
neuper@37906: end