(* Knowledge for tests, specifically simplified or bound to a fixed state

    for the purpose of simplifying tests.

    Author: Walther Neuper 2003

    (c) due to copyright terms

 Notes on cleanup:

 (0) revert import Test -- DiophantEq, this raises issues related to (1..4)

 (1) transfer methods to respective theories, if only test, then hierarchy at ["...", "Test"]:

     differentiate, root equatioh, polynomial equation, diophantine equation

 (2) transfer problems accordingly

 (3) rearrange rls according to (1..2)

 (4) rearrange axiomatizations according to (3)

 *) 

 theory Test imports Base_Tools Poly Rational Root Diff begin

 section \<open>consts\<close>

 subsection \<open>for scripts\<close>

 consts

   Solve'_univar'_err

              :: "[bool,real,bool,  

 		    bool list] => bool list"

                ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9)

   Solve'_linear

              :: "[bool,real,  

 		    bool list] => bool list"

                ("((Script Solve'_linear (_ _ =))// (_))" 9)

   Solve'_root'_equation 

              :: "[bool,real,  

 		    bool list] => bool list"

                ("((Script Solve'_root'_equation (_ _ =))// (_))" 9)

   Solve'_plain'_square 

              :: "[bool,real,  

 		    bool list] => bool list"

                ("((Script Solve'_plain'_square (_ _ =))// (_))" 9)

   Norm'_univar'_equation 

              :: "[bool,real,  

 		    bool] => bool"

                ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9)

   STest'_simplify

              :: "['z,  

 		    'z] => 'z"

                ("((Script STest'_simplify (_ =))// (_))" 9)

 subsection \<open>for problems\<close>

 consts

   "is'_root'_free"   :: "'a => bool"      ("is'_root'_free _" 10)

   "contains'_root"   :: "'a => bool"      ("contains'_root _" 10)

   "precond'_rootmet" :: "'a => bool"      ("precond'_rootmet _" 10)

   "precond'_rootpbl" :: "'a => bool"      ("precond'_rootpbl _" 10)

   "precond'_submet"  :: "'a => bool"      ("precond'_submet _" 10)

   "precond'_subpbl"  :: "'a => bool"      ("precond'_subpbl _" 10)

 section \<open>functions\<close>

 ML \<open>

 fun bin_o (Const (op_, (Type ("fun", [Type (s2, []), Type ("fun", [Type (s4, _),Type (s5, _)])]))))

       = if s2 = s4 andalso s4 = s5 then [op_] else []

     | bin_o _ = [];

 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)

   | bin_op t         =  bin_o t;

 fun is_bin_op t = (bin_op t <> []);

 fun bin_op_arg1 ((Const (_,

     (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) $ arg1 $ _) = arg1

   | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ Rule.term2str t);

 fun bin_op_arg2 ((Const (_,

     (Type ("fun", [Type (_, []),Type ("fun", [Type _, Type _])]))))$ _ $ arg2) = arg2

   | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ Rule.term2str t);

 exception NO_EQUATION_TERM;

 fun is_equation ((Const ("HOL.eq",

     (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ _ $ _) = true

   | is_equation _ = false;

 fun equ_lhs ((Const ("HOL.eq",

     (Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ l $ _) = l

   | equ_lhs _ = raise NO_EQUATION_TERM;

 fun equ_rhs ((Const ("HOL.eq", (Type ("fun",

 		 [Type (_, []), Type ("fun", [Type (_, []), Type ("bool",[])])])))) $ _ $ r) = r

   | equ_rhs _ = raise NO_EQUATION_TERM;

 fun atom (Const (_, Type (_,[]))) = true

   | atom (Free (_, Type (_,[]))) = true

   | atom (Var (_, Type (_,[]))) = true

   | atom((Const ("Bin.integ_of_bin",_)) $ _) = true

   | atom _ = false;

 fun varids (Const (s, Type (_,[]))) = [strip_thy s]

   | varids (Free (s, Type (_,[]))) = if TermC.is_num' s then [] else [strip_thy s]  

   | varids (Var((s, _),Type (_,[]))) = [strip_thy s]

 (*| varids (_      (s,"?DUMMY"   )) =   ..ML-error *)

   | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)

   | varids (Abs (a, _, t)) = union op = [a] (varids t)

   | varids (t1 $ t2) = union op = (varids t1) (varids t2)

   | varids _ = [];

 fun bin_ops_only ((Const op_) $ t1 $ t2) =

     if is_bin_op (Const op_) then bin_ops_only t1 andalso bin_ops_only t2 else false

   | bin_ops_only t = if atom t then true else bin_ops_only t;

 fun polynomial opl t _(* bdVar TODO *) =

     subset op = (bin_op t, opl) andalso (bin_ops_only t);

 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) 

     andalso polynomial opl (equ_lhs t) bdVar 

     andalso polynomial opl (equ_rhs t) bdVar

     andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse

              subset op = (varids bdVar, varids (equ_lhs t)));

 fun max (a,b) = if a < b then b else a;

 fun degree addl mul bdVar t =

 let

 fun deg _ _ v (Const  (s, Type (_, []))) = if v=strip_thy s then 1 else 0

   | deg _ _ v (Free   (s, Type (_, []))) = if v=strip_thy s then 1 else 0

   | deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy s then 1 else 0

 (*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *) 

   | deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0 

   | deg addl mul v (h $ t1 $ t2) =

     if subset op = (bin_op h, addl)

     then max (deg addl mul v t1  , deg addl mul v t2)

     else (*mul!*)(deg addl mul v t1) + (deg addl mul v t2)

   | deg _ _ _ t = raise ERROR ("deg: t = " ^ Rule.term2str t)

 in

   if polynomial (addl @ [mul]) t bdVar

   then SOME (deg addl mul (id_of bdVar) t)

   else (NONE:int option)

 end;

 fun degree_ addl mul bdVar t = (* do not export *)

 let

   fun opt (SOME i)= i

 	  | opt  NONE = 0

 in opt (degree addl mul bdVar t) end;

 fun linear addl mul t bdVar = (degree_ addl mul bdVar t) < 2;

 fun linear_equ addl mul bdVar t =

   if is_equation t 

   then

     let

       val degl = degree_ addl mul bdVar (equ_lhs t);

 	    val degr = degree_ addl mul bdVar (equ_rhs t)

 	  in if (degl>0 orelse degr>0)andalso max(degl,degr) < 2 then true else false end

   else false;

 (* strip_thy op_  before *)

 fun is_div_op (dv, (Const (op_,

     (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) ) = (dv = strip_thy op_)

   | is_div_op _ = false;

 fun is_denom bdVar div_op t =

     let fun is bool[v]dv (Const  (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

 	  | is bool[v]dv (Free   (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false) 

 	  | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

 	  | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false

 	  | is bool[v]dv (h$n$d) = 

 	      if is_div_op(dv,h) 

 	      then (is false[v]dv n)orelse(is true[v]dv d)

 	      else (is bool [v]dv n)orelse(is bool[v]dv d)

 in is false (varids bdVar) (strip_thy div_op) t end;

 fun rational t div_op bdVar = 

     is_denom bdVar div_op t andalso bin_ops_only t;

 \<close>

 section \<open>axiomatizations\<close>

 axiomatization where (*TODO: prove as theorems*)

   radd_mult_distrib2:      "(k::real) * (m + n) = k * m + k * n" and

   rdistr_right_assoc:      "(k::real) + l * n + m * n = k + (l + m) * n" and

   rdistr_right_assoc_p:    "l * n + (m * n + (k::real)) = (l + m) * n + k" and

   rdistr_div_right:        "((k::real) + l) / n = k / n + l / n" and

   rcollect_right:

           "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and

   rcollect_one_left:

           "m is_const ==> (n::real) + m * n = (1 + m) * n" and

   rcollect_one_left_assoc:

           "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and

   rcollect_one_left_assoc_p:

           "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and

   rtwo_of_the_same:        "a + a = 2 * a" and

   rtwo_of_the_same_assoc:  "(x + a) + a = x + 2 * a" and

   rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and

   rcancel_den:             "not(a=0) ==> a * (b / a) = b" and

   rcancel_const:           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and

   rshift_nominator:        "(a::real) * b / c = a / c * b" and

   exp_pow:                 "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and

   rsqare:                  "(a::real) * a = a ^^^ 2" and

   power_1:                 "(a::real) ^^^ 1 = a" and

   rbinom_power_2:          "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" and

   rmult_1:                 "1 * k = (k::real)" and

   rmult_1_right:           "k * 1 = (k::real)" and

   rmult_0:                 "0 * k = (0::real)" and

   rmult_0_right:           "k * 0 = (0::real)" and

   radd_0:                  "0 + k = (k::real)" and

   radd_0_right:            "k + 0 = (k::real)" and

   radd_real_const_eq:

           "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and

   radd_real_const:

           "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"  

    and

 (*for AC-operators*)

   radd_commute:            "(m::real) + (n::real) = n + m" and

   radd_left_commute:       "(x::real) + (y + z) = y + (x + z)" and

   radd_assoc:              "(m::real) + n + k = m + (n + k)" and

   rmult_commute:           "(m::real) * n = n * m" and

   rmult_left_commute:      "(x::real) * (y * z) = y * (x * z)" and

   rmult_assoc:             "(m::real) * n * k = m * (n * k)" and

 (*for equations: 'bdv' is a meta-constant*)

   risolate_bdv_add:       "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and

   risolate_bdv_mult_add:  "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and

   risolate_bdv_mult:      "((n::real) * bdv = m) = (bdv = m / n)" and

   rnorm_equation_add:

       "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and

 (*17.9.02 aus SqRoot.thy------------------------------vvv---*) 

   root_ge0:            "0 <= a ==> 0 <= sqrt a" and

   (*should be dropped with better simplification in eval_rls ...*)

   root_add_ge0:

 	"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and

   root_ge0_1:

 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and

   root_ge0_2:

 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and

   rroot_square_inv:         "(sqrt a)^^^ 2 = a" and

   rroot_times_root:         "sqrt a * sqrt b = sqrt(a*b)" and

   rroot_times_root_assoc:   "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and

   rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and

 (*for root-equations*)

   square_equation_left:

           "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and

   square_equation_right:

           "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and

   (*causes frequently non-termination:*)

   square_equation:  

           "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" and

   risolate_root_add:        "(a+  sqrt c = d) = (  sqrt c = d + (-1)*a)" and

   risolate_root_mult:       "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and

   risolate_root_div:        "(a * sqrt c = d) = (  sqrt c = d / a)" and

 (*for polynomial equations of degree 2; linear case in RatArith*)

   mult_square:		"(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and

   constant_square:       "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and

   constant_mult_square:  "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and

   square_equality: 

 	     "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and

   square_equality_0:

 	     "(x^^^2 = 0) = (x = 0)" and

 (*isolate root on the LEFT hand side of the equation

   otherwise shuffling from left to right would not terminate*)  

   rroot_to_lhs:

           "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and

   rroot_to_lhs_mult:

           "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and

   rroot_to_lhs_add_mult:

           "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"

 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)  

 section \<open>eval functions\<close>

 ML \<open>

 val thy = @{theory};

 (** evaluation of numerals and predicates **)

 (*does a term contain a root ?*)

 fun eval_contains_root (thmid:string) _ 

 		       (t as (Const("Test.contains'_root",t0) $ arg)) thy = 

   if member op = (ids_of arg) "sqrt"

   then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"",

 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"",

 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

 | eval_contains_root _ _ _ _ = NONE; 

 (*dummy precondition for root-met of x+1=2*)

 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy = 

     SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg)"",

       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

   | eval_precond_rootmet _ _ _ _ = NONE; 

 (*dummy precondition for root-pbl of x+1=2*)

 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy = 

     SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",

 	    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

 	| eval_precond_rootpbl _ _ _ _ = NONE;

 \<close>

 setup \<open>KEStore_Elems.add_calcs

   [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),

     ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),

     ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",

         eval_precond_rootpbl"#Test.precond_rootpbl_"))]

 \<close>

 ML \<open>

 (*8.4.03  aus Poly.ML--------------------------------vvv---

   make_polynomial  ---> make_poly

   ^-- for user          ^-- for systest _ONLY_*)  

 local (*. for make_polytest .*)

 open Term;  (* for type order = EQUAL | LESS | GREATER *)

 fun pr_ord EQUAL = "EQUAL"

   | pr_ord LESS  = "LESS"

   | pr_ord GREATER = "GREATER";

 fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)

   (case a of

      "Atools.pow" => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)

    | _ => (((a, 0), T), 0))

   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)

   | dest_hd' (Var v) = (v, 2)

   | dest_hd' (Bound i) = ((("", i), dummyT), 3)

   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);

 (* RL *)

 fun get_order_pow (t $ (Free(order,_))) = 

     	(case TermC.int_of_str_opt (order) of

 	             SOME d => d

 		   | NONE   => 0)

   | get_order_pow _ = 0;

 fun size_of_term' (Const(str,_) $ t) =

   if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)

   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body

   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t

   | size_of_term' _ = 1;

 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

     (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) 

                                    | ord => ord)

   | term_ord' pr thy (t, u) =

     (if pr then 

 	 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;

 	     val _ = tracing ("t= f@ts= \"" ^ Rule.term2str f ^ "\" @ \"[" ^

 	                      commas(map Rule.term2str ts) ^ "]\"")

 	     val _ = tracing ("u= g@us= \"" ^ Rule.term2str g ^"\" @ \"[" ^

 	                      commas(map Rule.term2str us) ^"]\"")

 	     val _ = tracing ("size_of_term(t,u)= (" ^

 	                      string_of_int (size_of_term' t) ^ ", " ^

 	                      string_of_int (size_of_term' u) ^ ")")

 	     val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o hd_ord) (f,g))

 	     val _ = tracing ("terms_ord(ts,us) = " ^

 			      (pr_ord o terms_ord str false) (ts,us));

 	     val _ = tracing "-------"

 	 in () end

        else ();

 	 case int_ord (size_of_term' t, size_of_term' u) of

 	   EQUAL =>

 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in

 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) 

 	     | ord => ord)

 	     end

 	 | ord => ord)

 and hd_ord (f, g) =                                        (* ~ term.ML *)

   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)

 and terms_ord str pr (ts, us) = 

     list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);

 in

 fun ord_make_polytest (pr:bool) thy (_: Rule.subst) tu = 

     (term_ord' pr thy(***) tu = LESS );

 end;(*local*)

 \<close> 

 section \<open>term order\<close>

 ML \<open>

 fun term_order (_: Rule.subst) tu = (term_ordI [] tu = LESS);

 \<close>

 section \<open>rulesets\<close>

 ML \<open>

 val testerls = 

   Rule.Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 

       erls = Rule.e_rls, srls = Rule.Erls, 

       calc = [], errpatts = [], 

       rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),

 	       Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),

 	       Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),

 	       Rule.Thm ("not_true",TermC.num_str @{thm not_true}),

 	       Rule.Thm ("not_false",TermC.num_str @{thm not_false}),

 	       Rule.Thm ("and_true",TermC.num_str @{thm and_true}),

 	       Rule.Thm ("and_false",TermC.num_str @{thm and_false}),

 	       Rule.Thm ("or_true",TermC.num_str @{thm or_true}),

 	       Rule.Thm ("or_false",TermC.num_str @{thm or_false}),

 	       Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}),

 	       Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}),

 	       Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),

 	       Rule.Calc ("Tools.matches", Tools.eval_matches ""),

 	       Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),

 	       Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),

 	       Rule.Calc ("Atools.pow" ,eval_binop "#power_"),

 	       Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

 	       Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

 	       Rule.Calc ("Atools.ident",eval_ident "#ident_")],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

       };      

 \<close>

 ML \<open>

 (*.for evaluation of conditions in rewrite rules.*)

 (*FIXXXXXXME 10.8.02: handle like _simplify*)

 val tval_rls =  

   Rule.Rls{id = "tval_rls", preconds = [], 

       rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), 

       erls=testerls,srls = Rule.e_rls, 

       calc=[], errpatts = [],

       rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),

 	       Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),

 	       Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),

 	       Rule.Thm ("not_true",TermC.num_str @{thm not_true}),

 	       Rule.Thm ("not_false",TermC.num_str @{thm not_false}),

 	       Rule.Thm ("and_true",TermC.num_str @{thm and_true}),

 	       Rule.Thm ("and_false",TermC.num_str @{thm and_false}),

 	       Rule.Thm ("or_true",TermC.num_str @{thm or_true}),

 	       Rule.Thm ("or_false",TermC.num_str @{thm or_false}),

 	       Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}),

 	       Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}),

 	       Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),

 	       Rule.Thm ("root_ge0",TermC.num_str @{thm root_ge0}),

 	       Rule.Thm ("root_add_ge0",TermC.num_str @{thm root_add_ge0}),

 	       Rule.Thm ("root_ge0_1",TermC.num_str @{thm root_ge0_1}),

 	       Rule.Thm ("root_ge0_2",TermC.num_str @{thm root_ge0_2}),

 	       Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),

 	       Rule.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),

 	       Rule.Calc ("Tools.matches", Tools.eval_matches ""),

 	       Rule.Calc ("Test.contains'_root",

 		     eval_contains_root"#contains_root_"),

 	       Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),

 	       Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),

 	       Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),

 	       Rule.Calc ("Atools.pow" ,eval_binop "#power_"),

 	       Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

 	       Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

 	       Rule.Calc ("Atools.ident",eval_ident "#ident_")],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

       };      

 \<close>

 setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close>

 ML \<open>

 (*make () dissappear*)   

 val rearrange_assoc =

   Rule.Rls{id = "rearrange_assoc", preconds = [], 

       rew_ord = ("e_rew_ord",Rule.e_rew_ord), 

       erls = Rule.e_rls, srls = Rule.e_rls, calc = [], errpatts = [],

       rules = 

       [Rule.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),

        Rule.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

       };      

 val ac_plus_times =

   Rule.Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),

       erls = Rule.e_rls, srls = Rule.e_rls, calc = [], errpatts = [],

       rules = 

       [Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),

        Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),

        Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),

        Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),

        Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),

        Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

       };      

 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)

 val norm_equation =

   Rule.Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),

       erls = tval_rls, srls = Rule.e_rls, calc = [], errpatts = [],

       rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})

 	       ],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

       };      

 \<close>

 ML \<open>

 (* expects * distributed over + *)

 val Test_simplify =

   Rule.Rls{id = "Test_simplify", preconds = [], 

       rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),

       erls = tval_rls, srls = Rule.e_rls, 

       calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],

       rules = [

 	       Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),

 	       Rule.Thm ("radd_mult_distrib2",TermC.num_str @{thm radd_mult_distrib2}),

 	       Rule.Thm ("rdistr_right_assoc",TermC.num_str @{thm rdistr_right_assoc}),

 	       Rule.Thm ("rdistr_right_assoc_p",TermC.num_str @{thm rdistr_right_assoc_p}),

 	       Rule.Thm ("rdistr_div_right",TermC.num_str @{thm rdistr_div_right}),

 	       Rule.Thm ("rbinom_power_2",TermC.num_str @{thm rbinom_power_2}),	       

                Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}), 

 	       Rule.Thm ("radd_left_commute",TermC.num_str @{thm radd_left_commute}),

 	       Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),

 	       Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),

 	       Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),

 	       Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc}),

 	       Rule.Thm ("radd_real_const_eq",TermC.num_str @{thm radd_real_const_eq}),

 	       Rule.Thm ("radd_real_const",TermC.num_str @{thm radd_real_const}),

 	       (* these 2 rules are invers to distr_div_right wrt. termination.

 		  thus they MUST be done IMMEDIATELY before calc *)

 	       Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

 	       Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),

 	       Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),

 	       Rule.Calc ("Atools.pow", eval_binop "#power_"),

 	       Rule.Thm ("rcollect_right",TermC.num_str @{thm rcollect_right}),

 	       Rule.Thm ("rcollect_one_left",TermC.num_str @{thm rcollect_one_left}),

 	       Rule.Thm ("rcollect_one_left_assoc",TermC.num_str @{thm rcollect_one_left_assoc}),

 	       Rule.Thm ("rcollect_one_left_assoc_p",TermC.num_str @{thm rcollect_one_left_assoc_p}),

 	       Rule.Thm ("rshift_nominator",TermC.num_str @{thm rshift_nominator}),

 	       Rule.Thm ("rcancel_den",TermC.num_str @{thm rcancel_den}),

 	       Rule.Thm ("rroot_square_inv",TermC.num_str @{thm rroot_square_inv}),

 	       Rule.Thm ("rroot_times_root",TermC.num_str @{thm rroot_times_root}),

 	       Rule.Thm ("rroot_times_root_assoc_p",TermC.num_str @{thm rroot_times_root_assoc_p}),

 	       Rule.Thm ("rsqare",TermC.num_str @{thm rsqare}),

 	       Rule.Thm ("power_1",TermC.num_str @{thm power_1}),

 	       Rule.Thm ("rtwo_of_the_same",TermC.num_str @{thm rtwo_of_the_same}),

 	       Rule.Thm ("rtwo_of_the_same_assoc_p",TermC.num_str @{thm rtwo_of_the_same_assoc_p}),

 	       Rule.Thm ("rmult_1",TermC.num_str @{thm rmult_1}),

 	       Rule.Thm ("rmult_1_right",TermC.num_str @{thm rmult_1_right}),

 	       Rule.Thm ("rmult_0",TermC.num_str @{thm rmult_0}),

 	       Rule.Thm ("rmult_0_right",TermC.num_str @{thm rmult_0_right}),

 	       Rule.Thm ("radd_0",TermC.num_str @{thm radd_0}),

 	       Rule.Thm ("radd_0_right",TermC.num_str @{thm radd_0_right})

 	       ],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

 		    (*since 040209 filled by prep_rls': STest_simplify*)

       };      

 \<close>

 ML \<open>

 (*isolate the root in a root-equation*)

 val isolate_root =

   Rule.Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord), 

       erls=tval_rls,srls = Rule.e_rls, calc=[], errpatts = [],

       rules = [Rule.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),

 	       Rule.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),

 	       Rule.Thm ("rroot_to_lhs_add_mult",TermC.num_str @{thm rroot_to_lhs_add_mult}),

 	       Rule.Thm ("risolate_root_add",TermC.num_str @{thm risolate_root_add}),

 	       Rule.Thm ("risolate_root_mult",TermC.num_str @{thm risolate_root_mult}),

 	       Rule.Thm ("risolate_root_div",TermC.num_str @{thm risolate_root_div})       ],

       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) 

       "empty_script")

       };

 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)

 val isolate_bdv =

     Rule.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),

 	erls=tval_rls,srls = Rule.e_rls, calc= [], errpatts = [],

 	rules = 

 	[Rule.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),

 	 Rule.Thm ("risolate_bdv_mult_add",TermC.num_str @{thm risolate_bdv_mult_add}),

 	 Rule.Thm ("risolate_bdv_mult",TermC.num_str @{thm risolate_bdv_mult}),

 	 Rule.Thm ("mult_square",TermC.num_str @{thm mult_square}),

 	 Rule.Thm ("constant_square",TermC.num_str @{thm constant_square}),

 	 Rule.Thm ("constant_mult_square",TermC.num_str @{thm constant_mult_square})

 	 ],

 	scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) 

 			  "empty_script")

 	};      

 \<close>

 ML \<open>val prep_rls' = LTool.prep_rls @{theory};\<close>

 setup \<open>KEStore_Elems.add_rlss 

   [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), 

   ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), 

   ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), 

   ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), 

   ("matches", (Context.theory_name @{theory}, prep_rls'

     (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches", Tools.eval_matches "#matches_")])))]

 \<close>

 subsection \<open>problems\<close>

 (** problem types **)

 setup \<open>KEStore_Elems.add_pbts

   [(Specify.prep_pbt thy "pbl_test" [] Celem.e_pblID (["test"], [], Rule.e_rls, NONE, [])),

     (Specify.prep_pbt thy "pbl_test_equ" [] Celem.e_pblID

       (["equation","test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

            ("#Where" ,["matches (?a = ?b) e_e"]),

            ("#Find"  ,["solutions v_v'i'"])],

         assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_uni" [] Celem.e_pblID

       (["univariate","equation","test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

            ("#Where" ,["matches (?a = ?b) e_e"]),

            ("#Find"  ,["solutions v_v'i'"])],

         assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_uni_lin" [] Celem.e_pblID

       (["LINEAR","univariate","equation","test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

            ("#Where" ,["(matches (   v_v = 0) e_e) | (matches (   ?b*v_v = 0) e_e) |" ^

              "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)  "]),

            ("#Find"  ,["solutions v_v'i'"])],

         assoc_rls' @{theory} "matches", 

         SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))]

 \<close>

 ML \<open>

 Rule.rew_ord' := overwritel (! Rule.rew_ord',

 [("termlessI", termlessI),

  ("ord_make_polytest", ord_make_polytest false thy)

  ]);

 val make_polytest =

   Rule.Rls{id = "make_polytest", preconds = []:term list, 

       rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),

       erls = testerls, srls = Rule.Erls,

       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 

 	      ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),

 	      ("POWER", ("Atools.pow", eval_binop "#power_"))

 	      ], errpatts = [],

       rules = [Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),

 	       (*"a - b = a + (-1) * b"*)

 	       Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),

 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

 	       Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),

 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

 	       Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),

 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

 	       Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),

 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

 	       Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),                 

 	       (*"1 * z = z"*)

 	       Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),        

 	       (*"0 * z = 0"*)

 	       Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),

 	       (*"0 + z = z"*)

 	       (*AC-rewriting*)

 	       Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),

 	       (* z * w = w * z *)

 	       Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),

 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

 	       Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),		

 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

 	       Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),	

 	       (*z + w = w + z*)

 	       Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),

 	       (*x + (y + z) = y + (x + z)*)

 	       Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),	               

 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)

 	       Rule.Thm ("sym_realpow_twoI",

                      TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),	

 	       (*"r1 * r1 = r1 ^^^ 2"*)

 	       Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),		

 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

 	       Rule.Thm ("sym_real_mult_2",

                      TermC.num_str (@{thm real_mult_2} RS @{thm sym})),	

 	       (*"z1 + z1 = 2 * z1"*)

 	       Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),	

 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

 	       Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 

 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)

 	       Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),

 	       (*"[| l is_const; m is_const |] ==>  

 				l * n + (m * n + k) =  (l + m) * n + k"*)

 	       Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),	

 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)

 	       Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 

 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

 	       Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

 	       Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),

 	       Rule.Calc ("Atools.pow", eval_binop "#power_")

 	       ],

       scr = Rule.EmptyScr(*Rule.Prog ((Thm.term_of o the o (parse thy)) 

       scr_make_polytest)*)

       }; 

 val expand_binomtest =

   Rule.Rls{id = "expand_binomtest", preconds = [], 

       rew_ord = ("termlessI",termlessI),

       erls = testerls, srls = Rule.Erls,

       calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")), 

 	      ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),

 	      ("POWER", ("Atools.pow", eval_binop "#power_"))

 	      ], errpatts = [],

       rules = 

       [Rule.Thm ("real_plus_binom_pow2"  ,TermC.num_str @{thm real_plus_binom_pow2}),     

 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)

        Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),    

 	      (*"(a + b)*(a + b) = ...*)

        Rule.Thm ("real_minus_binom_pow2" ,TermC.num_str @{thm real_minus_binom_pow2}),   

        (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)

        Rule.Thm ("real_minus_binom_times",TermC.num_str @{thm real_minus_binom_times}),   

        (*"(a - b)*(a - b) = ...*)

        Rule.Thm ("real_plus_minus_binom1",TermC.num_str @{thm real_plus_minus_binom1}),   

         (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)

        Rule.Thm ("real_plus_minus_binom2",TermC.num_str @{thm real_plus_minus_binom2}),   

         (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)

        (*RL 020915*)

        Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}), 

         (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)

        Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}), 

         (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)

        Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}), 

         (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)

        Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}), 

         (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)

        Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),                

         (*(a*b)^^^n = a^^^n * b^^^n*)

        Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),

         (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)

        Rule.Thm ("real_minus_binom_pow3",TermC.num_str @{thm real_minus_binom_pow3}),

         (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)

      (*  Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),	

 	 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

 	Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),	

 	(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

 	Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),	

 	(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

 	Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),	

 	(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

 	*)

 	Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),              

          (*"1 * z = z"*)

 	Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),              

          (*"0 * z = 0"*)

 	Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),

          (*"0 + z = z"*)

 	Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

 	Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),

 	Rule.Calc ("Atools.pow", eval_binop "#power_"),

         (*	       

 	 Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),		

         (*AC-rewriting*)

 	Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),

 	Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),

 	Rule.Thm ("add_commute",TermC.num_str @{thm add_commute}),	

 	Rule.Thm ("add_left_commute",TermC.num_str @{thm add_left_commute}),

 	Rule.Thm ("add_assoc",TermC.num_str @{thm add_assoc}),

 	*)

 	Rule.Thm ("sym_realpow_twoI",

               TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),

 	(*"r1 * r1 = r1 ^^^ 2"*)

 	Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),			

 	(*"r * r ^^^ n = r ^^^ (n + 1)"*)

 	(*Rule.Thm ("sym_real_mult_2",

                 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),

 	(*"z1 + z1 = 2 * z1"*)*)

 	Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),		

 	(*"z1 + (z1 + k) = 2 * z1 + k"*)

 	Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}), 

 	(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)

 	Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),	

 	(*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)

 	Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),		

 	(*"m is_const ==> n + m * n = (1 + m) * n"*)

 	Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}), 

 	(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

 	Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 

 	Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),

 	Rule.Calc ("Atools.pow", eval_binop "#power_")

 	],

       scr = Rule.EmptyScr

 (*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)

       };      

 \<close>

 setup \<open>KEStore_Elems.add_rlss 

   [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)), 

   ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\<close>

 setup \<open>KEStore_Elems.add_rlss 

   [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)), 

   ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)), 

   ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\<close>

 section \<open>problems\<close>

 setup \<open>KEStore_Elems.add_pbts

   [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Celem.e_pblID

     (["plain_square","univariate","equation","test"],

       [("#Given" ,["equality e_e","solveFor v_v"]),

         ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^

 	        "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^

 	        "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^

 	        "(matches (        v_v ^^^2 = 0) e_e)"]),

         ("#Find"  ,["solutions v_v'i'"])],

       assoc_rls' @{theory} "matches", 

       SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])),

     (Specify.prep_pbt thy "pbl_test_uni_poly" [] Celem.e_pblID

       (["polynomial","univariate","equation","test"],

         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),

           ("#Where" ,["HOL.False"]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.e_rls, SOME "solve (e_e::bool, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Celem.e_pblID

       (["degree_two","polynomial","univariate","equation","test"],

         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Celem.e_pblID

       (["pq_formula","degree_two","polynomial","univariate","equation","test"],

         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Celem.e_pblID

       (["abc_formula","degree_two","polynomial","univariate","equation","test"],

         [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_uni_root" [] Celem.e_pblID

       (["squareroot","univariate","equation","test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["precond_rootpbl v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.append_rls "contains_root" Rule.e_rls [Rule.Calc ("Test.contains'_root",

             eval_contains_root "#contains_root_")], 

         SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),

     (Specify.prep_pbt thy "pbl_test_uni_norm" [] Celem.e_pblID

       (["normalise","univariate","equation","test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,[]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),

     (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Celem.e_pblID

       (["sqroot-test","univariate","equation","test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["precond_rootpbl v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         Rule.e_rls, SOME "solve (e_e::bool, v_v)", [])),

     (Specify.prep_pbt thy "pbl_test_intsimp" [] Celem.e_pblID

       (["inttype","test"],

         [("#Given" ,["intTestGiven t_t"]),

           ("#Where" ,[]),

           ("#Find"  ,["intTestFind s_s"])],

       Rule.e_rls, NONE, [["Test","intsimp"]]))]\<close>

 section \<open>methods\<close>

 subsection \<open>differentiate\<close>

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID

       (["Test"], [],

         {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,

           crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")]

 \<close>

 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where

 "solve_linear e_e v_v =

   (let e_e =

     Repeat

       (((Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@

         (Rewrite_Set ''Test_simplify'' False))) e_e

    in [e_e])"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID

       (["Test","solve_linear"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["matches (?a = ?b) e_e"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,

           prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],

           nrls = Test_simplify},

         "Script Solve_linear (e_e::bool) (v_v::real)=                     " ^

           "(let e_e =                                                       " ^

           "  Repeat                                                         " ^

           "    (((Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@  " ^

           "      (Rewrite_Set ''Test_simplify'' False))) e_e" ^

           " in [e_e::bool])")]

 \<close>

 subsection \<open>root equation\<close>

 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where

 "solve_root_equ e_e v_v =

   (let e_e =

      ((While (contains_root e_e) Do

         ((Rewrite ''square_equation_left'' True) @@

          (Try (Rewrite_Set ''Test_simplify'' False)) @@

          (Try (Rewrite_Set ''rearrange_assoc'' False)) @@

          (Try (Rewrite_Set ''isolate_root'' False)) @@

          (Try (Rewrite_Set ''Test_simplify'' False)))) @@

       (Try (Rewrite_Set ''norm_equation'' False)) @@

       (Try (Rewrite_Set ''Test_simplify'' False)) @@

       (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@

       (Try (Rewrite_Set ''Test_simplify'' False))) e_e                                                                

    in [e_e])"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy  "met_test_sqrt" [] Celem.e_metID

       (*root-equation, version for tests before 8.01.01*)

       (["Test","sqrt-equ-test"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["contains_root (e_e::bool)"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,

           srls = Rule.append_rls "srls_contains_root" Rule.e_rls

               [Rule.Calc ("Test.contains'_root",eval_contains_root "")],

           prls = Rule.append_rls "prls_contains_root" Rule.e_rls 

               [Rule.Calc ("Test.contains'_root",eval_contains_root "")],

           calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],

           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},

         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^

           "(let e_e = " ^

           "   ((While (contains_root e_e) Do" ^

           "      ((Rewrite ''square_equation_left'' True) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

           "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^

           "       (Try (Rewrite_Set ''isolate_root'' False)) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^

           "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^

           "    (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

           "    (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^

           "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^

           "   e_e" ^

           " in [e_e::bool])")]

 \<close>

 (* UNUSED?

 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where "solve_root_equ e_e v_v =                   

 (let e_e =                                                           

    ((While (contains_root e_e) Do                                    

       ((Rewrite ''square_equation_left'' True) @@                    

        (Try (Rewrite_Set ''Test_simplify'' False)) @@                

        (Try (Rewrite_Set ''rearrange_assoc'' False)) @@              

        (Try (Rewrite_Set ''isolate_root'' False)) @@                 

        (Try (Rewrite_Set ''Test_simplify'' False)))) @@              

     (Try (Rewrite_Set ''norm_equation'' False)) @@                   

     (Try (Rewrite_Set ''Test_simplify'' False)) @@                   

     (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@

     (Try (Rewrite_Set ''Test_simplify'' False)))                     

    e_e;                                                              

   (L_L::bool list) = Tac ''subproblem_equation_dummy'';                  

   L_L = Tac ''solve_equation_dummy''                                     

   in Check_elementwise L_L {(v_v::real). Assumptions})               "

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy  "met_test_sqrt2" [] Celem.e_metID

       (*root-equation ... for test-*.sml until 8.01*)

       (["Test","squ-equ-test2"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,

           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 

               [Rule.Calc ("Test.contains'_root",eval_contains_root"")],

           prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],

           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},

         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^

           "(let e_e = " ^

           "   ((While (contains_root e_e) Do" ^

           "      ((Rewrite ''square_equation_left'' True) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

           "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^

           "       (Try (Rewrite_Set ''isolate_root'' False)) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^

           "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^

           "    (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

           "    (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^

           "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^

           "   e_e;" ^

           "  (L_L::bool list) = Tac subproblem_equation_dummy;          " ^

           "  L_L = Tac solve_equation_dummy                             " ^

           "  in Check_elementwise L_L {(v_v::real). Assumptions})")]

 \<close>

 *)

 partial_function (tailrec) solve_root_equation ::

   "bool \<Rightarrow> real \<Rightarrow> bool list"

 where "minisubpbl e_e v_v =

   (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@

               (Try (Rewrite_Set ''Test_simplify'' False))) e_e;

       (L_L::bool list) =

              SubProblem (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],

                  [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]

    in Check_elementwise L_L {(v_v::real). Assumptions})"

 (* ^^^used for test/../Minisubpbl/

 # difference between partial_function above and Script below:

 "Solve_root_equation" is a constant, which is NOT accepted by partial_function

 # differences between original "Solve_root_equation" and the version below:

 (1) the program name, see note above

 (2) the first argument of SubProblem: ''Test''' is NOT accepted by partial_function,

     thus previous change-set Test' \<longrightarrow> TestX

 ''Test'#TODO#''. Note: this change is NOT recognised by Interpret!

 *)

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID

       (*tests subproblem fixed linear*)

       (["Test","squ-equ-test-subpbl1"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["precond_rootmet v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,

           prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls

               [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],

           calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},

         "Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^

         " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@               " ^

         "             (Try (Rewrite_Set ''Test_simplify'' False))) e_e;            " ^

         "     (L_L::bool list) =                                               " ^

         "            (SubProblem (''Test'',                                    " ^

         "                [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^

         "                [''Test'', ''solve_linear''])                         " ^

         "              [BOOL e_e, REAL v_v])                                   " ^

         "  in Check_elementwise L_L {(v_v::real). Assumptions})                ")]

 \<close>

 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where "solve_root_equ e_e v_v =

 (let e_e =

       ((While (contains_root e_e) Do

          ((Rewrite ''square_equation_left'' True) @@

           (Try (Rewrite_Set ''Test_simplify'' False)) @@

           (Try (Rewrite_Set ''rearrange_assoc'' False)) @@

           (Try (Rewrite_Set ''isolate_root'' False)) @@

           (Try (Rewrite_Set ''Test_simplify'' False)))) @@

        (Try (Rewrite_Set ''norm_equation'' False)) @@

        (Try (Rewrite_Set ''Test_simplify'' False))) e_e;

      L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],

              [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]

   in Check_elementwise L_L {(v_v::real). Assumptions})                                       "

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy  "met_test_eq1" [] Celem.e_metID

       (*root-equation1:*)

       (["Test","square_equation1"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,

           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 

             [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls,

               errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),

               ("square_equation_right","")]*)},

         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^

           "(let e_e = " ^

           "   ((While (contains_root e_e) Do" ^

           "      ((Rewrite ''square_equation_left'' True) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

           "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^

           "       (Try (Rewrite_Set ''isolate_root'' False)) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^

           "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^

           "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^

           "   e_e;" ^

           "  (L_L::bool list) = (SubProblem (''Test'',[''LINEAR'',''univariate'',''equation'',''test'']," ^

           "                    [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^

           "  in Check_elementwise L_L {(v_v::real). Assumptions})")]

 \<close>

 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where

 "solve_root_equ e_e v_v =

   (let e_e =

         ((While (contains_root e_e) Do

            (((Rewrite ''square_equation_left'' True) Or

              (Rewrite ''square_equation_right'' True)) @@

             (Try (Rewrite_Set ''Test_simplify'' False)) @@

             (Try (Rewrite_Set ''rearrange_assoc'' False)) @@

             (Try (Rewrite_Set ''isolate_root'' False)) @@

             (Try (Rewrite_Set ''Test_simplify'' False)))) @@

          (Try (Rewrite_Set ''norm_equation'' False)) @@

          (Try (Rewrite_Set ''Test_simplify'' False))) e_e;

        L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],

                [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]

     in Check_elementwise L_L {(v_v::real). Assumptions})"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID

       (*root-equation2*)

         (["Test","square_equation2"],

           [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,

           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 

               [Rule.Calc ("Test.contains'_root",eval_contains_root"")],

           prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],

           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},

         "Script Solve_root_equation (e_e::bool) (v_v::real)  =  " ^

         "(let e_e = " ^

         "   ((While (contains_root e_e) Do" ^

         "      (((Rewrite ''square_equation_left'' True) Or " ^

         "        (Rewrite ''square_equation_right'' True)) @@" ^

         "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

         "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^

         "       (Try (Rewrite_Set ''isolate_root'' False)) @@" ^

         "       (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^

         "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^

         "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^

         "   e_e;" ^

         "  (L_L::bool list) = (SubProblem (''Test'',[''plain_square'',''univariate'',''equation'',''test'']," ^

         "                    [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^

         "  in Check_elementwise L_L {(v_v::real). Assumptions})")]

 \<close>

 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where

 "solve_root_equ e_e v_v =

 (let e_e =

       ((While (contains_root e_e) Do

          (((Rewrite ''square_equation_left'' True) Or

            (Rewrite ''square_equation_right'' True)) @@

           (Try (Rewrite_Set ''Test_simplify'' False)) @@

           (Try (Rewrite_Set ''rearrange_assoc'' False)) @@

           (Try (Rewrite_Set ''isolate_root'' False)) @@

           (Try (Rewrite_Set ''Test_simplify'' False)))) @@

        (Try (Rewrite_Set ''norm_equation'' False)) @@

        (Try (Rewrite_Set ''Test_simplify'' False))) e_e;

      L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],

              [''no_met'']) [BOOL e_e, REAL v_v]

   in Check_elementwise L_L {(v_v::real). Assumptions})"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID

       (*root-equation*)

       (["Test","square_equation"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,

           srls = Rule.append_rls "srls_contains_root" Rule.e_rls 

               [Rule.Calc ("Test.contains'_root",eval_contains_root"")],

           prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],

           asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},

         "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^

           "(let e_e = " ^

           "   ((While (contains_root e_e) Do" ^

           "      (((Rewrite ''square_equation_left'' True) Or" ^

           "        (Rewrite ''square_equation_right'' True)) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^

           "       (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^

           "       (Try (Rewrite_Set ''isolate_root'' False)) @@" ^

           "       (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^

           "    (Try (Rewrite_Set ''norm_equation'' False)) @@" ^

           "    (Try (Rewrite_Set ''Test_simplify'' False)))" ^

           "   e_e;" ^

           "  (L_L::bool list) = (SubProblem (''Test'',[''univariate'',''equation'',''test'']," ^

           "                    [''no_met'']) [BOOL e_e, REAL v_v])" ^

           "  in Check_elementwise L_L {(v_v::real). Assumptions})")]

 \<close>

 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where

 "solve_plain_square e_e v_v =         

  (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@

              (Try (Rewrite_Set ''Test_simplify'' False))    @@

              ((Rewrite ''square_equality_0'' False) Or

               (Rewrite ''square_equality'' True)) @@

              (Try (Rewrite_Set ''tval_rls'' False))) e_e

   in Or_to_List e_e)"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID

       (*solve_plain_square*)

       (["Test","solve_plain_square"],

         [("#Given",["equality e_e","solveFor v_v"]),

           ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^

               "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^

               "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^

               "(matches (        v_v ^^^2 = 0) e_e)"]), 

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls,

           prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,

           asm_rls=[],asm_thm=[]*)},

         "Script Solve_plain_square (e_e::bool) (v_v::real) =           " ^

           " (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@         " ^

           "            (Try (Rewrite_Set ''Test_simplify'' False)) @@     " ^

           "            ((Rewrite ''square_equality_0'' False) Or        " ^

           "             (Rewrite ''square_equality'' True)) @@            " ^

           "            (Try (Rewrite_Set ''tval_rls'' False))) e_e             " ^

           "  in ((Or_to_List e_e)::bool list))")]

 \<close>

 subsection \<open>polynomial equation\<close>

 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"

   where

 "norm_univariate_equ e_e v_v =

  (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@

              (Try (Rewrite_Set ''Test_simplify'' False))) e_e

   in SubProblem (''Test'', [''univariate'', ''equation'', ''test''],

         [''no_met'']) [BOOL e_e, REAL v_v])"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID

       (["Test","norm_univar_equation"],

         [("#Given",["equality e_e","solveFor v_v"]),

           ("#Where" ,[]), 

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,

           errpats = [], nrls = Rule.e_rls},

         "Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^

           " (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@   " ^

           "            (Try (Rewrite_Set ''Test_simplify'' False))) e_e   " ^

           "  in (SubProblem (''Test'',[''univariate'',''equation'',''test''],         " ^

           "                    [''no_met'']) [BOOL e_e, REAL v_v]))")]

 \<close>

 subsection \<open>diophantine equation\<close>

 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"

   where

 "test_simplify t_t =           

   (Repeat                                    

       ((Try (Calculate ''PLUS'')) @@         

        (Try (Calculate ''TIMES''))) t_t)"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID

       (["Test","intsimp"],

         [("#Given" ,["intTestGiven t_t"]),

           ("#Where" ,[]),

           ("#Find"  ,["intTestFind s_s"])],

         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,  prls = Rule.e_rls, calc = [],

           crls = tval_rls, errpats = [], nrls = Test_simplify},

         "Script STest_simplify (t_t::int) =                  " ^

           "(Repeat                                                          " ^

           "    ((Try (Calculate ''PLUS'')) @@  " ^

           "     (Try (Calculate ''TIMES''))) t_t::int)")]

 \<close>

 end