(* 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 (\<^type_name>\<open>fun\<close>, [Type (s2, []), Type (\<^type_name>\<open>fun\<close>, [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 (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) $ arg1 $ _) = arg1

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

fun bin_op_arg2 ((Const (_,

    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>fun\<close>, [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 (\<^const_name>\<open>HOL.eq\<close>,

    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ _) = true

  | is_equation _ = false;

fun equ_lhs ((Const (\<^const_name>\<open>HOL.eq\<close>,

    (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []),Type (\<^type_name>\<open>bool\<close>,[])])])))) $ l $ _) = l

  | equ_lhs _ = raise NO_EQUATION_TERM;

fun equ_rhs ((Const (\<^const_name>\<open>HOL.eq\<close>, (Type (\<^type_name>\<open>fun\<close>,

		 [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>bool\<close>,[])])])))) $ _ $ 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 (\<^const_name>\<open>numeral\<close>, _) $ _) = []

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

  | varids (Free (s, Type (_,[]))) = [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 (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [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_num; m is_num |] ==> (l::real)*n + m*n = (l + m) * n" and

  rcollect_one_left:

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

  rcollect_one_left_assoc:

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

  rcollect_one_left_assoc_p:

          "m is_num ==> 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_num; b is_num |] ==> 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_num; c is_num; d is_num |] ==> a/d + c/d = (a+c)/(d::real)" and

  radd_real_const:

          "[| a is_num; b is_num; c is_num; d is_num |] ==> 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 (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) ctxt = 

  if member op = (ids_of arg) "sqrt"

  then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",

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

  else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt 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 (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)) ctxt = 

    SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt 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 (\<^const_name>\<open>Test.precond_rootpbl\<close>, _) $ arg)) ctxt = 

    SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",

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

	| eval_precond_rootpbl _ _ _ _ = NONE;

\<close>

calculation contains_root = \<open>eval_contains_root "#contains_root_"\<close>

calculation Test.precond_rootmet = \<open>eval_precond_rootmet "#Test.precond_rootmet_"\<close>

calculation Test.precond_rootpbl = \<open>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

      \<^const_name>\<open>realpow\<close> => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)

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

  | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)

  | 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 \<^const_name>\<open>realpow\<close>=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) (ts, us) = 

    (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = 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>\<open>refl\<close>,

	     \<^rule_thm>\<open>order_refl\<close>,

	     \<^rule_thm>\<open>radd_left_cancel_le\<close>,

	     \<^rule_thm>\<open>not_true\<close>,

	     \<^rule_thm>\<open>not_false\<close>,

	     \<^rule_thm>\<open>and_true\<close>,

	     \<^rule_thm>\<open>and_false\<close>,

	     \<^rule_thm>\<open>or_true\<close>,

	     \<^rule_thm>\<open>or_false\<close>,

	     \<^rule_thm>\<open>and_commute\<close>,

	     \<^rule_thm>\<open>or_commute\<close>,

	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),

	     \<^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>realpow\<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>\<open>refl\<close>,

	     \<^rule_thm>\<open>order_refl\<close>,

	     \<^rule_thm>\<open>radd_left_cancel_le\<close>,

	     \<^rule_thm>\<open>not_true\<close>,

	     \<^rule_thm>\<open>not_false\<close>,

	     \<^rule_thm>\<open>and_true\<close>,

	     \<^rule_thm>\<open>and_false\<close>,

	     \<^rule_thm>\<open>or_true\<close>,

	     \<^rule_thm>\<open>or_false\<close>,

	     \<^rule_thm>\<open>and_commute\<close>,

	     \<^rule_thm>\<open>or_commute\<close>,

	     \<^rule_thm>\<open>real_diff_minus\<close>,

	     \<^rule_thm>\<open>root_ge0\<close>,

	     \<^rule_thm>\<open>root_add_ge0\<close>,

	     \<^rule_thm>\<open>root_ge0_1\<close>,

	     \<^rule_thm>\<open>root_ge0_2\<close>,

	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),

	     \<^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>realpow\<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 = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 

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

    rules = [

      \<^rule_thm_sym>\<open>add.assoc\<close>,

      \<^rule_thm_sym>\<open>rmult_assoc\<close>],

    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>\<open>radd_commute\<close>,

      \<^rule_thm>\<open>radd_left_commute\<close>,

      \<^rule_thm>\<open>add.assoc\<close>,

      \<^rule_thm>\<open>rmult_commute\<close>,

      \<^rule_thm>\<open>rmult_left_commute\<close>,

      \<^rule_thm>\<open>rmult_assoc\<close>],

    scr = Rule.Empty_Prog};      

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

val norm_equation =

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

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

    rules = [

      \<^rule_thm>\<open>rnorm_equation_add\<close>],

    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>\<open>real_diff_minus\<close>,

	     \<^rule_thm>\<open>radd_mult_distrib2\<close>,

	     \<^rule_thm>\<open>rdistr_right_assoc\<close>,

	     \<^rule_thm>\<open>rdistr_right_assoc_p\<close>,

	     \<^rule_thm>\<open>rdistr_div_right\<close>,

	     \<^rule_thm>\<open>rbinom_power_2\<close>,	       

             \<^rule_thm>\<open>radd_commute\<close>,

	     \<^rule_thm>\<open>radd_left_commute\<close>,

	     \<^rule_thm>\<open>add.assoc\<close>,

	     \<^rule_thm>\<open>rmult_commute\<close>,

	     \<^rule_thm>\<open>rmult_left_commute\<close>,

	     \<^rule_thm>\<open>rmult_assoc\<close>,

	     \<^rule_thm>\<open>radd_real_const_eq\<close>,

	     \<^rule_thm>\<open>radd_real_const\<close>,

	     (* 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>realpow\<close> (**)(eval_binop "#power_"),

	     \<^rule_thm>\<open>rcollect_right\<close>,

	     \<^rule_thm>\<open>rcollect_one_left\<close>,

	     \<^rule_thm>\<open>rcollect_one_left_assoc\<close>,

	     \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>,

	     \<^rule_thm>\<open>rshift_nominator\<close>,

	     \<^rule_thm>\<open>rcancel_den\<close>,

	     \<^rule_thm>\<open>rroot_square_inv\<close>,

	     \<^rule_thm>\<open>rroot_times_root\<close>,

	     \<^rule_thm>\<open>rroot_times_root_assoc_p\<close>,

	     \<^rule_thm>\<open>rsqare\<close>,

	     \<^rule_thm>\<open>power_1\<close>,

	     \<^rule_thm>\<open>rtwo_of_the_same\<close>,

	     \<^rule_thm>\<open>rtwo_of_the_same_assoc_p\<close>,

	     \<^rule_thm>\<open>rmult_1\<close>,

	     \<^rule_thm>\<open>rmult_1_right\<close>,

	     \<^rule_thm>\<open>rmult_0\<close>,

	     \<^rule_thm>\<open>rmult_0_right\<close>,

	     \<^rule_thm>\<open>radd_0\<close>,

	     \<^rule_thm>\<open>radd_0_right\<close>],

    scr = Rule.Empty_Prog};      

\<close>

ML \<open>

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

val isolate_root =

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

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

    rules = [

       \<^rule_thm>\<open>rroot_to_lhs\<close>,

	     \<^rule_thm>\<open>rroot_to_lhs_mult\<close>,

	     \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>,

	     \<^rule_thm>\<open>risolate_root_add\<close>,

	     \<^rule_thm>\<open>risolate_root_mult\<close>,

	     \<^rule_thm>\<open>risolate_root_div\<close>],

    scr = Rule.Empty_Prog};      

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

val isolate_bdv =

  Rule_Def.Repeat{

    id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),

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

  	rules = [

      \<^rule_thm>\<open>risolate_bdv_add\<close>,

      \<^rule_thm>\<open>risolate_bdv_mult_add\<close>,

      \<^rule_thm>\<open>risolate_bdv_mult\<close>,

      \<^rule_thm>\<open>mult_square\<close>,

      \<^rule_thm>\<open>constant_square\<close>,

      \<^rule_thm>\<open>constant_mult_square\<close>],

    scr = Rule.Empty_Prog};      

\<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 pbl_test : "test" = \<open>Rule_Set.empty\<close>

problem pbl_test_equ : "equation/test" =

  \<open>assoc_rls' @{theory} "matches"\<close>

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality e_e" "solveFor v_v"

  Where: "matches (?a = ?b) e_e"

  Find: "solutions v_v'i'"

problem pbl_test_uni : "univariate/equation/test" =

  \<open>assoc_rls' @{theory} "matches"\<close>

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality e_e" "solveFor v_v"

  Where: "matches (?a = ?b) e_e"

  Find: "solutions v_v'i'"

problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =

  \<open>assoc_rls' @{theory} "matches"\<close>

  Method_Ref: "Test/solve_linear"

  CAS: "solve (e_e::bool, v_v)"

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

setup \<open>KEStore_Elems.add_rew_ord [

  ("termlessI", termlessI),

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

ML \<open>

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"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 

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

	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],

    errpatts = [],

    rules = [

       \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)

	     \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

	     \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

	     \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

	     \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

	     \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)

	     \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)

	     \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)

	     (*AC-rewriting*)

	     \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)

	     \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

	     \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

	     \<^rule_thm>\<open>add.commute\<close>,	 (*z + w = w + z*)

	     \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)

	     \<^rule_thm>\<open>add.assoc\<close>, (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)

	     \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)

	     \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)

	     \<^rule_thm_sym>\<open>real_mult_2\<close>,	 (*"z1 + z1 = 2 * z1"*)

	     \<^rule_thm>\<open>real_mult_2_assoc\<close>,	 (*"z1 + (z1 + k) = 2 * z1 + k"*)

	     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)

	     \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)

	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)

	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> 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>realpow\<close> (**)(eval_binop "#power_")],

    scr = Rule.Empty_Prog}; 

val expand_binomtest =

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

    rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,

    calc = [

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

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

	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))

	    ],

    errpatts = [],

    rules = [

      \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)

      \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)

      \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)

      \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)

      \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)

      \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)

      (*RL 020915*)

      \<^rule_thm>\<open>real_pp_binom_times\<close>,  (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)

      \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)

      \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)

      \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)

      \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)

      \<^rule_thm>\<open>real_plus_binom_pow3\<close>, (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)

      \<^rule_thm>\<open>real_minus_binom_pow3\<close>, (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)

    	\<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)

    	\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)

    	\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)

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

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

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

    	\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)

    	\<^rule_thm>\<open>realpow_plus_1\<close>,	 (*"r * r \<up> n = r \<up> (n + 1)"*)

    	(*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)

    	\<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)

    	\<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==> l * n + m * n = (l + m) * n"*)

    	\<^rule_thm>\<open>real_num_collect_assoc\<close>,	 (*"[| l is_num; m is_num |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)

    	\<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)

    	\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> 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>realpow\<close> (**)(eval_binop "#power_")],

    scr = Rule.Empty_Prog};      

\<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>

problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =

  \<open>assoc_rls' @{theory} "matches"\<close>

  Method_Ref: "Test/solve_plain_square"

  CAS: "solve (e_e::bool, v_v)"

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

problem pbl_test_uni_poly : "polynomial/univariate/equation/test" =

  \<open>Rule_Set.empty\<close>

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"

  Where: "HOL.False"

  Find: "solutions v_v'i'"

problem pbl_test_uni_poly_deg2 : "degree_two/polynomial/univariate/equation/test" =

  \<open>Rule_Set.empty\<close>

  CAS: "solve (v_v  \<up> 2 + p_p * v_v + q__q = 0, v_v)"

  Given: "equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"

  Find: "solutions v_v'i'"

problem pbl_test_uni_poly_deg2_pq : "pq_formula/degree_two/polynomial/univariate/equation/test" =

  \<open>Rule_Set.empty\<close>

  CAS: "solve (v_v  \<up> 2 + p_p * v_v + q__q = 0, v_v)"

  Given: "equality (v_v  \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"

  Find: "solutions v_v'i'"

problem pbl_test_uni_poly_deg2_abc : "abc_formula/degree_two/polynomial/univariate/equation/test" =

  \<open>Rule_Set.empty\<close>

  CAS: "solve (a_a * x  \<up> 2 + b_b * x + c_c = 0, v_v)"

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

  Find: "solutions v_v'i'"

problem pbl_test_uni_root : "squareroot/univariate/equation/test" =

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

    (eval_contains_root "#contains_root_")]\<close>

  Method_Ref: "Test/square_equation"

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality e_e" "solveFor v_v"

  Where: "precond_rootpbl v_v"

  Find: "solutions v_v'i'"

problem pbl_test_uni_norm : "normalise/univariate/equation/test" =

  \<open>Rule_Set.empty\<close>

  Method_Ref: "Test/norm_univar_equation"

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality e_e" "solveFor v_v"

  Where:

  Find: "solutions v_v'i'"

problem pbl_test_uni_roottest : "sqroot-test/univariate/equation/test" =

  \<open>Rule_Set.empty\<close>

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality e_e" "solveFor v_v"

  Where: "precond_rootpbl v_v"

  Find: "solutions v_v'i'"

problem pbl_test_intsimp : "inttype/test" =

  \<open>Rule_Set.empty\<close>

  Method_Ref: "Test/intsimp"

  Given: "intTestGiven t_t"

  Where:

  Find: "intTestFind s_s"

section \<open>methods\<close>

subsection \<open>differentiate\<close>

method "met_test" : "Test" =

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

  crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}\<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])"

method met_test_solvelin : "Test/solve_linear" =

  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,

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

    nrls = Test_simplify}\<close>

  Program: solve_linear.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "matches (?a = ?b) e_e"

  Find: "solutions v_v'i'"

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

method met_test_sqrt : "Test/sqrt-equ-test" =

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

  \<open>{rew_ord'="Rewrite_Ord.id_empty",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", "")]*)}\<close>

  Program: solve_root_equ.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "contains_root (e_e::bool)"

  Find: "solutions v_v'i'"

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

method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =

  (*tests subproblem fixed linear*)

  \<open>{rew_ord' = "Rewrite_Ord.id_empty", 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}\<close>

  Program: minisubpbl.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "precond_rootmet v_v"

  Find: "solutions v_v'i'"

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

method met_test_eq1 : "Test/square_equation1" =

  (*root-equation1:*)

  \<open>{rew_ord'="Rewrite_Ord.id_empty",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}\<close>

  Program: solve_root_equ2.simps

  Given: "equality e_e" "solveFor v_v"

  Find: "solutions v_v'i'"

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

method met_test_squ2 : "Test/square_equation2" =

  (*root-equation2*)

  \<open>{rew_ord'="Rewrite_Ord.id_empty",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}\<close>

  Program: solve_root_equ3.simps

  Given: "equality e_e" "solveFor v_v"

  Find: "solutions v_v'i'"

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

  where

"solve_root_equ4 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'', [''univariate'', ''equation'', ''test''],

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

  in

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

method met_test_squeq : "Test/square_equation" =

  (*root-equation*)

  \<open>{rew_ord'="Rewrite_Ord.id_empty",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}\<close>

  Program: solve_root_equ4.simps

  Given: "equality e_e" "solveFor v_v"

  Find: "solutions v_v'i'"

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

  where

"solve_plain_square e_e v_v = (

  let

    e_e = (

      (Try (Rewrite_Set ''isolate_bdv'' )) #>

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

      ((Rewrite ''square_equality_0'' ) Or

       (Rewrite ''square_equality'' )) #>

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

  in

    Or_to_List e_e)"

method met_test_eq_plain : "Test/solve_plain_square" =

  (*solve_plain_square*)

  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,

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

    asm_rls=[],asm_thm=[]*)}\<close>

  Program: solve_plain_square.simps

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

subsection \<open>polynomial equation\<close>

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

  where

"norm_univariate_equ e_e v_v = (

  let

    e_e = (

      (Try (Rewrite ''rnorm_equation_add'' )) #>

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

  in

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

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

method met_test_norm_univ : "Test/norm_univar_equation" =

  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,

    errpats = [], nrls = Rule_Set.empty}\<close>

  Program: norm_univariate_equ.simps

  Given: "equality e_e" "solveFor v_v"

  Where:

  Find: "solutions v_v'i'"

subsection \<open>diophantine equation\<close>

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

  where

"test_simplify t_t = (

  Repeat (

    (Try (Calculate ''PLUS'')) #>         

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