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

   Author: Walther Neuper 2003

   (c) due to copyright terms

*) 

theory Test imports Base_Tools Poly Rational Root Diff begin

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)

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

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

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

ML {*

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;

*}

setup {* 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_"))] *}

ML {*

(** term order **)

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

(** rule sets **)

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

      };      

*}

ML {*

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

      };      

*}

setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))] *}

ML {*

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

      };      

*}

ML {*

(** rule sets **)

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

  "Script STest_simplify (t_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_t)";

*}

ML {*

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

      };      

*}

ML {*

(** rule sets **)

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

	};      

*}

ML {*

(* association list for calculate_, calculate

   "Groups.plus_class.plus" 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"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

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

     ("DIVIDE" ,("Rings.divide_class.divide"  ,eval_cancel "#divide_e")),

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

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

     ("le"      ,("Orderings.ord_class.less"        ,eval_equ "#less_")),

     ("leq"     ,("Orderings.ord_class.less_eq"       ,eval_equ "#less_equal_")),

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

     (*von hier (ehem.SqRoot*)

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

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

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

			    eval_contains_root"#contains_root_"))

     ];

*}

ML {* val prep_rls' = LTool.prep_rls @{theory}; *}

setup {* 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",eval_matches "#matches_")])))] *}

(** problem types **)

setup {* 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"]]))(*,

    (Specify.prep_pbt thy

      (["thy"],

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

          ("#Find"  ,"boolTestFind f_f")],

        [])),

    (Specify.prep_pbt thy

      (["testeq","thy"],

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

         ("#Find"  ,"boolTestFind f_f")],

        []))*)] *}

(*val ttt = (Thm.term_of o the o (parse (Thy_Info_get_theory "Isac"))) "(matches (   v_v = 0) e_e)";

 ------ 25.8.01*)

(** methods **)

setup {* 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"),

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

    Specify.prep_met thy (*test for equations*)

      (["Test","testeq"],

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

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

        {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},

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

          "Repeat                                                            " ^

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

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

*}

setup {* 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))] *}

ML {*

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 ("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 $ r) 

              = l

  | equ_lhs _ = raise NO_EQUATION_TERM;

fun equ_rhs ((Const ("HOL.eq",(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 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,t)) = union op = [a] (varids t)

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

  | varids _         = [];

(*> val t = Thm.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 **)

setup {* 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"]]))] *}

(*

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

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

 val env = [(e_,ve)];

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

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

	      "(matches (    b*v_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 = (Thm.global_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 = "HOL.True" : cterm

*)

setup {* KEStore_Elems.add_pbts

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

(*

show_ptyps();

get_pbt ["inttype","test"];

*)

setup {* 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])"),

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

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

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

      (*tests subproblem fixed degree 2*)

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

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

          ("#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 (*, 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_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^

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

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

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

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

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

        [("#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})"),

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

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

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

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