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

   for the purpose of simplifying tests.

   Author: Walther Neuper 2003

   (c) due to copyright terms

Notes on cleanup:

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

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

    differentiate, root equatioh, polynomial equation, diophantine equation

(2) transfer problems accordingly

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

(4) rearrange axiomatizations according to (3)

*) 

theory Test imports Base_Tools Poly Rational Root Diff begin

section \<open>consts for problems\<close>

consts

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

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

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

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

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

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

section \<open>functions\<close>

ML \<open>

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

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

    | bin_o _ = [];

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

  | bin_op t         =  bin_o t;

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

fun bin_op_arg1 ((Const (_,

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

  | bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);

fun bin_op_arg2 ((Const (_,

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

  | bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);

exception NO_EQUATION_TERM;

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

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

  | is_equation _ = false;

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

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

  | equ_lhs _ = raise NO_EQUATION_TERM;

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

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

  | equ_rhs _ = raise NO_EQUATION_TERM;

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

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

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

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

  | atom _ = false;

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

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

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

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

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

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

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

  | varids _ = [];

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

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

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

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

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

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

    andalso polynomial opl (equ_lhs t) bdVar 

    andalso polynomial opl (equ_rhs t) bdVar

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

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

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

fun degree addl mul bdVar t =

let

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

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

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

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

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

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

    if subset op = (bin_op h, addl)

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

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

  | deg _ _ _ t = raise ERROR ("deg: t = " ^ UnparseC.term t)

in

  if polynomial (addl @ [mul]) t bdVar

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

  else (NONE:int option)

end;

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

let

  fun opt (SOME i)= i

	  | opt  NONE = 0

in opt (degree addl mul bdVar t) end;

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

fun linear_equ addl mul bdVar t =

  if is_equation t 

  then

    let

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

	    val degr = degree_ addl mul bdVar (equ_rhs t)

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

  else false;

(* strip_thy op_  before *)

fun is_div_op (dv, (Const (op_,

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

  | is_div_op _ = false;

fun is_denom bdVar div_op t =

  let

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

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

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

  	  | is _ [_] _ ((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)

  	  | is _ _ _ _ = raise ERROR "is_denom: uncovered case in fun.def."    

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

fun rational t div_op bdVar = 

    is_denom bdVar div_op t andalso bin_ops_only t;

\<close>

section \<open>axiomatizations\<close>

axiomatization where (*TODO: prove as theorems*)

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

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

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

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

  rcollect_right:

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

  rcollect_one_left:

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

  rcollect_one_left_assoc:

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

  rcollect_one_left_assoc_p:

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

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

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

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

  rcancel_den:             "a \<noteq> 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 \<up> b) \<up> c = a \<up> (b * c)" and

  rsqare:                  "(a::real) * a = a \<up> 2" and

  power_1:                 "(a::real) \<up> 1 = a" and

  rbinom_power_2:          "((a::real) + b) \<up>  2 = a \<up>  2 + 2*a*b + b \<up>  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 = True" 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) \<up>  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 \<up>  2)))" and

  square_equation_right:

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

  (*causes frequently non-termination:*)

  square_equation:  

          "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a \<up>  2)=b \<up>  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 \<up> 2 = b) = (bdv \<up> 2 = b / a)" and

  constant_square:       "(a + bdv \<up> 2 = b) = (bdv \<up> 2 = b + -1*a)" and

  constant_mult_square:  "(a + b*bdv \<up> 2 = c) = (b*bdv \<up> 2 = c + -1*a)" and

  square_equality: 

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

  square_equality_0:

	     "(x \<up> 2 = 0) = (x = 0)" and

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

  otherwise shuffling from left to right would not terminate*)  

(*Ambiguous input\<^here> produces 2 parse trees -----------------------------\\*)

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

(*Ambiguous input\<^here> produces 2 parse trees -----------------------------//*)

section \<open>eval functions\<close>

ML \<open>

(** evaluation of numerals and predicates **)

(*does a term contain a root ?*)

fun eval_contains_root (thmid:string) _ 

		       (t as (Const("Test.contains_root", _) $ arg)) thy = 

  if member op = (ids_of arg) "sqrt"

  then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",

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

  else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy 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 (UnparseC.term_in_thy 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 (UnparseC.term_in_thy thy arg) "",

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

	| eval_precond_rootpbl _ _ _ _ = NONE;

\<close>

setup \<open>KEStore_Elems.add_calcs

  [("contains_root", ("Test.contains_root", eval_contains_root"#contains_root_")),

    ("Test.precond_rootmet", ("Test.precond_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),

    ("Test.precond_rootpbl", ("Test.precond_rootpbl",

        eval_precond_rootpbl"#Test.precond_rootpbl_"))]

\<close>

ML \<open>

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

  make_polynomial  ---> make_poly

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

local (*. for make_polytest .*)

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

fun pr_ord EQUAL = "EQUAL"

  | pr_ord LESS  = "LESS"

  | pr_ord GREATER = "GREATER";

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

    (case a of

      "Transcendental.powr" => ((("|||||||||||||", 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)

  | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";

\<^isac_test>\<open>

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

    	(case TermC.int_opt_of_string order of

	             SOME d => d

		   | NONE   => 0)

  | get_order_pow _ = 0;

\<close>

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

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

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

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

  | size_of_term' _ = 1;

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

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

                                   | ord => ord)

  | term_ord' pr _ (t, u) =

    (if pr then 

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

	     val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^

	                      commas(map UnparseC.term ts) ^ "]\"")

	     val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^

	                      commas(map UnparseC.term us) ^"]\"")

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

	                      string_of_int (size_of_term' t) ^ ", " ^

	                      string_of_int (size_of_term' u) ^ ")")

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

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

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

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

	 in () end

       else ();

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

	   EQUAL =>

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

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

	     | ord => ord)

	     end

	 | ord => ord)

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

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

and terms_ord _ pr (ts, us) = 

    list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);

in

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

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

end;(*local*)

\<close> 

section \<open>term order\<close>

ML \<open>

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

\<close>

section \<open>rulesets\<close>

ML \<open>

val testerls = 

  Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), 

      erls = Rule_Set.empty, srls = Rule_Set.Empty, 

      calc = [], errpatts = [], 

      rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),

	       Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),

	       Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),

	       Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

	       Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),

	       Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),

	       Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),

	       Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),

	       Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),

	       Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),

	       Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),

	       \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),

	       \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),

	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),

	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),

	       \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

	       \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),

	       \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],

      scr = Rule.Empty_Prog

      };      

\<close>

ML \<open>

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

(*FIXXXXXXME 10.8.02: handle like _simplify*)

val tval_rls =  

  Rule_Def.Repeat{id = "tval_rls", preconds = [], 

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

      erls=testerls,srls = Rule_Set.empty, 

      calc=[], errpatts = [],

      rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),

	       Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),

	       Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),

	       Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

	       Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),

	       Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),

	       Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),

	       Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),

	       Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),

	       Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),

	       Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),

	       Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),

	       Rule.Thm ("root_ge0",ThmC.numerals_to_Free @{thm root_ge0}),

	       Rule.Thm ("root_add_ge0",ThmC.numerals_to_Free @{thm root_add_ge0}),

	       Rule.Thm ("root_ge0_1",ThmC.numerals_to_Free @{thm root_ge0_1}),

	       Rule.Thm ("root_ge0_2",ThmC.numerals_to_Free @{thm root_ge0_2}),

	       \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),

	       \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),

	       \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),

	       \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),

	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),

	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	       \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),

	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),

	       \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

	       \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),

	       \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],

      scr = Rule.Empty_Prog

      };      

\<close>

rule_set_knowledge testerls = \<open>prep_rls' testerls\<close>

ML \<open>

(*make () dissappear*)   

val rearrange_assoc =

  Rule_Def.Repeat{id = "rearrange_assoc", preconds = [], 

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

      erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],

      rules = 

      [Rule.Thm ("sym_add.assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),

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

      scr = Rule.Empty_Prog

      };      

val ac_plus_times =

  Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),

      erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],

      rules = 

      [Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),

       Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),

       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),

       Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),

       Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),

       Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc})],

      scr = Rule.Empty_Prog

      };      

(*todo: replace by Rewrite("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add)*)

val norm_equation =

  Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),

      erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],

      rules = [Rule.Thm ("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add})

	       ],

      scr = Rule.Empty_Prog

      };      

\<close>

ML \<open>

(* expects * distributed over + *)

val Test_simplify =

  Rule_Def.Repeat{id = "Test_simplify", preconds = [], 

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

      erls = tval_rls, srls = Rule_Set.empty, 

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

      rules = [

	       Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),

	       Rule.Thm ("radd_mult_distrib2",ThmC.numerals_to_Free @{thm radd_mult_distrib2}),

	       Rule.Thm ("rdistr_right_assoc",ThmC.numerals_to_Free @{thm rdistr_right_assoc}),

	       Rule.Thm ("rdistr_right_assoc_p",ThmC.numerals_to_Free @{thm rdistr_right_assoc_p}),

	       Rule.Thm ("rdistr_div_right",ThmC.numerals_to_Free @{thm rdistr_div_right}),

	       Rule.Thm ("rbinom_power_2",ThmC.numerals_to_Free @{thm rbinom_power_2}),	       

               Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}), 

	       Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),

	       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),

	       Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),

	       Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),

	       Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc}),

	       Rule.Thm ("radd_real_const_eq",ThmC.numerals_to_Free @{thm radd_real_const_eq}),

	       Rule.Thm ("radd_real_const",ThmC.numerals_to_Free @{thm radd_real_const}),

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

		  thus they MUST be done IMMEDIATELY before calc *)

	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),

	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),

	       Rule.Thm ("rcollect_right",ThmC.numerals_to_Free @{thm rcollect_right}),

	       Rule.Thm ("rcollect_one_left",ThmC.numerals_to_Free @{thm rcollect_one_left}),

	       Rule.Thm ("rcollect_one_left_assoc",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc}),

	       Rule.Thm ("rcollect_one_left_assoc_p",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc_p}),

	       Rule.Thm ("rshift_nominator",ThmC.numerals_to_Free @{thm rshift_nominator}),

	       Rule.Thm ("rcancel_den",ThmC.numerals_to_Free @{thm rcancel_den}),

	       Rule.Thm ("rroot_square_inv",ThmC.numerals_to_Free @{thm rroot_square_inv}),

	       Rule.Thm ("rroot_times_root",ThmC.numerals_to_Free @{thm rroot_times_root}),

	       Rule.Thm ("rroot_times_root_assoc_p",ThmC.numerals_to_Free @{thm rroot_times_root_assoc_p}),

	       Rule.Thm ("rsqare",ThmC.numerals_to_Free @{thm rsqare}),

	       Rule.Thm ("power_1",ThmC.numerals_to_Free @{thm power_1}),

	       Rule.Thm ("rtwo_of_the_same",ThmC.numerals_to_Free @{thm rtwo_of_the_same}),

	       Rule.Thm ("rtwo_of_the_same_assoc_p",ThmC.numerals_to_Free @{thm rtwo_of_the_same_assoc_p}),

	       Rule.Thm ("rmult_1",ThmC.numerals_to_Free @{thm rmult_1}),

	       Rule.Thm ("rmult_1_right",ThmC.numerals_to_Free @{thm rmult_1_right}),

	       Rule.Thm ("rmult_0",ThmC.numerals_to_Free @{thm rmult_0}),

	       Rule.Thm ("rmult_0_right",ThmC.numerals_to_Free @{thm rmult_0_right}),

	       Rule.Thm ("radd_0",ThmC.numerals_to_Free @{thm radd_0}),

	       Rule.Thm ("radd_0_right",ThmC.numerals_to_Free @{thm radd_0_right})

	       ],

      scr = Rule.Empty_Prog

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

      };      

\<close>

ML \<open>

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

val isolate_root =

  Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), 

      erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],

      rules = [Rule.Thm ("rroot_to_lhs",ThmC.numerals_to_Free @{thm rroot_to_lhs}),

	       Rule.Thm ("rroot_to_lhs_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_mult}),

	       Rule.Thm ("rroot_to_lhs_add_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_add_mult}),

	       Rule.Thm ("risolate_root_add",ThmC.numerals_to_Free @{thm risolate_root_add}),

	       Rule.Thm ("risolate_root_mult",ThmC.numerals_to_Free @{thm risolate_root_mult}),

	       Rule.Thm ("risolate_root_div",ThmC.numerals_to_Free @{thm risolate_root_div})       ],

      scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) 

      "empty_script")

      };

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

val isolate_bdv =

    Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),

	erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],

	rules = 

	[Rule.Thm ("risolate_bdv_add",ThmC.numerals_to_Free @{thm risolate_bdv_add}),

	 Rule.Thm ("risolate_bdv_mult_add",ThmC.numerals_to_Free @{thm risolate_bdv_mult_add}),

	 Rule.Thm ("risolate_bdv_mult",ThmC.numerals_to_Free @{thm risolate_bdv_mult}),

	 Rule.Thm ("mult_square",ThmC.numerals_to_Free @{thm mult_square}),

	 Rule.Thm ("constant_square",ThmC.numerals_to_Free @{thm constant_square}),

	 Rule.Thm ("constant_mult_square",ThmC.numerals_to_Free @{thm constant_mult_square})

	 ],

	scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) 

			  "empty_script")

	};      

\<close>

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

rule_set_knowledge

  Test_simplify = \<open>prep_rls' Test_simplify\<close> and

  tval_rls = \<open>prep_rls' tval_rls\<close> and

  isolate_root = \<open>prep_rls' isolate_root\<close> and

  isolate_bdv = \<open>prep_rls' isolate_bdv\<close> and

  matches = \<open>prep_rls'

    (Rule_Set.append_rules "matches" testerls

      [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "#matches_")])\<close>

subsection \<open>problems\<close>

(** problem types **)

setup \<open>KEStore_Elems.add_pbts

  [(Problem.prep_input @{theory} "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),

    (Problem.prep_input @{theory} "pbl_test_equ" [] Problem.id_empty

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

    (Problem.prep_input @{theory} "pbl_test_uni" [] Problem.id_empty

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

    (Problem.prep_input @{theory} "pbl_test_uni_lin" [] Problem.id_empty

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

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

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

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

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

        assoc_rls' @{theory} "matches", 

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

\<close>

ML \<open>

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

[("termlessI", termlessI),

 ("ord_make_polytest", ord_make_polytest false \<^theory>)

 ]);

val make_polytest =

  Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, 

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

      erls = testerls, srls = Rule_Set.Empty,

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

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

	      ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))

	      ], errpatts = [],

      rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),

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

	       Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),

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

	       Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),

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

	       Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),

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

	       Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),

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

	       Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),                 

	       (*"1 * z = z"*)

	       Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),        

	       (*"0 * z = 0"*)

	       Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),

	       (*"0 + z = z"*)

	       (*AC-rewriting*)

	       Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),

	       (* z * w = w * z *)

	       Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),

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

	       Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),		

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

	       Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),	

	       (*z + w = w + z*)

	       Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),

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

	       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),	               

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

	       Rule.Thm ("sym_realpow_twoI",

                     ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),	

	       (*"r1 * r1 = r1 \<up> 2"*)

	       Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),		

	       (*"r * r \<up> n = r \<up> (n + 1)"*)

	       Rule.Thm ("sym_real_mult_2",

                     ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),	

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

	       Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),	

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

	       Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}), 

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

	       Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),

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

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

	       Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),	

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

	       Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}), 

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

	       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	       \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")

	       ],

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

      scr_make_polytest)*)

      }; 

val expand_binomtest =

  Rule_Def.Repeat{id = "expand_binomtest", preconds = [], 

      rew_ord = ("termlessI",termlessI),

      erls = testerls, srls = Rule_Set.Empty,

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

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

	      ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))

	      ], errpatts = [],

      rules = 

      [Rule.Thm ("real_plus_binom_pow2"  ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),     

	       (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)

       Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),    

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

       Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),   

       (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)

       Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),   

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

       Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),   

        (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)

       Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),   

        (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)

       (*RL 020915*)

       Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}), 

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

       Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}), 

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

       Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}), 

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

       Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}), 

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

       Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),                

        (*(a*b) \<up> n = a \<up> n * b \<up> n*)

       Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),

        (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)

       Rule.Thm ("real_minus_binom_pow3",ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),

        (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)

     (*  Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),	

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

	Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),	

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

	Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),	

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

	Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),	

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

	*)

	Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),              

         (*"1 * z = z"*)

	Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),              

         (*"0 * z = 0"*)

	Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),

         (*"0 + z = z"*)

	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),

        (*	       

	 Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),		

        (*AC-rewriting*)

	Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),

	Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),

	Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),	

	Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),

	Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),

	*)

	Rule.Thm ("sym_realpow_twoI",

              ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),

	(*"r1 * r1 = r1 \<up> 2"*)

	Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),			

	(*"r * r \<up> n = r \<up> (n + 1)"*)

	(*Rule.Thm ("sym_real_mult_2",

                ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),

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

	Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),		

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

	Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}), 

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

	Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),	

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

	Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),		

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

	Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}), 

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

	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 

	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	\<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")

	],

      scr = Rule.Empty_Prog

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

      };      

\<close>

rule_set_knowledge

  make_polytest = \<open>prep_rls' make_polytest\<close> and

  expand_binomtest = \<open>prep_rls' expand_binomtest\<close>

rule_set_knowledge

  norm_equation = \<open>prep_rls' norm_equation\<close> and

  ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and

  rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>

section \<open>problems\<close>

setup \<open>KEStore_Elems.add_pbts

  [(Problem.prep_input @{theory} "pbl_test_uni_plain2" [] Problem.id_empty

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

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

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

	        "(matches (     ?b*v_v  \<up> 2 = 0) e_e) |" ^

	        "(matches (?a +    v_v  \<up> 2 = 0) e_e) |" ^

	        "(matches (        v_v  \<up> 2 = 0) e_e)"]),

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

      assoc_rls' @{theory} "matches", 

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

    (Problem.prep_input @{theory} "pbl_test_uni_poly" [] Problem.id_empty

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

        [("#Given" ,["equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),

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

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

        Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),

    (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2" [] Problem.id_empty

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

        [("#Given" ,["equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),

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

        Rule_Set.empty, SOME "solve (v_v  \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),

    (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty

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

        [("#Given" ,["equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),

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

        Rule_Set.empty, SOME "solve (v_v  \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),

    (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty

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

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

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

        Rule_Set.empty, SOME "solve (a_a * x  \<up> 2 + b_b * x + c_c = 0, v_v)", [])),

    (Problem.prep_input @{theory} "pbl_test_uni_root" [] Problem.id_empty

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

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

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

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

        Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>

            (eval_contains_root "#contains_root_")], 

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

    (Problem.prep_input @{theory} "pbl_test_uni_norm" [] Problem.id_empty

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

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

          ("#Where" ,[]),

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

        Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test", "norm_univar_equation"]])),

    (Problem.prep_input @{theory} "pbl_test_uni_roottest" [] Problem.id_empty

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

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

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

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

        Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),

    (Problem.prep_input @{theory} "pbl_test_intsimp" [] Problem.id_empty

      (["inttype", "test"],

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

          ("#Where" ,[]),

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

      Rule_Set.empty, NONE, [["Test", "intsimp"]]))]\<close>

section \<open>methods\<close>

subsection \<open>differentiate\<close>

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory "Diff"} "met_test" [] MethodC.id_empty

      (["Test"], [],

        {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,

          crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]

\<close>

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

  where

"solve_linear e_e v_v = (

  let e_e =

    Repeat (

      (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>

      (Rewrite_Set ''Test_simplify'')) e_e

  in

    [e_e])"

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory} "met_test_solvelin" [] MethodC.id_empty

      (["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_Set.empty,

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

          nrls = Test_simplify},

        @{thm solve_linear.simps})]

\<close>

subsection \<open>root equation\<close>

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

  where

"solve_root_equ e_e v_v = (

  let

    e_e = (

      (While (contains_root e_e) Do (

        (Rewrite ''square_equation_left'' ) #>

        (Try (Rewrite_Set ''Test_simplify'' )) #>

        (Try (Rewrite_Set ''rearrange_assoc'' )) #>

        (Try (Rewrite_Set ''isolate_root'' )) #>

        (Try (Rewrite_Set ''Test_simplify'' )))) #>

      (Try (Rewrite_Set ''norm_equation'' )) #>

      (Try (Rewrite_Set ''Test_simplify'' )) #>

      (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>

      (Try (Rewrite_Set ''Test_simplify'' ))

      ) e_e                                                                

  in

    [e_e])"

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory} "met_test_sqrt" [] MethodC.id_empty

      (*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_Set.append_rules "srls_contains_root" Rule_Set.empty

              [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],

          prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty 

              [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],

          calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],

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

        @{thm solve_root_equ.simps})]

\<close>

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

  where

"minisubpbl e_e v_v = (

  let

    e_e = (

      (Try (Rewrite_Set ''norm_equation'' )) #>

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

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

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

  in

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

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory} "met_test_squ_sub" [] MethodC.id_empty

      (*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_Set.empty,

          prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty

              [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],

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

        @{thm minisubpbl.simps})]

\<close>

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

  where

"solve_root_equ2 e_e v_v = (

  let

    e_e = (

      (While (contains_root e_e) Do (

        (Rewrite ''square_equation_left'' ) #>

        (Try (Rewrite_Set ''Test_simplify'' )) #>

        (Try (Rewrite_Set ''rearrange_assoc'' )) #>

        (Try (Rewrite_Set ''isolate_root'' )) #>

        (Try (Rewrite_Set ''Test_simplify'' )))) #>

      (Try (Rewrite_Set ''norm_equation'' )) #>

      (Try (Rewrite_Set ''Test_simplify'' ))

      ) e_e;

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

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

  in

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

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory} "met_test_eq1" [] MethodC.id_empty

      (*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_Set.append_rules "srls_contains_root" Rule_Set.empty 

            [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,

              errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),

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

        @{thm solve_root_equ2.simps})]

\<close>

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

  where

"solve_root_equ3 e_e v_v = (

  let

    e_e = (

      (While (contains_root e_e) Do ((

        (Rewrite ''square_equation_left'' ) Or

        (Rewrite ''square_equation_right'' )) #>

        (Try (Rewrite_Set ''Test_simplify'' )) #>

        (Try (Rewrite_Set ''rearrange_assoc'' )) #>

        (Try (Rewrite_Set ''isolate_root'' )) #>

        (Try (Rewrite_Set ''Test_simplify'' )))) #>

      (Try (Rewrite_Set ''norm_equation'' )) #>

      (Try (Rewrite_Set ''Test_simplify'' ))

      ) e_e;

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

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

  in

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

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory} "met_test_squ2" [] MethodC.id_empty

      (*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_Set.append_rules "srls_contains_root" Rule_Set.empty 

              [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],

          prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],

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

        @{thm solve_root_equ3.simps})]

\<close>

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

  where

"solve_root_equ4 e_e v_v = (

  let