
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@59472: section \<open>consts\<close>
wneuper@59472: subsection \<open>for scripts\<close>
neuper@37906: consts
neuper@37906:   Solve'_univar'_err
neuper@37954:              :: "[bool,real,bool,  
neuper@37954: 		    bool list] => bool list"
wneuper@59334:                ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9)
neuper@37906:   Solve'_linear
neuper@37954:              :: "[bool,real,  
neuper@37954: 		    bool list] => bool list"
wneuper@59334:                ("((Script Solve'_linear (_ _ =))// (_))" 9)
wneuper@59430:   Solve'_root'_equation 
wneuper@59430:              :: "[bool,real,  
wneuper@59430: 		    bool list] => bool list"
wneuper@59430:                ("((Script Solve'_root'_equation (_ _ =))// (_))" 9)
wneuper@59430:   Solve'_plain'_square 
wneuper@59430:              :: "[bool,real,  
wneuper@59430: 		    bool list] => bool list"
wneuper@59430:                ("((Script Solve'_plain'_square (_ _ =))// (_))" 9)
wneuper@59430:   Norm'_univar'_equation 
wneuper@59430:              :: "[bool,real,  
wneuper@59430: 		    bool] => bool"
wneuper@59430:                ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9)
wneuper@59430:   STest'_simplify
wneuper@59430:              :: "['z,  
wneuper@59430: 		    'z] => 'z"
wneuper@59430:                ("((Script STest'_simplify (_ =))// (_))" 9)
neuper@37906: 
neuper@37906: 
wneuper@59472: subsection \<open>for problems\<close>
wneuper@59430: consts
neuper@42008:   "is'_root'_free"   :: "'a => bool"      ("is'_root'_free _" 10)
neuper@42008:   "contains'_root"   :: "'a => bool"      ("contains'_root _" 10)
neuper@42008: 
neuper@42008:   "precond'_rootmet" :: "'a => bool"      ("precond'_rootmet _" 10)
neuper@42008:   "precond'_rootpbl" :: "'a => bool"      ("precond'_rootpbl _" 10)
neuper@42008:   "precond'_submet"  :: "'a => bool"      ("precond'_submet _" 10)
neuper@42008:   "precond'_subpbl"  :: "'a => bool"      ("precond'_subpbl _" 10)
neuper@37906: 
neuper@37906: 
wneuper@59472: section \<open>functions\<close>
wneuper@59472: ML \<open>
wneuper@59430: fun bin_o (Const (op_, (Type ("fun", [Type (s2, []), Type ("fun", [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 (_,
wneuper@59430:     (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) $ arg1 $ _) = arg1
wneuper@59430:   | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ Rule.term2str t);
wneuper@59430: fun bin_op_arg2 ((Const (_,
wneuper@59430:     (Type ("fun", [Type (_, []),Type ("fun", [Type _, Type _])]))))$ _ $ arg2) = arg2
wneuper@59430:   | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ Rule.term2str t);
neuper@37906: 
wneuper@59430: exception NO_EQUATION_TERM;
wneuper@59430: fun is_equation ((Const ("HOL.eq",
wneuper@59430:     (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ _ $ _) = true
wneuper@59430:   | is_equation _ = false;
wneuper@59430: fun equ_lhs ((Const ("HOL.eq",
wneuper@59430:     (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ l $ _) = l
wneuper@59430:   | equ_lhs _ = raise NO_EQUATION_TERM;
wneuper@59430: fun equ_rhs ((Const ("HOL.eq", (Type ("fun",
wneuper@59430: 		 [Type (_, []), Type ("fun", [Type (_, []), Type ("bool",[])])])))) $ _ $ 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
wneuper@59430:   | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
wneuper@59430:   | atom _ = false;
wneuper@59430: 
wneuper@59430: fun varids (Const (s, Type (_,[]))) = [strip_thy s]
wneuper@59430:   | varids (Free (s, Type (_,[]))) = if TermC.is_num' s then [] else [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)
wneuper@59430:   | deg _ _ _ t = raise ERROR ("deg: t = " ^ Rule.term2str 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_,
wneuper@59430:     (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) ) = (dv = strip_thy op_)
wneuper@59430:   | is_div_op _ = false;
wneuper@59430: 
wneuper@59430: fun is_denom bdVar div_op t =
wneuper@59430:     let fun is bool[v]dv (Const  (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
wneuper@59430: 	  | is bool[v]dv (Free   (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) 
wneuper@59430: 	  | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
wneuper@59430: 	  | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
wneuper@59430: 	  | is bool[v]dv (h$n$d) = 
wneuper@59430: 	      if is_div_op(dv,h) 
wneuper@59430: 	      then (is false[v]dv n)orelse(is true[v]dv d)
wneuper@59430: 	      else (is bool [v]dv n)orelse(is bool[v]dv d)
wneuper@59430: 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:
neuper@52148:           "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
neuper@37983:   rcollect_one_left:
neuper@52148:           "m is_const ==> (n::real) + m * n = (1 + m) * n" and
neuper@37983:   rcollect_one_left_assoc:
neuper@52148:           "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
neuper@37983:   rcollect_one_left_assoc_p:
neuper@52148:           "m is_const ==> 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: 
neuper@52148:   rcancel_den:             "not(a=0) ==> a * (b / a) = b" and
neuper@52148:   rcancel_const:           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
neuper@52148:   rshift_nominator:        "(a::real) * b / c = a / c * b" and
neuper@37906: 
neuper@52148:   exp_pow:                 "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
neuper@52148:   rsqare:                  "(a::real) * a = a ^^^ 2" and
neuper@52148:   power_1:                 "(a::real) ^^^ 1 = a" and
neuper@52148:   rbinom_power_2:          "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 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:
neuper@52148:           "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
neuper@37983:   radd_real_const:
neuper@37906:           "[| a is_const; b is_const; c is_const; d is_const |] ==> 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---*) 
neuper@52148:   root_ge0:            "0 <= a ==> 0 <= sqrt a" 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: 
neuper@52148:   rroot_square_inv:         "(sqrt a)^^^ 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:
neuper@52148:           "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and
neuper@37983:   square_equation_right:
neuper@52148:           "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and
neuper@37906:   (*causes frequently non-termination:*)
neuper@37983:   square_equation:  
neuper@52148:           "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 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*)
neuper@52148:   mult_square:		"(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and
neuper@52148:   constant_square:       "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and
neuper@52148:   constant_mult_square:  "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and
neuper@37906: 
neuper@37983:   square_equality: 
neuper@52148: 	     "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
neuper@37983:   square_equality_0:
neuper@52148: 	     "(x^^^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: 
neuper@37983:   rroot_to_lhs:
neuper@52148:           "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
neuper@37983:   rroot_to_lhs_mult:
neuper@52148:           "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
neuper@37983:   rroot_to_lhs_add_mult:
neuper@37906:           "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
neuper@37906: (*17.9.02 aus SqRoot.thy------------------------------^^^---*)  
neuper@37906: 
wneuper@59472: section \<open>eval functions\<close>
wneuper@59472: ML \<open>
neuper@37972: val thy = @{theory};
neuper@37972: 
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) _ 
neuper@37954: 		       (t as (Const("Test.contains'_root",t0) $ arg)) thy = 
neuper@38053:   if member op = (ids_of arg) "sqrt"
wneuper@59416:   then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
wneuper@59416:   else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy 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*)
neuper@42008: fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy = 
wneuper@59416:     SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy 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*)
neuper@42008: fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy = 
wneuper@59416:     SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
wneuper@59390: 	    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
s1210629013@52159: 	| eval_precond_rootpbl _ _ _ _ = NONE;
wneuper@59472: \<close>
wneuper@59472: setup \<open>KEStore_Elems.add_calcs
wneuper@59403:   [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
s1210629013@52145:     ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
s1210629013@52145:     ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
wneuper@59430:         eval_precond_rootpbl"#Test.precond_rootpbl_"))]
wneuper@59472: \<close>
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 *)
wneuper@59430:   (case a of
wneuper@59430:      "Atools.pow" => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)
wneuper@59430:    | _ => (((a, 0), T), 0))
wneuper@59430:   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
wneuper@59430:   | dest_hd' (Var v) = (v, 2)
wneuper@59430:   | dest_hd' (Bound i) = ((("", i), dummyT), 3)
wneuper@59430:   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
wneuper@59430: (* RL *)
wneuper@59430: fun get_order_pow (t $ (Free(order,_))) = 
wneuper@59430:     	(case TermC.int_of_str_opt (order) of
wneuper@59430: 	             SOME d => d
wneuper@59430: 		   | NONE   => 0)
wneuper@59430:   | get_order_pow _ = 0;
wneuper@59430: 
wneuper@59430: fun size_of_term' (Const(str,_) $ t) =
wneuper@59430:   if "Atools.pow"=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)
wneuper@59430:   | term_ord' pr thy (t, u) =
wneuper@59430:     (if pr then 
wneuper@59430: 	 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
wneuper@59430: 	     val _ = tracing ("t= f@ts= \"" ^ Rule.term2str f ^ "\" @ \"[" ^
wneuper@59430: 	                      commas(map Rule.term2str ts) ^ "]\"")
wneuper@59430: 	     val _ = tracing ("u= g@us= \"" ^ Rule.term2str g ^"\" @ \"[" ^
wneuper@59430: 	                      commas(map Rule.term2str 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)
wneuper@59430: and terms_ord str pr (ts, us) = 
wneuper@59430:     list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
wneuper@59430: in
wneuper@59430: 
wneuper@59430: fun ord_make_polytest (pr:bool) thy (_: Rule.subst) tu = 
wneuper@59430:     (term_ord' pr thy(***) tu = LESS );
wneuper@59430: 
wneuper@59430: end;(*local*)
wneuper@59472: \<close> 
wneuper@59430: 
wneuper@59472: section \<open>term order\<close>
wneuper@59472: ML \<open>
wneuper@59416: fun term_order (_: Rule.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 = 
wneuper@59416:   Rule.Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 
wneuper@59416:       erls = Rule.e_rls, srls = Rule.Erls, 
neuper@42451:       calc = [], errpatts = [], 
wneuper@59416:       rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),
wneuper@59416: 	       Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
wneuper@59416: 	       Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
wneuper@59416: 	       Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
wneuper@59416: 	       Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
wneuper@59416: 	       Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
wneuper@59416: 	       Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
wneuper@59416: 	       Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
wneuper@59416: 	       Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
wneuper@59416: 	       Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}),
wneuper@59416: 	       Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}),
neuper@37954: 
wneuper@59416: 	       Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
wneuper@59416: 	       Rule.Calc ("Tools.matches",eval_matches ""),
neuper@37954:     
wneuper@59416: 	       Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
wneuper@59416: 	       Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
wneuper@59416: 	       Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37954: 		    
wneuper@59416: 	       Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 	       Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
neuper@37954: 	     	    
wneuper@59416: 	       Rule.Calc ("Atools.ident",eval_ident "#ident_")],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
wneuper@59406:       };      
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 =  
wneuper@59416:   Rule.Rls{id = "tval_rls", preconds = [], 
wneuper@59397:       rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), 
wneuper@59416:       erls=testerls,srls = Rule.e_rls, 
neuper@42451:       calc=[], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),
wneuper@59416: 	       Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
wneuper@59416: 	       Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
wneuper@59416: 	       Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
wneuper@59416: 	       Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
wneuper@59416: 	       Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
wneuper@59416: 	       Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
wneuper@59416: 	       Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
wneuper@59416: 	       Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
wneuper@59416: 	       Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}),
wneuper@59416: 	       Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}),
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("root_ge0",TermC.num_str @{thm root_ge0}),
wneuper@59416: 	       Rule.Thm ("root_add_ge0",TermC.num_str @{thm root_add_ge0}),
wneuper@59416: 	       Rule.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}),
wneuper@59416: 	       Rule.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}),
neuper@37954: 
wneuper@59416: 	       Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
wneuper@59416: 	       Rule.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),
wneuper@59416: 	       Rule.Calc ("Tools.matches",eval_matches ""),
wneuper@59416: 	       Rule.Calc ("Test.contains'_root",
neuper@37954: 		     eval_contains_root"#contains_root_"),
neuper@37954:     
wneuper@59416: 	       Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
wneuper@59416: 	       Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
wneuper@59416: 	       Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
wneuper@59416: 	       Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37954: 		    
wneuper@59416: 	       Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
wneuper@59416: 	       Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
neuper@37954: 	     	    
wneuper@59416: 	       Rule.Calc ("Atools.ident",eval_ident "#ident_")],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
wneuper@59406:       };      
wneuper@59472: \<close>
wneuper@59472: setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close>
neuper@52155: 
wneuper@59472: ML \<open>
neuper@37954: (*make () dissappear*)   
neuper@37954: val rearrange_assoc =
wneuper@59416:   Rule.Rls{id = "rearrange_assoc", preconds = [], 
wneuper@59416:       rew_ord = ("e_rew_ord",Rule.e_rew_ord), 
wneuper@59416:       erls = Rule.e_rls, srls = Rule.e_rls, calc = [], errpatts = [],
neuper@37954:       rules = 
wneuper@59416:       [Rule.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
wneuper@59416:        Rule.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
wneuper@59406:       };      
neuper@37954: 
neuper@37954: val ac_plus_times =
wneuper@59416:   Rule.Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
wneuper@59416:       erls = Rule.e_rls, srls = Rule.e_rls, calc = [], errpatts = [],
neuper@37954:       rules = 
wneuper@59416:       [Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
wneuper@59416:        Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
wneuper@59416:        Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
wneuper@59416:        Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
wneuper@59416:        Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
wneuper@59416:        Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
wneuper@59406:       };      
neuper@37954: 
wneuper@59389: (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
neuper@37954: val norm_equation =
wneuper@59416:   Rule.Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
wneuper@59416:       erls = tval_rls, srls = Rule.e_rls, calc = [], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
neuper@37954: 	       ],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
wneuper@59406:       };      
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37954: (* expects * distributed over + *)
neuper@37954: val Test_simplify =
wneuper@59416:   Rule.Rls{id = "Test_simplify", preconds = [], 
wneuper@59397:       rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
wneuper@59416:       erls = tval_rls, srls = Rule.e_rls, 
s1210629013@55444:       calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
neuper@37954:       rules = [
wneuper@59416: 	       Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
wneuper@59416: 	       Rule.Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}),
wneuper@59416: 	       Rule.Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}),
wneuper@59416: 	       Rule.Thm ("rdistr_right_assoc_p",TermC.num_str @{thm rdistr_right_assoc_p}),
wneuper@59416: 	       Rule.Thm ("rdistr_div_right",TermC.num_str @{thm rdistr_div_right}),
wneuper@59416: 	       Rule.Thm ("rbinom_power_2",TermC.num_str @{thm rbinom_power_2}),	       
neuper@37954: 
wneuper@59416:                Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}), 
wneuper@59416: 	       Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),
wneuper@59416: 	       Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
wneuper@59416: 	       Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
wneuper@59416: 	       Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
wneuper@59416: 	       Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc}),
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("radd_real_const_eq",TermC.num_str @{thm radd_real_const_eq}),
wneuper@59416: 	       Rule.Thm ("radd_real_const",TermC.num_str @{thm radd_real_const}),
neuper@37954: 	       (* these 2 rules are invers to distr_div_right wrt. termination.
neuper@37954: 		  thus they MUST be done IMMEDIATELY before calc *)
wneuper@59416: 	       Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
wneuper@59416: 	       Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
wneuper@59416: 	       Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
wneuper@59416: 	       Rule.Calc ("Atools.pow", eval_binop "#power_"),
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("rcollect_right",TermC.num_str @{thm rcollect_right}),
wneuper@59416: 	       Rule.Thm ("rcollect_one_left",TermC.num_str @{thm rcollect_one_left}),
wneuper@59416: 	       Rule.Thm ("rcollect_one_left_assoc",TermC.num_str @{thm rcollect_one_left_assoc}),
wneuper@59416: 	       Rule.Thm ("rcollect_one_left_assoc_p",TermC.num_str @{thm rcollect_one_left_assoc_p}),
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("rshift_nominator",TermC.num_str @{thm rshift_nominator}),
wneuper@59416: 	       Rule.Thm ("rcancel_den",TermC.num_str @{thm rcancel_den}),
wneuper@59416: 	       Rule.Thm ("rroot_square_inv",TermC.num_str @{thm rroot_square_inv}),
wneuper@59416: 	       Rule.Thm ("rroot_times_root",TermC.num_str @{thm rroot_times_root}),
wneuper@59416: 	       Rule.Thm ("rroot_times_root_assoc_p",TermC.num_str @{thm rroot_times_root_assoc_p}),
wneuper@59416: 	       Rule.Thm ("rsqare",TermC.num_str @{thm rsqare}),
wneuper@59416: 	       Rule.Thm ("power_1",TermC.num_str @{thm power_1}),
wneuper@59416: 	       Rule.Thm ("rtwo_of_the_same",TermC.num_str @{thm rtwo_of_the_same}),
wneuper@59416: 	       Rule.Thm ("rtwo_of_the_same_assoc_p",TermC.num_str @{thm rtwo_of_the_same_assoc_p}),
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("rmult_1",TermC.num_str @{thm rmult_1}),
wneuper@59416: 	       Rule.Thm ("rmult_1_right",TermC.num_str @{thm rmult_1_right}),
wneuper@59416: 	       Rule.Thm ("rmult_0",TermC.num_str @{thm rmult_0}),
wneuper@59416: 	       Rule.Thm ("rmult_0_right",TermC.num_str @{thm rmult_0_right}),
wneuper@59416: 	       Rule.Thm ("radd_0",TermC.num_str @{thm radd_0}),
wneuper@59416: 	       Rule.Thm ("radd_0_right",TermC.num_str @{thm radd_0_right})
neuper@37954: 	       ],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
s1210629013@55444: 		    (*since 040209 filled by prep_rls': STest_simplify*)
wneuper@59406:       };      
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@37954: (*isolate the root in a root-equation*)
neuper@37954: val isolate_root =
wneuper@59416:   Rule.Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord), 
wneuper@59416:       erls=tval_rls,srls = Rule.e_rls, calc=[], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
wneuper@59416: 	       Rule.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
wneuper@59416: 	       Rule.Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}),
wneuper@59416: 	       Rule.Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}),
wneuper@59416: 	       Rule.Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}),
wneuper@59416: 	       Rule.Thm ("risolate_root_div",TermC.num_str @{thm risolate_root_div})       ],
wneuper@59416:       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) 
neuper@37954:       "empty_script")
wneuper@59406:       };
neuper@37954: 
neuper@37954: (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
neuper@37954: val isolate_bdv =
wneuper@59416:     Rule.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
wneuper@59416: 	erls=tval_rls,srls = Rule.e_rls, calc= [], errpatts = [],
neuper@37954: 	rules = 
wneuper@59416: 	[Rule.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
wneuper@59416: 	 Rule.Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}),
wneuper@59416: 	 Rule.Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}),
wneuper@59416: 	 Rule.Thm ("mult_square",TermC.num_str @{thm mult_square}),
wneuper@59416: 	 Rule.Thm ("constant_square",TermC.num_str @{thm constant_square}),
wneuper@59416: 	 Rule.Thm ("constant_mult_square",TermC.num_str @{thm constant_mult_square})
neuper@37954: 	 ],
wneuper@59416: 	scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) 
neuper@37954: 			  "empty_script")
wneuper@59406: 	};      
wneuper@59472: \<close>
wneuper@59472: ML \<open>val prep_rls' = LTool.prep_rls @{theory};\<close>
wneuper@59472: setup \<open>KEStore_Elems.add_rlss 
s1210629013@55444:   [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), 
s1210629013@55444:   ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), 
s1210629013@55444:   ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), 
s1210629013@55444:   ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), 
s1210629013@55444:   ("matches", (Context.theory_name @{theory}, prep_rls'
wneuper@59430:     (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches",eval_matches "#matches_")])))]
wneuper@59472: \<close>
neuper@37954: 
wneuper@59472: subsection \<open>problems\<close>
neuper@37954: (** problem types **)
wneuper@59472: setup \<open>KEStore_Elems.add_pbts
wneuper@59416:   [(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Rule.e_rls, NONE, [])),
wneuper@59406:     (Specify.prep_pbt thy "pbl_test_equ" [] Celem.e_pblID
s1210629013@55339:       (["equation","test"],
s1210629013@55339:         [("#Given" ,["equality e_e","solveFor v_v"]),
s1210629013@55339:            ("#Where" ,["matches (?a = ?b) e_e"]),
s1210629013@55339:            ("#Find"  ,["solutions v_v'i'"])],
s1210629013@55339:         assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
wneuper@59406:     (Specify.prep_pbt thy "pbl_test_uni" [] Celem.e_pblID
s1210629013@55339:       (["univariate","equation","test"],
s1210629013@55339:         [("#Given" ,["equality e_e","solveFor v_v"]),
s1210629013@55339:            ("#Where" ,["matches (?a = ?b) e_e"]),
s1210629013@55339:            ("#Find"  ,["solutions v_v'i'"])],
s1210629013@55339:         assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
wneuper@59406:     (Specify.prep_pbt thy "pbl_test_uni_lin" [] Celem.e_pblID
s1210629013@55339:       (["LINEAR","univariate","equation","test"],
s1210629013@55339:         [("#Given" ,["equality e_e","solveFor v_v"]),
s1210629013@55339:            ("#Where" ,["(matches (   v_v = 0) e_e) | (matches (   ?b*v_v = 0) e_e) |" ^
s1210629013@55339:              "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)  "]),
s1210629013@55339:            ("#Find"  ,["solutions v_v'i'"])],
s1210629013@55339:         assoc_rls' @{theory} "matches", 
wneuper@59430:         SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))]
wneuper@59472: \<close>
wneuper@59472: ML \<open>
wneuper@59416: Rule.rew_ord' := overwritel (! Rule.rew_ord',
neuper@37954: [("termlessI", termlessI),
neuper@37954:  ("ord_make_polytest", ord_make_polytest false thy)
neuper@37954:  ]);
neuper@37954: 
neuper@37954: val make_polytest =
wneuper@59416:   Rule.Rls{id = "make_polytest", preconds = []:term list, 
neuper@52105:       rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
wneuper@59416:       erls = testerls, srls = Rule.Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@38034: 	      ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37954: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@42451: 	      ], errpatts = [],
wneuper@59416:       rules = [Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
neuper@37954: 	       (*"a - b = a + (-1) * b"*)
wneuper@59416: 	       Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
neuper@37954: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	       Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
neuper@37954: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
wneuper@59416: 	       Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
neuper@37954: 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
wneuper@59416: 	       Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
neuper@37954: 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
wneuper@59416: 	       Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),                 
neuper@37954: 	       (*"1 * z = z"*)
wneuper@59416: 	       Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),        
neuper@37954: 	       (*"0 * z = 0"*)
wneuper@59416: 	       Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
neuper@37954: 	       (*"0 + z = z"*)
neuper@37954: 
neuper@37954: 	       (*AC-rewriting*)
wneuper@59416: 	       Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
neuper@37954: 	       (* z * w = w * z *)
wneuper@59416: 	       Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
neuper@37954: 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
wneuper@59416: 	       Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),		
neuper@37954: 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
wneuper@59416: 	       Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),	
neuper@37954: 	       (*z + w = w + z*)
wneuper@59416: 	       Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
neuper@37954: 	       (*x + (y + z) = y + (x + z)*)
wneuper@59416: 	       Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),	               
neuper@37954: 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("sym_realpow_twoI",
wneuper@59389:                      TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),	
neuper@37954: 	       (*"r1 * r1 = r1 ^^^ 2"*)
wneuper@59416: 	       Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),		
neuper@37954: 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)
wneuper@59416: 	       Rule.Thm ("sym_real_mult_2",
wneuper@59389:                      TermC.num_str (@{thm real_mult_2} RS @{thm sym})),	
neuper@37954: 	       (*"z1 + z1 = 2 * z1"*)
wneuper@59416: 	       Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),	
neuper@37954: 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37954: 
wneuper@59416: 	       Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 
neuper@37954: 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
wneuper@59416: 	       Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
neuper@37954: 	       (*"[| l is_const; m is_const |] ==>  
neuper@37954: 				l * n + (m * n + k) =  (l + m) * n + k"*)
wneuper@59416: 	       Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),	
neuper@37954: 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
wneuper@59416: 	       Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 
neuper@37954: 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37954: 
wneuper@59416: 	       Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
wneuper@59416: 	       Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
wneuper@59416: 	       Rule.Calc ("Atools.pow", eval_binop "#power_")
neuper@37954: 	       ],
wneuper@59416:       scr = Rule.EmptyScr(*Rule.Prog ((Thm.term_of o the o (parse thy)) 
neuper@37954:       scr_make_polytest)*)
wneuper@59406:       }; 
neuper@37954: 
neuper@37954: val expand_binomtest =
wneuper@59416:   Rule.Rls{id = "expand_binomtest", preconds = [], 
neuper@37954:       rew_ord = ("termlessI",termlessI),
wneuper@59416:       erls = testerls, srls = Rule.Erls,
neuper@38014:       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 
neuper@38034: 	      ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37954: 	      ("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@42451: 	      ], errpatts = [],
neuper@38001:       rules = 
wneuper@59416:       [Rule.Thm ("real_plus_binom_pow2"  ,TermC.num_str @{thm real_plus_binom_pow2}),     
neuper@37954: 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
wneuper@59416:        Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),    
neuper@37954: 	      (*"(a + b)*(a + b) = ...*)
wneuper@59416:        Rule.Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),   
neuper@38001:        (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
wneuper@59416:        Rule.Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),   
neuper@38001:        (*"(a - b)*(a - b) = ...*)
wneuper@59416:        Rule.Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),   
neuper@38001:         (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
wneuper@59416:        Rule.Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),   
neuper@38001:         (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
neuper@38001:        (*RL 020915*)
wneuper@59416:        Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}), 
neuper@38001:         (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
wneuper@59416:        Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}), 
neuper@38001:         (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
wneuper@59416:        Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}), 
neuper@38001:         (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
wneuper@59416:        Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}), 
neuper@38001:         (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
wneuper@59416:        Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),                
neuper@38001:         (*(a*b)^^^n = a^^^n * b^^^n*)
wneuper@59416:        Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
neuper@38001:         (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
wneuper@59416:        Rule.Thm ("real_minus_binom_pow3",TermC.num_str @{thm real_minus_binom_pow3}),
neuper@38001:         (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
neuper@37954: 
neuper@37954: 
wneuper@59416:      (*  Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),	
neuper@38001: 	 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
wneuper@59416: 	Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),	
neuper@38001: 	(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
wneuper@59416: 	Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),	
neuper@38001: 	(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
wneuper@59416: 	Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),	
neuper@38001: 	(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
neuper@38001: 	*)
neuper@38001: 	
wneuper@59416: 	Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),              
neuper@38001:          (*"1 * z = z"*)
wneuper@59416: 	Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),              
neuper@38001:          (*"0 * z = 0"*)
wneuper@59416: 	Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
neuper@38001:          (*"0 + z = z"*)
neuper@37954: 
wneuper@59416: 	Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
wneuper@59416: 	Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
wneuper@59416: 	Rule.Calc ("Atools.pow", eval_binop "#power_"),
neuper@38001:         (*	       
wneuper@59416: 	 Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),		
neuper@38001:         (*AC-rewriting*)
wneuper@59416: 	Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
wneuper@59416: 	Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
wneuper@59416: 	Rule.Thm ("add_commute",TermC.num_str @{thm add_commute}),	
wneuper@59416: 	Rule.Thm ("add_left_commute",TermC.num_str @{thm add_left_commute}),
wneuper@59416: 	Rule.Thm ("add_assoc",TermC.num_str @{thm add_assoc}),
neuper@38001: 	*)
neuper@38001: 	
wneuper@59416: 	Rule.Thm ("sym_realpow_twoI",
wneuper@59389:               TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@38001: 	(*"r1 * r1 = r1 ^^^ 2"*)
wneuper@59416: 	Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),			
neuper@38001: 	(*"r * r ^^^ n = r ^^^ (n + 1)"*)
wneuper@59416: 	(*Rule.Thm ("sym_real_mult_2",
wneuper@59389:                 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@38001: 	(*"z1 + z1 = 2 * z1"*)*)
wneuper@59416: 	Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),		
neuper@38001: 	(*"z1 + (z1 + k) = 2 * z1 + k"*)
neuper@37954: 
wneuper@59416: 	Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 
neuper@38001: 	(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
wneuper@59416: 	Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),	
neuper@38001: 	(*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)
wneuper@59416: 	Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),		
neuper@38001: 	(*"m is_const ==> n + m * n = (1 + m) * n"*)
wneuper@59416: 	Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 
neuper@38001: 	(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
neuper@37954: 
wneuper@59416: 	Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
wneuper@59416: 	Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
wneuper@59416: 	Rule.Calc ("Atools.pow", eval_binop "#power_")
neuper@38001: 	],
wneuper@59416:       scr = Rule.EmptyScr
wneuper@59186: (*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
wneuper@59406:       };      
wneuper@59472: \<close>
wneuper@59472: setup \<open>KEStore_Elems.add_rlss 
s1210629013@55444:   [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)), 
wneuper@59472:   ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\<close>
wneuper@59472: setup \<open>KEStore_Elems.add_rlss 
wneuper@59430:   [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)), 
wneuper@59430:   ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)), 
wneuper@59472:   ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\<close>
wneuper@59430: 
wneuper@59472: section \<open>problems\<close>
wneuper@59472: setup \<open>KEStore_Elems.add_pbts
wneuper@59430:   [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Celem.e_pblID
wneuper@59430:     (["plain_square","univariate","equation","test"],
wneuper@59430:       [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:         ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
wneuper@59430: 	        "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
wneuper@59430: 	        "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
wneuper@59430: 	        "(matches (        v_v ^^^2 = 0) e_e)"]),
wneuper@59430:         ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:       assoc_rls' @{theory} "matches", 
wneuper@59430:       SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_poly" [] Celem.e_pblID
wneuper@59430:       (["polynomial","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["HOL.False"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.e_rls, SOME "solve (e_e::bool, v_v)", [])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Celem.e_pblID
wneuper@59430:       (["degree_two","polynomial","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Celem.e_pblID
wneuper@59430:       (["pq_formula","degree_two","polynomial","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Celem.e_pblID
wneuper@59430:       (["abc_formula","degree_two","polynomial","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_root" [] Celem.e_pblID
wneuper@59430:       (["squareroot","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["precond_rootpbl v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.append_rls "contains_root" Rule.e_rls [Rule.Calc ("Test.contains'_root",
wneuper@59430:             eval_contains_root "#contains_root_")], 
wneuper@59430:         SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_norm" [] Celem.e_pblID
wneuper@59430:       (["normalise","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,[]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Celem.e_pblID
wneuper@59430:       (["sqroot-test","univariate","equation","test"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["precond_rootpbl v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         Rule.e_rls, SOME "solve (e_e::bool, v_v)", [])),
wneuper@59430:     (Specify.prep_pbt thy "pbl_test_intsimp" [] Celem.e_pblID
wneuper@59430:       (["inttype","test"],
wneuper@59430:         [("#Given" ,["intTestGiven t_t"]),
wneuper@59430:           ("#Where" ,[]),
wneuper@59430:           ("#Find"  ,["intTestFind s_s"])],
wneuper@59472:       Rule.e_rls, NONE, [["Test","intsimp"]]))]\<close>
wneuper@59430: 
wneuper@59472: section \<open>methods\<close>
wneuper@59472: subsection \<open>differentiate\<close>
wneuper@59430: partial_function (tailrec) dummy1 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy1 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
wneuper@59430:       (["Test"], [],
wneuper@59430:         {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
wneuper@59473:           crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")]
wneuper@59473: \<close>
wneuper@59473: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
wneuper@59430:       (["Test","solve_linear"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["matches (?a = ?b) e_e"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
wneuper@59430:           prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
wneuper@59430:           nrls = Test_simplify},
wneuper@59430:         "Script Solve_linear (e_e::bool) (v_v::real)=                     " ^
wneuper@59430:           "(let e_e =                                                       " ^
wneuper@59430:           "  Repeat                                                         " ^
wneuper@59430:           "    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@  " ^
wneuper@59430:           "      (Rewrite_Set Test_simplify False))) e_e" ^
wneuper@59430:           " in [e_e::bool])")]
wneuper@59472: \<close>
wneuper@59472: subsection \<open>root equation\<close>
wneuper@59430: partial_function (tailrec) dummy2 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy2 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy  "met_test_sqrt" [] Celem.e_metID
wneuper@59430:       (*root-equation, version for tests before 8.01.01*)
wneuper@59430:       (["Test","sqrt-equ-test"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["contains_root (e_e::bool)"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,
wneuper@59430:           srls = Rule.append_rls "srls_contains_root" Rule.e_rls
wneuper@59430:               [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
wneuper@59430:           prls = Rule.append_rls "prls_contains_root" Rule.e_rls 
wneuper@59430:               [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
wneuper@59430:           calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
wneuper@59430:           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
wneuper@59430:         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
wneuper@59430:           "(let e_e = " ^
wneuper@59430:           "   ((While (contains_root e_e) Do" ^
wneuper@59430:           "      ((Rewrite square_equation_left True) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set isolate_root False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)))) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set norm_equation False)) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:           "    (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set Test_simplify False)))" ^
wneuper@59430:           "   e_e" ^
wneuper@59430:           " in [e_e::bool])")]
wneuper@59472: \<close>
wneuper@59430: partial_function (tailrec) dummy3 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy3 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy  "met_test_sqrt2" [] Celem.e_metID
wneuper@59430:       (*root-equation ... for test-*.sml until 8.01*)
wneuper@59430:       (["Test","squ-equ-test2"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,
wneuper@59430:           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 
wneuper@59430:               [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
wneuper@59430:           prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
wneuper@59430:           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
wneuper@59430:         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
wneuper@59430:           "(let e_e = " ^
wneuper@59430:           "   ((While (contains_root e_e) Do" ^
wneuper@59430:           "      ((Rewrite square_equation_left True) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set isolate_root False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)))) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set norm_equation False)) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:           "    (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set Test_simplify False)))" ^
wneuper@59430:           "   e_e;" ^
wneuper@59430:           "  (L_L::bool list) = Tac subproblem_equation_dummy;          " ^
wneuper@59430:           "  L_L = Tac solve_equation_dummy                             " ^
wneuper@59430:           "  in Check_elementwise L_L {(v_v::real). Assumptions})")]
wneuper@59472: \<close>
wneuper@59477: 
wneuper@59477: partial_function (tailrec) solve_root_equation ::
wneuper@59477:   "bool \<Rightarrow> real \<Rightarrow> bool list"
wneuper@59477: where "minisubpbl e_e v_v =
wneuper@59477:   (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
wneuper@59477:               (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
wneuper@59477:       (L_L::bool list) =
wneuper@59477:              (SubProblem (''TestX'',
wneuper@59477:                  [''LINEAR'', ''univariate'', ''equation'', ''test''],
wneuper@59477:                  [''Test'', ''solve_linear''])
wneuper@59477:                [BOOL e_e, REAL v_v])
wneuper@59477:    in Check_elementwise L_L {(v_v::real). Assumptions})"
wneuper@59477: 
wneuper@59477: (* ^^^used for test/../Minisubpbl/
wneuper@59477: # difference between partial_function above and Script below:
wneuper@59477: "Solve_root_equation" is a constant, which is NOT accepted by partial_function
wneuper@59477: 
wneuper@59477: # differences between original "Solve_root_equation" and the version below:
wneuper@59477: (1) the program name, see note above
wneuper@59477: (2) the first argument of SubProblem: ''Test''' is NOT accepted by partial_function,
wneuper@59477:     thus previous change-set Test' \<longrightarrow> TestX
wneuper@59477: ''Test'#TODO#''. Note: this change is NOT recognised by Interpret!
wneuper@59477: *)
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
wneuper@59430:       (*tests subproblem fixed linear*)
wneuper@59430:       (["Test","squ-equ-test-subpbl1"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["precond_rootmet v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
wneuper@59430:           prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls
wneuper@59430:               [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
wneuper@59430:           calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
wneuper@59477:         "Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^
wneuper@59477:         " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@               " ^
wneuper@59477:         "             (Try (Rewrite_Set Test_simplify False))) e_e;            " ^
wneuper@59477:         "     (L_L::bool list) =                                               " ^
wneuper@59477:         "            (SubProblem (''TestX'',                                   " ^
wneuper@59477:         "                [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
wneuper@59477:         "                [''Test'', ''solve_linear''])                         " ^
wneuper@59477:         "              [BOOL e_e, REAL v_v])                                   " ^
wneuper@59477:         "  in Check_elementwise L_L {(v_v::real). Assumptions})                ")]
wneuper@59472: \<close>
wneuper@59430: partial_function (tailrec) dummy7 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy7 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy  "met_test_eq1" [] Celem.e_metID
wneuper@59430:       (*root-equation1:*)
wneuper@59430:       (["Test","square_equation1"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,
wneuper@59430:           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 
wneuper@59430:             [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls,
wneuper@59430:               errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
wneuper@59430:               ("square_equation_right","")]*)},
wneuper@59430:         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
wneuper@59430:           "(let e_e = " ^
wneuper@59430:           "   ((While (contains_root e_e) Do" ^
wneuper@59430:           "      ((Rewrite square_equation_left True) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set isolate_root False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)))) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set norm_equation False)) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set Test_simplify False)))" ^
wneuper@59430:           "   e_e;" ^
wneuper@59430:           "  (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
wneuper@59430:           "                    [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
wneuper@59430:           "  in Check_elementwise L_L {(v_v::real). Assumptions})")]
wneuper@59472: \<close>
wneuper@59430: partial_function (tailrec) dummy8 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy8 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
wneuper@59430:       (*root-equation2*)
wneuper@59430:         (["Test","square_equation2"],
wneuper@59430:           [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,
wneuper@59430:           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 
wneuper@59430:               [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
wneuper@59430:           prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
wneuper@59430:           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
wneuper@59430:         "Script Solve_root_equation (e_e::bool) (v_v::real)  =  " ^
wneuper@59430:         "(let e_e = " ^
wneuper@59430:         "   ((While (contains_root e_e) Do" ^
wneuper@59430:         "      (((Rewrite square_equation_left True) Or " ^
wneuper@59430:         "        (Rewrite square_equation_right True)) @@" ^
wneuper@59430:         "       (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:         "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^
wneuper@59430:         "       (Try (Rewrite_Set isolate_root False)) @@" ^
wneuper@59430:         "       (Try (Rewrite_Set Test_simplify False)))) @@" ^
wneuper@59430:         "    (Try (Rewrite_Set norm_equation False)) @@" ^
wneuper@59430:         "    (Try (Rewrite_Set Test_simplify False)))" ^
wneuper@59430:         "   e_e;" ^
wneuper@59430:         "  (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
wneuper@59430:         "                    [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
wneuper@59430:         "  in Check_elementwise L_L {(v_v::real). Assumptions})")]
wneuper@59472: \<close>
wneuper@59430: partial_function (tailrec) dummy9 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy9 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
wneuper@59430:       (*root-equation*)
wneuper@59430:       (["Test","square_equation"],
wneuper@59430:         [("#Given" ,["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,
wneuper@59430:           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 
wneuper@59430:               [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
wneuper@59430:           prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
wneuper@59430:           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
wneuper@59430:         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
wneuper@59430:           "(let e_e = " ^
wneuper@59430:           "   ((While (contains_root e_e) Do" ^
wneuper@59430:           "      (((Rewrite square_equation_left True) Or" ^
wneuper@59430:           "        (Rewrite square_equation_right True)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set isolate_root False)) @@" ^
wneuper@59430:           "       (Try (Rewrite_Set Test_simplify False)))) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set norm_equation False)) @@" ^
wneuper@59430:           "    (Try (Rewrite_Set Test_simplify False)))" ^
wneuper@59430:           "   e_e;" ^
wneuper@59430:           "  (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
wneuper@59430:           "                    [no_met]) [BOOL e_e, REAL v_v])" ^
wneuper@59430:           "  in Check_elementwise L_L {(v_v::real). Assumptions})")]
wneuper@59472: \<close>
wneuper@59430: partial_function (tailrec) dummy10 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy10 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
wneuper@59430:       (*solve_plain_square*)
wneuper@59430:       (["Test","solve_plain_square"],
wneuper@59430:         [("#Given",["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
wneuper@59430:               "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
wneuper@59430:               "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
wneuper@59430:               "(matches (        v_v ^^^2 = 0) e_e)"]), 
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls,
wneuper@59430:           prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,
wneuper@59430:           asm_rls=[],asm_thm=[]*)},
wneuper@59430:         "Script Solve_plain_square (e_e::bool) (v_v::real) =           " ^
wneuper@59430:           " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@         " ^
wneuper@59430:           "            (Try (Rewrite_Set Test_simplify False)) @@     " ^
wneuper@59430:           "            ((Rewrite square_equality_0 False) Or        " ^
wneuper@59430:           "             (Rewrite square_equality True)) @@            " ^
wneuper@59430:           "            (Try (Rewrite_Set tval_rls False))) e_e             " ^
wneuper@59430:           "  in ((Or_to_List e_e)::bool list))")]
wneuper@59472: \<close>
wneuper@59472: subsection \<open>polynomial equation\<close>
wneuper@59430: partial_function (tailrec) dummy11 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy11 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
wneuper@59430:       (["Test","norm_univar_equation"],
wneuper@59430:         [("#Given",["equality e_e","solveFor v_v"]),
wneuper@59430:           ("#Where" ,[]), 
wneuper@59430:           ("#Find"  ,["solutions v_v'i'"])],
wneuper@59430:         {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,
wneuper@59430:           errpats = [], nrls = Rule.e_rls},
wneuper@59430:         "Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^
wneuper@59430:           " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@   " ^
wneuper@59430:           "            (Try (Rewrite_Set Test_simplify False))) e_e   " ^
wneuper@59430:           "  in (SubProblem (Test',[univariate,equation,test],         " ^
wneuper@59430:           "                    [no_met]) [BOOL e_e, REAL v_v]))")]
wneuper@59472: \<close>
wneuper@59472: subsection \<open>diophantine equation\<close>
wneuper@59430: partial_function (tailrec) dummy12 :: "real \<Rightarrow> real"
wneuper@59430:   where "dummy12 xxx = xxx"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
wneuper@59473:     [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
wneuper@59430:       (["Test","intsimp"],
wneuper@59430:         [("#Given" ,["intTestGiven t_t"]),
wneuper@59430:           ("#Where" ,[]),
wneuper@59430:           ("#Find"  ,["intTestFind s_s"])],
wneuper@59430:         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,  prls = Rule.e_rls, calc = [],
wneuper@59430:           crls = tval_rls, errpats = [], nrls = Test_simplify},
wneuper@59430:         "Script STest_simplify (t_t::int) =                  " ^
wneuper@59430:           "(Repeat                                                          " ^
wneuper@59430:           "    ((Try (Calculate PLUS)) @@  " ^
wneuper@59430:           "     (Try (Calculate TIMES))) t_t::int)")]
wneuper@59472: \<close>
wneuper@59430: 
neuper@37906: end




