(* some tests are based on specficially simple scripts etc.

    Author: Walther Neuper 2003

    (c) due to copyright terms

 *) 

 theory Test imports Atools + Rational + Root + Poly + 

 consts

 (*"cancel":: [real, real] => real    (infixl "'/'/'/" 70) ...divide 2002*)

   Expand'_binomtest

              :: "['y,  

 		    'y] => 'y"

                ("((Script Expand'_binomtest (_ =))//  

                    (_))" 9)

   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)

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

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

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

   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)

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

 axioms (*TODO: prove as theorems*)

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

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

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

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

   rcollect_right:

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

   rcollect_one_left:

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

   rcollect_one_left_assoc:

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

   rcollect_one_left_assoc_p:

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

   rtwo_of_the_same:        "a + a = 2 * a"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   radd_real_const_eq:

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

   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))"  

 (*for AC-operators*)

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

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

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

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

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

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

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

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

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

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

   rnorm_equation_add:

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

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

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

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

   root_add_ge0:

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

   root_ge0_1:

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

   root_ge0_2:

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

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

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

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

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

 (*for root-equations*)

   square_equation_left:

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

   square_equation_right:

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

   (*causes frequently non-termination:*)

   square_equation:  

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

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

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

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

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

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

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

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

   square_equality: 

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

   square_equality_0:

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

 (*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)"

   rroot_to_lhs_mult:

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

   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------------------------------^^^---*)  

 ML {*

 val thy = @{theory};

 (** evaluation of numerals and predicates **)

 (*does a term contain a root ?*)

 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy = 

   if strip_thy op0 <> "is'_root'_free" 

     then raise error ("eval_root_free: wrong "^op0)

   else if const_in (strip_thy op0) arg

 	 then SOME (mk_thmid thmid "" 

 		    ((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

 		    Trueprop $ (mk_equality (t, false_as_term)))

        else SOME (mk_thmid thmid "" 

 		  ((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

 		  Trueprop $ (mk_equality (t, true_as_term)))

   | eval_root_free _ _ _ _ = NONE; 

 (*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 (mk_thmid thmid "" 

 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

 	       Trueprop $ (mk_equality (t, true_as_term)))

     else SOME (mk_thmid thmid "" 

 			((Syntax.string_of_term (thy2ctxt thy)) arg) "", 

 	       Trueprop $ (mk_equality (t, false_as_term)))

   | eval_contains_root _ _ _ _ = NONE; 

 calclist':= overwritel (!calclist', 

    [("is_root_free", ("Test.is'_root'_free", 

 		      eval_root_free"#is_root_free_e")),

     ("contains_root", ("Test.contains'_root",

 		       eval_contains_root"#contains_root_"))

     ]);

 (** term order **)

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

 (** rule sets GOON **)

 val testerls = 

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

       erls = e_rls, srls = Erls, 

       calc = [], 

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

 	       Thm ("real_le_refl",num_str @{thm real_le_refl}),

 	       Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),

 	       Thm ("not_true",num_str @{thm not_true}),

 	       Thm ("not_false",num_str @{thm not_false}),

 	       Thm ("and_true",num_str @{thm and_true}),

 	       Thm ("and_false",num_str @{thm and_false}),

 	       Thm ("or_true",num_str @{thm or_true}),

 	       Thm ("or_false",num_str @{thm or_false}),

 	       Thm ("and_commute",num_str @{thm and_commute}),

 	       Thm ("or_commute",num_str @{thm or_commute}),

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

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

 	       Calc ("op +",eval_binop "#add_"),

 	       Calc ("op *",eval_binop "#mult_"),

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

 	       Calc ("op <",eval_equ "#less_"),

 	       Calc ("op <=",eval_equ "#less_equal_"),

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

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

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

 (*FIXXXXXXME 10.8.02: handle like _simplify*)

 val tval_rls =  

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

       rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")), 

       erls=testerls,srls = e_rls, 

       calc=[],

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

 	       Thm ("real_le_refl",num_str @{thm real_le_refl}),

 	       Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),

 	       Thm ("not_true",num_str @{thm not_true}),

 	       Thm ("not_false",num_str @{thm not_false}),

 	       Thm ("and_true",num_str @{thm and_true}),

 	       Thm ("and_false",num_str @{thm and_false}),

 	       Thm ("or_true",num_str @{thm or_true}),

 	       Thm ("or_false",num_str @{thm or_false}),

 	       Thm ("and_commute",num_str @{thm and_commute}),

 	       Thm ("or_commute",num_str @{or_commute}),

 	       Thm ("real_diff_minus",num_str @{thm real_diff_minus}),

 	       Thm ("root_ge0",num_str @{thm root_ge0}),

 	       Thm ("root_add_ge0",num_str @{thm root_add_ge0}),

 	       Thm ("root_ge0_1",num_str @{thm root_ge0_1}),

 	       Thm ("root_ge0_2",num_str @{thm root_ge0_2}),

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

 	       Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_e"),

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

 	       Calc ("Test.contains'_root",

 		     eval_contains_root"#contains_root_"),

 	       Calc ("op +",eval_binop "#add_"),

 	       Calc ("op *",eval_binop "#mult_"),

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

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

 	       Calc ("op <",eval_equ "#less_"),

 	       Calc ("op <=",eval_equ "#less_equal_"),

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

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

 ruleset' := overwritelthy @{theory} (!ruleset',

   [("testerls", prep_rls testerls)

    ]);

 (*make () dissappear*)   

 val rearrange_assoc =

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

       rew_ord = ("e_rew_ord",e_rew_ord), 

       erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

       rules = 

       [Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),

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

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

 val ac_plus_times =

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

       erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

       rules = 

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

        Thm ("radd_left_commute",num_str @{thm radd_left_commute}),

        Thm ("add_assoc",num_str @{thm add_assoc}),

        Thm ("rmult_commute",num_str @{thm rmult_commute}),

        Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),

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

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

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

 val norm_equation =

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

       erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

       rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add)

 	       ],

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

 (** rule sets **)

 val STest_simplify =     (*   vv--- not changed to real by parse*)

   "Script STest_simplify (t_::'z) =                           " ^

   "(Repeat" ^

   "    ((Try (Repeat (Rewrite real_diff_minus False))) @@        " ^

   "     (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@  " ^

   "     (Try (Repeat (Rewrite rdistr_right_assoc False))) @@  " ^

   "     (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@" ^

   "     (Try (Repeat (Rewrite rdistr_div_right False))) @@    " ^

   "     (Try (Repeat (Rewrite rbinom_power_2 False))) @@      " ^

   "     (Try (Repeat (Rewrite radd_commute False))) @@        " ^

   "     (Try (Repeat (Rewrite radd_left_commute False))) @@   " ^

   "     (Try (Repeat (Rewrite add_assoc False))) @@          " ^

   "     (Try (Repeat (Rewrite rmult_commute False))) @@       " ^

   "     (Try (Repeat (Rewrite rmult_left_commute False))) @@  " ^

   "     (Try (Repeat (Rewrite rmult_assoc False))) @@         " ^

   "     (Try (Repeat (Rewrite radd_real_const_eq False))) @@   " ^

   "     (Try (Repeat (Rewrite radd_real_const False))) @@   " ^

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

   "     (Try (Repeat (Calculate TIMES))) @@   " ^

   "     (Try (Repeat (Calculate divide_))) @@" ^

   "     (Try (Repeat (Calculate POWER))) @@  " ^

   "     (Try (Repeat (Rewrite rcollect_right False))) @@   " ^

   "     (Try (Repeat (Rewrite rcollect_one_left False))) @@   " ^

   "     (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@   " ^

   "     (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@   " ^

   "     (Try (Repeat (Rewrite rshift_nominator False))) @@   " ^

   "     (Try (Repeat (Rewrite rcancel_den False))) @@   " ^

   "     (Try (Repeat (Rewrite rroot_square_inv False))) @@   " ^

   "     (Try (Repeat (Rewrite rroot_times_root False))) @@   " ^

   "     (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@   " ^

   "     (Try (Repeat (Rewrite rsqare False))) @@   " ^

   "     (Try (Repeat (Rewrite power_1 False))) @@   " ^

   "     (Try (Repeat (Rewrite rtwo_of_the_same False))) @@   " ^

   "     (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@   " ^

   "     (Try (Repeat (Rewrite rmult_1 False))) @@   " ^

   "     (Try (Repeat (Rewrite rmult_1_right False))) @@   " ^

   "     (Try (Repeat (Rewrite rmult_0 False))) @@   " ^

   "     (Try (Repeat (Rewrite rmult_0_right False))) @@   " ^

   "     (Try (Repeat (Rewrite radd_0 False))) @@   " ^

   "     (Try (Repeat (Rewrite radd_0_right False)))) " ^

   " t_)";

 (* expects * distributed over + *)

 val Test_simplify =

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

       rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),

       erls = tval_rls, srls = e_rls, 

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

       (*asm_thm = [],*)

       rules = [

 	       Thm ("real_diff_minus",num_str @{thm real_diff_minus}),

 	       Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}),

 	       Thm ("rdistr_right_assoc",num_str @{thm rdistr_right_assoc}),

 	       Thm ("rdistr_right_assoc_p",num_str @{thm rdistr_right_assoc_p}),

 	       Thm ("rdistr_div_right",num_str @{thm rdistr_div_right}),

 	       Thm ("rbinom_power_2",num_str @{thm rbinom_power_2}),	       

                Thm ("radd_commute",num_str @{thm radd_commute}), 

 	       Thm ("radd_left_commute",num_str @{thm radd_left_commute}),

 	       Thm ("add_assoc",num_str @{thm add_assoc}),

 	       Thm ("rmult_commute",num_str @{thm rmult_commute}),

 	       Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),

 	       Thm ("rmult_assoc",num_str @{thm rmult_assoc}),

 	       Thm ("radd_real_const_eq",num_str @{thm radd_real_const_eq}),

 	       Thm ("radd_real_const",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 *)

 	       Calc ("op +", eval_binop "#add_"), 

 	       Calc ("op *", eval_binop "#mult_"),

 	       Calc ("HOL.divide", eval_cancel "#divide_e"),

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

 	       Thm ("rcollect_right",num_str @{thm rcollect_right}),

 	       Thm ("rcollect_one_left",num_str @{thm rcollect_one_left}),

 	       Thm ("rcollect_one_left_assoc",num_str @{thm rcollect_one_left_assoc}),

 	       Thm ("rcollect_one_left_assoc_p",num_str @{thm rcollect_one_left_assoc_p}),

 	       Thm ("rshift_nominator",num_str @{thm rshift_nominator}),

 	       Thm ("rcancel_den",num_str @{thm rcancel_den}),

 	       Thm ("rroot_square_inv",num_str @{thm rroot_square_inv}),

 	       Thm ("rroot_times_root",num_str @{thm rroot_times_root}),

 	       Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),

 	       Thm ("rsqare",num_str @{thm rsqare}),

 	       Thm ("power_1",num_str @{power_1}),

 	       Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),

 	       Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),

 	       Thm ("rmult_1",num_str @{thm rmult_1}),

 	       Thm ("rmult_1_right",num_str @{thm rmult_1_right}),

 	       Thm ("rmult_0",num_str @{thm rmult_0}),

 	       Thm ("rmult_0_right",num_str @{thm rmult_0_right}),

 	       Thm ("radd_0",num_str @{thm radd_0}),

 	       Thm ("radd_0_right",num_str @{thm radd_0_right})

 	       ],

       scr = Script ((term_of o the o (parse thy)) "empty_script")

 		    (*since 040209 filled by prep_rls: STest_simplify*)

       }:rls;      

 (** rule sets **)

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

 val isolate_root =

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

       erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)

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

 	       Thm ("rroot_to_lhs_mult",num_str @{thm rroot_to_lhs_mult}),

 	       Thm ("rroot_to_lhs_add_mult",num_str @{thm rroot_to_lhs_add_mult}),

 	       Thm ("risolate_root_add",num_str @{thm risolate_root_add}),

 	       Thm ("risolate_root_mult",num_str @{thm risolate_root_mult}),

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

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;

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

 val isolate_bdv =

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

 	erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)

 	rules = 

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

 	 Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),

 	 Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),

 	 Thm ("mult_square",num_str @{mult_square}),

 	 Thm ("constant_square",num_str @{constant_square}),

 	 Thm ("constant_mult_square",num_str @{constant_mult_square})

 	 ],

 	scr = Script ((term_of o the o (parse thy)) 

 			  "empty_script")

 	}:rls;      

 (* association list for calculate_, calculate

    "op +" etc. not usable in scripts *)

 val calclist = 

     [

      (*as Tools.ML*)

      ("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")),

      ("matches",("Tools.matches",eval_matches "#matches_")),

      ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),

      (*aus Atools.ML*)

      ("PLUS"    ,("op +"        ,eval_binop "#add_")),

      ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

      ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_e")),

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

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

      ("le"      ,("op <"        ,eval_equ "#less_")),

      ("leq"     ,("op <="       ,eval_equ "#less_equal_")),

      ("ident"   ,("Atools.ident",eval_ident "#ident_")),

      (*von hier (ehem.SqRoot*)

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

      ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")),

      ("Test.contains_root",("contains'_root",

 			    eval_contains_root"#contains_root_"))

      ];

 ruleset' := overwritelthy @{theory} (!ruleset',

   [("Test_simplify", prep_rls Test_simplify),

    ("tval_rls", prep_rls tval_rls),

    ("isolate_root", prep_rls isolate_root),

    ("isolate_bdv", prep_rls isolate_bdv),

    ("matches", 

     prep_rls (append_rls "matches" testerls 

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

    ]);

 (** problem types **)

 store_pbt

  (prep_pbt thy "pbl_test" [] e_pblID

  (["test"],

   [],

   e_rls, NONE, []));

 store_pbt

  (prep_pbt thy "pbl_test_equ" [] e_pblID

  (["equation","test"],

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

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

    ("#Find"  ,["solutions v_i"])

   ],

   assoc_rls "matches",

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

 store_pbt

  (prep_pbt thy "pbl_test_uni" [] e_pblID

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

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

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

    ("#Find"  ,["solutions v_i"])

   ],

   assoc_rls "matches",

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

 store_pbt

  (prep_pbt thy "pbl_test_uni_lin" [] e_pblID

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

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

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

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

    ("#Find"  ,["solutions v_i"])

   ],

   assoc_rls "matches", 

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

 (*25.8.01 ------

 store_pbt

  (prep_pbt thy

  (["thy"],

   [("#Given" ,"boolTestGiven g_"),

    ("#Find"  ,"boolTestFind f_")

   ],

   []));

 store_pbt

  (prep_pbt thy

  (["testeq","thy"],

   [("#Given" ,"boolTestGiven g_"),

    ("#Find"  ,"boolTestFind f_")

   ],

   []));

 val ttt = (term_of o the o (parse (theory "Isac"))) "(matches (   v_v = 0) e_e)";

  ------ 25.8.01*)

 (** methods **)

 store_met

  (prep_met (theory "Diff") "met_test" [] e_metID

  (["Test"],

    [],

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

     crls=Atools_erls, nrls=e_rls(*,

     asm_rls=[],asm_thm=[]*)}, "empty_script"));

 (*

 store_met

  (prep_met (theory "Script")

  (e_metID,(*empty method*)

    [],

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

     asm_rls=[],asm_thm=[]},

    "Undef"));*)

 store_met

  (prep_met thy "met_test_solvelin" [] e_metID

  (["Test","solve_linear"]:metID,

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

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

     ("#Find"  ,["solutions v_i"])

     ],

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

     prls=assoc_rls "matches",

     calc=[],

     crls=tval_rls, 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_::bool])"

  )

 (*, prep_met thy (*test for equations*)

  (["Test","testeq"]:metID,

   [("#Given" ,["boolTestGiven g_"]),

    ("#Find"  ,["boolTestFind f_"])

     ],

   {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],

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

  "Script Testeq (eq_::bool) =                                         " ^

    "Repeat                                                            " ^

    " (let e_e = Try (Repeat (Rewrite rroot_square_inv False eq_));      " ^

    "      e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^

    "      e_e = Try (Repeat (Rewrite rmult_0 False e_e))                " ^

    "   in e_e) Until (is_root_free e_e)" (*deleted*)

  )

 , ---------27.4.02*)

 );

 ruleset' := overwritelthy @{theory} (!ruleset',

   [("norm_equation", prep_rls norm_equation),

    ("ac_plus_times", prep_rls ac_plus_times),

    ("rearrange_assoc", prep_rls rearrange_assoc)

    ]);

 fun bin_o (Const (op_,(Type ("fun",

 	   [Type (s2,[]),Type ("fun",

 	    [Type (s4,tl4),Type (s5,tl5)])])))) = 

     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 (op_,(Type ("fun",

 	   [Type (s2,[]),Type ("fun",

 	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = 

     arg1;

 fun bin_op_arg2 ((Const (op_,(Type ("fun",

 	   [Type (s2,[]),Type ("fun",

 	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) = 

     arg2;

 exception NO_EQUATION_TERM;

 fun is_equation ((Const ("op =",(Type ("fun",

 		 [Type (_,[]),Type ("fun",

 		  [Type (_,[]),Type ("bool",[])])])))) $ _ $ _) 

                   = true

   | is_equation _ = false;

 fun equ_lhs ((Const ("op =",(Type ("fun",

 		 [Type (_,[]),Type ("fun",

 		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r) 

               = l

   | equ_lhs _ = raise NO_EQUATION_TERM;

 fun equ_rhs ((Const ("op =",(Type ("fun",

 		 [Type (_,[]),Type ("fun",

 		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r) 

               = r

   | equ_rhs _ = raise NO_EQUATION_TERM;

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

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

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

 (*| atom (_     (_,"?DUMMY"   ))           = true ..ML-error *)

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

   | atom _                                 = false;

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

   | varids (Free   (s,Type (_,[])))         = if is_no 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,t)) = union op = [a] (varids t)

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

   | varids _         = [];

 (*> val t = term_of (hd (parse Diophant.thy "x"));

 val t = Free ("x","?DUMMY") : term

 > varids t;

 val it = [] : string list          [] !!! *)

 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 = (* 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 is =

     let fun max_ m [] = m 

 	  | max_ m (i::is) = if m<i then max_ i is else max_ m is;

     in max_ (hd is) is end;

 > max [1,5,3,7,4,2];

 val it = 7 : int  *)

 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 _ _ v((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)

 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 (s2,[]),Type ("fun",

 	    [Type (s4,tl4),Type (s5,tl5)])])))) )= (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;

 (** problem types **)

 store_pbt

  (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID

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

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

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

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

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

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

    ("#Find"  ,["solutions v_i"])

   ],

   assoc_rls "matches", 

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

 (*

  val e_e = (term_of o the o (parse thy)) "e_::bool";

  val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";

  val env = [(e_,ve)];

  val pre = (term_of o the o (parse thy))

 	      "(matches (a + b*v_ ^^^2 = 0, e_e::bool)) |" ^

 	      "(matches (    b*v_ ^^^2 = 0, e_e::bool)) |" ^

 	      "(matches (a +   v_v ^^^2 = 0, e_e::bool)) |" ^

 	      "(matches (      v_v ^^^2 = 0, e_e::bool))";

  val prei = subst_atomic env pre;

  val cpre = (cterm_of thy) prei;

  val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;

 val ct = "True | False | False | False" : cterm 

 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

 val ct = "True" : cterm

 *)

 store_pbt

  (prep_pbt thy "pbl_test_uni_poly" [] e_pblID

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

   [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),

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

    ("#Find"  ,["solutions v_i"]) 

   ],

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

 store_pbt

  (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID

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

   [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),

    ("#Find"  ,["solutions v_i"]) 

   ],

   e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));

 store_pbt

  (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID

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

   [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),

    ("#Find"  ,["solutions v_i"]) 

   ],

   e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));

 store_pbt

  (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID

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

   [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_v"]),

    ("#Find"  ,["solutions v_i"]) 

   ],

   e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_v)", []));

 store_pbt

  (prep_pbt thy "pbl_test_uni_root" [] e_pblID

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

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

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

    ("#Find"  ,["solutions v_i"]) 

   ],

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

 			  eval_contains_root "#contains_root_")], 

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

 store_pbt

  (prep_pbt thy "pbl_test_uni_norm" [] e_pblID

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

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

    ("#Where" ,[]),

    ("#Find"  ,["solutions v_i"]) 

   ],

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

 store_pbt

  (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID

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

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

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

    ("#Find"  ,["solutions v_i"]) 

   ],

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

 (*

 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];

   *)

 store_met

  (prep_met thy  "met_test_sqrt" [] e_metID

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

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

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

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

    ("#Find"  ,["solutions v_i"])

    ],

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

    srls =append_rls "srls_contains_root" e_rls 

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

    prls =append_rls "prls_contains_root" e_rls 

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

    calc=[],

    crls=tval_rls, nrls=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_::bool])"

   ));

 store_met

  (prep_met thy  "met_test_sqrt2" [] e_metID

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

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

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

    ("#Find"  ,["solutions v_i"])

    ],

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

    srls = append_rls "srls_contains_root" e_rls 

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

    prls=e_rls,calc=[],

    crls=tval_rls, nrls=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_::bool list) = Tac subproblem_equation_dummy;          " ^

  "  L_L = Tac solve_equation_dummy                             " ^

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

   ));

 store_met

  (prep_met thy "met_test_squ_sub" [] e_metID

 (*tests subproblem fixed linear*)

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

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

    ("#Find"  ,["solutions v_i"])

    ],

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

     crls=tval_rls, 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_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^

    "                    [Test,solve_linear]) [BOOL e_e, REAL v_])" ^

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

   ));

 store_met

  (prep_met thy "met_test_squ_sub2" [] e_metID

  (*tests subproblem fixed degree 2*)

  (["Test","squ-equ-test-subpbl2"]:metID,

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

    ("#Find"  ,["solutions v_i"])

    ],

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

     crls=tval_rls, nrls=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 = Try (Rewrite_Set norm_equation False) e_e;              " ^

    "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^

    "                    [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^

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

    )); 

 store_met

  (prep_met thy "met_test_squ_nonterm" [] e_metID

  (*root-equation: see foils..., but notTerminating*)

  (["Test","square_equation...notTerminating"]:metID,

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

    ("#Find"  ,["solutions v_i"])

    ],

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

    srls = append_rls "srls_contains_root" e_rls 

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

    prls=e_rls,calc=[],

     crls=tval_rls, nrls=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_::bool list) =                                        " ^

  "    (SubProblem (Test_,[linear,univariate,equation,test]," ^

  "                 [Test,solve_linear]) [BOOL e_e, REAL v_])" ^

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

   ));

 store_met

  (prep_met thy  "met_test_eq1" [] e_metID

 (*root-equation1:*)

  (["Test","square_equation1"]:metID,

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

     ("#Find"  ,["solutions v_i"])

     ],

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

    srls = append_rls "srls_contains_root" e_rls 

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

    prls=e_rls,calc=[],

     crls=tval_rls, nrls=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_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^

  "                    [Test,solve_linear]) [BOOL e_e, REAL v_])" ^

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

   ));

 store_met

  (prep_met thy "met_test_squ2" [] e_metID

  (*root-equation2*)

  (["Test","square_equation2"]:metID,

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

     ("#Find"  ,["solutions v_i"])

     ],

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

    srls = append_rls "srls_contains_root" e_rls 

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

    prls=e_rls,calc=[],

     crls=tval_rls, nrls=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_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^

  "                    [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^

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

   ));

 store_met

  (prep_met thy "met_test_squeq" [] e_metID

  (*root-equation*)

  (["Test","square_equation"]:metID,

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

     ("#Find"  ,["solutions v_i"])

     ],

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

    srls = append_rls "srls_contains_root" e_rls 

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

    prls=e_rls,calc=[],

     crls=tval_rls, nrls=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_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^

  "                    [no_met]) [BOOL e_e, REAL v_])" ^

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

   ) ); (*#######*)

 store_met

  (prep_met thy "met_test_eq_plain" [] e_metID

  (*solve_plain_square*)

  (["Test","solve_plain_square"]:metID,

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

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

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

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

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

    ("#Find"  ,["solutions v_i"]) 

    ],

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

     prls = assoc_rls "matches",

     crls=tval_rls, nrls=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))"

  ));

 store_met

  (prep_met thy "met_test_norm_univ" [] e_metID

  (["Test","norm_univar_equation"]:metID,

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

    ("#Where" ,[]), 

    ("#Find"  ,["solutions v_i"]) 

    ],

    {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,

    calc=[],

     crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},

   "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_]))"

  ));

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

 (*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 int_of_str (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.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

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

   | Term_Ord.term_ord' pr thy (t, u) =

       (if pr then 

 	 let

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

 	   val _=writeln("t= f@ts= " ^ "" ^

 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^

 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]""");

 	   val _=writeln("u= g@us= " ^ "" ^

 	      ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^

 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]""");

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

 	      (string_of_int(size_of_term' t)) ^ ", " ^

 	      (string_of_int(size_of_term' u)) ^ ")");

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

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

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

 	   val _=writeln("-------");

 	 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 (assoc_thy "Isac"))(ts, us);

 in

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

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

 end;(*local*)

 rew_ord' := overwritel (!rew_ord',

 [("termlessI", termlessI),

  ("ord_make_polytest", ord_make_polytest false thy)

  ]);

 (*WN060510 this was a preparation for prep_rls ...

 val scr_make_polytest = 

 "Script Expand_binomtest t_ =" ^

 "(Repeat                       " ^

 "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 

 " (Try (Repeat (Rewrite left_distrib   False))) @@ " ^	 

 " (Try (Repeat (Rewrite right_distrib  False))) @@ " ^	

 " (Try (Repeat (Rewrite left_diff_distrib  False))) @@ " ^	

 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^	

 " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^		   

 " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^		   

 " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^	 

 " (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^		

 " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	

 " (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^		

 " (Try (Repeat (Rewrite add_commute        False))) @@ " ^		

 " (Try (Repeat (Rewrite add_left_commute   False))) @@ " ^	 

 " (Try (Repeat (Rewrite add_assoc          False))) @@ " ^	 

 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 

 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 

 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^		

 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^		

 " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^		

 " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^	

 " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^		

 " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^   

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

 " (Try (Repeat (Calculate TIMES ))) @@ " ^

 " (Try (Repeat (Calculate POWER)))) " ^  

 " t_)";

 -----------------------------------------------------*)

 val make_polytest =

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

       rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),

       erls = testerls, srls = Erls,

       calc = [("PLUS"  , ("op +", eval_binop "#add_")), 

 	      ("TIMES" , ("op *", eval_binop "#mult_")),

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

 	      ],

       (*asm_thm = [],*)

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

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

 	       Thm ("left_distrib" ,num_str @{thm left_distrib}),

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

 	       Thm ("right_distrib",num_str @{thm right_distrib}),

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

 	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),

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

 	       Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),

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

 	       Thm ("mult_1_left",num_str @{thm mult_1_left}),                 

 	       (*"1 * z = z"*)

 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),        

 	       (*"0 * z = 0"*)

 	       Thm ("add_0_left",num_str @{thm add_0_left}),

 	       (*"0 + z = z"*)

 	       (*AC-rewriting*)

 	       Thm ("real_mult_commute",num_str @{thm real_mult_commute}),

 	       (* z * w = w * z *)

 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),

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

 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),		

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

 	       Thm ("add_commute",num_str @{thm add_commute}),	

 	       (*z + w = w + z*)

 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),

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

 	       Thm ("add_assoc",num_str @{thm add_assoc}),	               

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

 	       Thm ("sym_realpow_twoI",

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

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

 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),		

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

 	       Thm ("sym_real_mult_2",

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

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

 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),	

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

 	       Thm ("real_num_collect",num_str @{thm real_num_collect}), 

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

 	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),

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

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

 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),	

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

 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 

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

 	       Calc ("op +", eval_binop "#add_"), 

 	       Calc ("op *", eval_binop "#mult_"),

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

 	       ],

       scr = EmptyScr(*Script ((term_of o the o (parse thy)) 

       scr_make_polytest)*)

       }:rls;      

 (*WN060510 this was done before 'fun prep_rls' ...

 val scr_expand_binomtest =

 "Script Expand_binomtest t_ =" ^

 "(Repeat                       " ^

 "((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ " ^

 " (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ " ^

 " (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^

 " (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^

 " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^

 " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^

 " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^

 " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^

 " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^

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

 " (Try (Repeat (Calculate TIMES ))) @@ " ^

 " (Try (Repeat (Calculate POWER))) @@ " ^

 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^

 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^

 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^

 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^

 " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^

 " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^

 " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^

 " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^ 

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

 " (Try (Repeat (Calculate TIMES ))) @@ " ^

 " (Try (Repeat (Calculate POWER)))) " ^  

 " t_)";

 ------------------------------------------------------*)

 val expand_binomtest =

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

       rew_ord = ("termlessI",termlessI),

       erls = testerls, srls = Erls,

       calc = [("PLUS"  , ("op +", eval_binop "#add_")), 

 	      ("TIMES" , ("op *", eval_binop "#mult_")),

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

 	      ],

       rules = [Thm ("real_plus_binom_pow2"  ,num_str @{thm real_plus_binom_pow2}),     

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

 	       Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),    

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

 	       Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),   

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

 	       Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),   

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

 	       Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),   

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

 	       Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),   

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

 	       (*RL 020915*)

 	       Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), 

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

                Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), 

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

                Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), 

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

                Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), 

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

 	       Thm ("realpow_multI",num_str @{thm realpow_multI}),                

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

 	       Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),

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

 	       Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),

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

              (*  Thm ("left_distrib" ,num_str @{thm left_distrib}}),	

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

 	       Thm ("right_distrib",num_str @{thm right_distrib}),	

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

 	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),	

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

 	       Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),	

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

 	       *)

 	       Thm ("mult_1_left",num_str @{thm mult_1_left}}),              (*"1 * z = z"*)

 	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}}),              (*"0 * z = 0"*)

 	       Thm ("add_0_left",num_str @{thm add_0_left}}),(*"0 + z = z"*)

 	       Calc ("op +", eval_binop "#add_"), 

 	       Calc ("op *", eval_binop "#mult_"),

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

                (*	       

 	        Thm ("real_mult_commute",num_str @{thm real_mult_commute}),		(*AC-rewriting*)

 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),	(**)

 	       Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),			(**)

 	       Thm ("add_commute",num_str @{thm add_commute}),		(**)

 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),	(**)

 	       Thm ("add_assoc",num_str @{thm add_assoc}),	                (**)

 	       *)

 	       Thm ("sym_realpow_twoI",

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

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

 	       Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),			

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

 	       (*Thm ("sym_real_mult_2",

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

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

 	       Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),		

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

 	       Thm ("real_num_collect",num_str @{thm real_num_collect}), 

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

 	       Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),	

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

 	       Thm ("real_one_collect",num_str @{thm real_one_collect}),		

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

 	       Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), 

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

 	       Calc ("op +", eval_binop "#add_"), 

 	       Calc ("op *", eval_binop "#mult_"),

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

 	       ],

       scr = EmptyScr

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

       }:rls;      

 ruleset' := overwritelthy @{theory} (!ruleset',

    [("make_polytest", prep_rls make_polytest),

     ("expand_binomtest", prep_rls expand_binomtest)

     ]);

 *}

 end