(*.(c) by Richard Lang, 2003 .*)

(* collecting all knowledge for Root Equations

   created by: rlang 

         date: 02.08

   changed by: rlang

   last change by: rlang

             date: 02.11.14

*)

theory RootEq imports Root Equation begin

text \<open>univariate equations containing real square roots:

  This type of equations has been used to bootstrap Lucas-Interpretation.

  In 2003 this type has been extended and integrated into ISAC's equation solver

  by Richard Lang in 2003.

  The assumptions (all containing "<") didn't pass the xml-parsers at the 

  interface between math-engine and front-end.

  The migration Isabelle2002 --> 2011 dropped this type of equation, see

  test/../rooteq.sml, rootrateq.sml.

\<close>

subsection \<open>consts definition for predicates\<close>

consts

  is_rootTerm_in     :: "[real, real] => bool" ("_ is'_rootTerm'_in _")

  is_sqrtTerm_in     :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _") 

  is_normSqrtTerm_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _") 

subsection \<open>theorems not yet adopted from Isabelle\<close>

axiomatization where

(* normalise *)

  makex1_x:            "a \<up> 1  = a"   and

  real_assoc_1:        "a+(b+c) = a+b+c" and

  real_assoc_2:        "a*(b*c) = a*b*c" and

  (* simplification of root*)

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

  sqrt_square_2:       "sqrt (a  \<up>  2) = a" and

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

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

  (* isolate one root on the LEFT or RIGHT hand side of the equation *)

  sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==> 

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

  sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>

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

  sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>

   (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" and

  sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>

   (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" and

  sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>

   (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" and

  sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>

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

  sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>

   (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" and

  sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>

   (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" and

 (* small hack: thm 3,5,6 are not needed if rootnormalise is well done*)

  sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>

   (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" and

  sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>

   (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" and

  sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>

   (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" and

  sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>

   (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" and

  (* eliminate isolates sqrt *)

  sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==> 

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

     (a+2*sqrt(a)*sqrt(b)+b  = c+2*sqrt(c)*sqrt(d)+d))" and

  sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==> 

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

     (a - 2*sqrt(a)*sqrt(b)+b  = c+2*sqrt(c)*sqrt(d)+d))" and

  sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==> 

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

     (a + 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))" and

  sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==> 

   ( (sqrt a - sqrt b           = sqrt c - sqrt d) = 

     (a - 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))" and

  sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>

   ( (sqrt (a) = b) = (a = (b \<up> 2)))" and

  sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> 

   ( (c*sqrt(a) = b) = (c \<up> 2*a = b \<up> 2))" and

  sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> 

   ( c/sqrt(a) = b) = (c \<up> 2 / a = b \<up> 2)" and

  (* small hack: thm 4-6 are not needed if rootnormalise is well done*)

  sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> 

   ( (c*(d/sqrt (a)) = b) = (c \<up> 2*(d \<up> 2/a) = b \<up> 2))" and

  sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> 

   ( c/(d*sqrt(a)) = b) = (c \<up> 2 / (d \<up> 2*a) = b \<up> 2)" and

  sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> 

   ( (c*(d/(e*sqrt (a))) = b) = (c \<up> 2*(d \<up> 2/(e \<up> 2*a)) = b \<up> 2))" and

  sqrt_square_equation_right_1:  "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> 

   ( (a = sqrt (b)) = (a \<up> 2 = b))" and

  sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> 

   ( (a = c*sqrt (b)) = ((a \<up> 2) = c \<up> 2*b))" and

  sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> 

   ( (a = c/sqrt (b)) = (a \<up> 2 = c \<up> 2/b))" and

 (* small hack: thm 4-6 are not needed if rootnormalise is well done*)

  sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> 

   ( (a = c*(d/sqrt (b))) = ((a \<up> 2) = c \<up> 2*(d \<up> 2/b)))" and

  sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> 

   ( (a = c/(d*sqrt (b))) = (a \<up> 2 = c \<up> 2/(d \<up> 2*b)))" and

  sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> 

   ( (a = c*(d/(e*sqrt (b)))) = ((a \<up> 2) = c \<up> 2*(d \<up> 2/(e \<up> 2*b))))"

subsection \<open>predicates\<close>

ML \<open>

(* true if bdv is under sqrt of a Equation*)

fun is_rootTerm_in t v = 

  let 

   	fun findroot (t as (_ $ _ $ _ $ _)) _ = raise TERM ( "is_rootTerm_in", [t])

	  (* at the moment there is no term like this, but ....*)

	  | findroot (Const (\<^const_name>\<open>nroot\<close>, _) $ _ $ t3) v = Prog_Expr.occurs_in v t3

	  | findroot (_ $ t2 $ t3) v = findroot t2 v orelse findroot t3 v

	  | findroot (Const (\<^const_name>\<open>sqrt\<close>, _) $ t2) v = Prog_Expr.occurs_in v t2

	  | findroot (_ $ t2) v = findroot t2 v

	  | findroot _ _ = false;

  in

	  findroot t v

  end;

fun is_sqrtTerm_in t v = 

  let 

    fun findsqrt (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_sqrteqation_in", [t])

    (* at the moment there is no term like this, but ....*)

    | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)

    | findsqrt (Const (\<^const_name>\<open>sqrt\<close>, _) $ a) v = Prog_Expr.occurs_in v a

    | findsqrt (_ $ t1) v = findsqrt t1 v

    | findsqrt _ _ = false;

  in

   findsqrt t v

  end;

(* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,

and the subterm ist connected with + or * --> is normalised*)

fun is_normSqrtTerm_in t v =

  let

     fun isnorm (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_normSqrtTerm_in", [t])

         (* at the moment there is no term like this, but ....*)

       | isnorm (Const (\<^const_name>\<open>plus\<close>,_) $ _ $ t2) v = is_sqrtTerm_in t2 v

       | isnorm (Const (\<^const_name>\<open>times\<close>,_) $ _ $ t2) v = is_sqrtTerm_in t2 v

       | isnorm (Const (\<^const_name>\<open>minus\<close>,_) $ _ $ _) _ = false

       | isnorm (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) v =

         is_sqrtTerm_in t1 v orelse is_sqrtTerm_in t2 v

       | isnorm (Const (\<^const_name>\<open>sqrt\<close>, _) $ t1) v = Prog_Expr.occurs_in v t1

	     | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v

       | isnorm _ _ = false;

   in

     isnorm t v

   end;

fun eval_is_rootTerm_in _ _ (p as (Const (\<^const_name>\<open>RootEq.is_rootTerm_in\<close>,_) $ t $ v)) _ =

    if is_rootTerm_in t v

    then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);

fun eval_is_sqrtTerm_in _ _ (p as (Const (\<^const_name>\<open>is_sqrtTerm_in\<close>,_) $ t $ v)) _ =

    if is_sqrtTerm_in t v

    then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);

fun eval_is_normSqrtTerm_in _ _ (p as (Const (\<^const_name>\<open>is_normSqrtTerm_in\<close>,_) $ t $ v)) _ =

    if is_normSqrtTerm_in t v

    then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);

\<close>

calculation is_rootTerm_in = \<open>eval_is_rootTerm_in ""\<close>

calculation is_sqrtTerm_in = \<open>eval_is_sqrtTerm_in ""\<close>

calculation is_normSqrtTerm_in = \<open>eval_is_normSqrtTerm_in ""\<close>

subsection \<open>rule-sets\<close>

ML \<open>

val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)

  Rule_Set.append_rules "RootEq_prls" Rule_Set.empty [

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

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

    \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),

    \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),

    \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),

    \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),

    \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),

    \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),

    \<^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>];

val RootEq_erls =

  Rule_Set.append_rules "RootEq_erls" Root_erls

    [\<^rule_thm>\<open>divide_divide_eq_left\<close>];

val RootEq_crls = 

  Rule_Set.append_rules "RootEq_crls" Root_crls

    [\<^rule_thm>\<open>divide_divide_eq_left\<close>];

val rooteq_srls = 

  Rule_Set.append_rules "rooteq_srls" Rule_Set.empty [

     \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),

     \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in""),

     \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in "")];

\<close>

ML \<open>

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

 val sqrt_isolate = prep_rls'(

  Rule_Def.Repeat {

    id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), 

    asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

    rules = [

       \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)

       \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)

       \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)

       \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)

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

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

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

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

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

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

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

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

       \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)

       \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)

       \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)

       \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)

       \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)

       \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)

       (*

       \<^rule_thm>\<open>sqrt_isolate_l_div\<close>, (* b*sqrt(x) = d sqrt(x) d/b *)*)

       \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)

       \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)

       \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)

       \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)

       \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)

       \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)

       (*

       \<^rule_thm>\<open>sqrt_isolate_r_div\<close>, (* a=e*sqrt(x) -> a/e = sqrt(x) *)*)

       \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, (* sqrt(x)=b -> x=b^2 *)

       \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, (* c*sqrt(x)=b -> c^2*x=b^2 *)

       \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, (* c/sqrt(x)=b -> c^2/x=b^2 *)

       \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)

       \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>, (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)

       \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>, (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)

       \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>, (* a=sqrt(x) ->a^2=x *)

       \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>, (* a=c*sqrt(x) ->a^2=c^2*x *)

       \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>, (* a=c/sqrt(x) ->a^2=c^2/x *)

       \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>, (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)

       \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>, (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)

       \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>], (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)

    program = Rule.Empty_Prog});

\<close> ML \<open>

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

val l_sqrt_isolate = prep_rls'(

  Rule_Def.Repeat {

  id = "l_sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), 

  asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

  rules = [

     \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)

     \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)

     \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)

     \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)

     \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)

     \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)

     \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)

     \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)

     \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)

     \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)

     (*

     \<^rule_thm>\<open>sqrt_isolate_l_div\<close>, (* b*sqrt(x) = d sqrt(x) d/b *)*)

     \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, (* sqrt(x)=b -> x=b^2 *)

     \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, (* a*sqrt(x)=b -> a^2*x=b^2*)

     \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, (* c/sqrt(x)=b -> c^2/x=b^2 *)

     \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)

     \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>, (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)

     \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>], (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)

  program = Rule.Empty_Prog});

\<close> ML \<open>

(* -- right 28.8.02--*)

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

val r_sqrt_isolate = prep_rls'(

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

   asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

   rules = [

     \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)

     \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)

     \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)

     \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)

     \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)

     \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)

     \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)

     \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)

     \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)

     \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)

      (*

     \<^rule_thm>\<open>sqrt_isolate_r_div\<close>, (* a=e*sqrt(x) -> a/e = sqrt(x) *)*)

     \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>, (* a=sqrt(x) ->a^2=x *)

     \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>, (* a=c*sqrt(x) ->a^2=c^2*x *)

     \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>, (* a=c/sqrt(x) ->a^2=c^2/x *)

     \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>, (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)

     \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>, (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)

     \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>], (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)

   program = Rule.Empty_Prog});

\<close> ML \<open>

val rooteq_simplify = prep_rls'(

  Rule_Def.Repeat {

    id = "rooteq_simplify", preconds = [], rew_ord = ("termlessI",termlessI), 

    asm_rls = RootEq_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],

    rules = [

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

      \<^rule_thm>\<open>real_assoc_2\<close>, (* a*(b*c) = a*b*c *)

      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),

      \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),

      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),

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

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

      \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),

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

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

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

      \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt b * sqrt c = sqrt(b*c) *)

      \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a * sqrt a * sqrt b = a * sqrt(a*b) *)

      \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) = a *)

      \<^rule_thm>\<open>sqrt_square_1\<close>], (* sqrt a  \<up>  2 = a *)

    program = Rule.Empty_Prog});

\<close>

rule_set_knowledge

  RootEq_erls = RootEq_erls and

  rooteq_srls = rooteq_srls and

  sqrt_isolate = sqrt_isolate and

  l_sqrt_isolate = l_sqrt_isolate and

  r_sqrt_isolate = r_sqrt_isolate and

  rooteq_simplify = rooteq_simplify

subsection \<open>problems\<close>

problem pbl_equ_univ_root : "rootX/univariate/equation" =

  \<open>RootEq_prls\<close>

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

  Given: "equality e_e" "solveFor v_v"

  Where:

    (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)

    "(lhs e_e) is_rootTerm_in  (v_v::real) |

     (rhs e_e) is_rootTerm_in  (v_v::real)"

  Find: "solutions v_v'i'"

problem pbl_equ_univ_root_sq : "sq/rootX/univariate/equation" =

  \<open>RootEq_prls\<close>

  Method_Ref: "RootEq/solve_sq_root_equation"

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

  Given: "equality e_e" "solveFor v_v"

  Where:

    "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &

       ((lhs e_e) is_normSqrtTerm_in (v_v::real)) )  |

     ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &

       ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"

  Find: "solutions v_v'i'"

(* ---------normalise----------- *)

problem pbl_equ_univ_root_norm : "normalise/rootX/univariate/equation" =

  \<open>RootEq_prls\<close>

  Method_Ref: "RootEq/norm_sq_root_equation"

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

  Given: "equality e_e" "solveFor v_v"

  Where:

    "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &

       Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  |

     ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &

       Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"

  Find: "solutions v_v'i'"

subsection \<open>methods\<close>

method met_rooteq : "RootEq" =

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

    errpats = [], rew_rls = norm_Poly}\<close>

    (*-- normalise 20.10.02 --*)

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

  where

"norm_sqrt_equ e_e v_v = (

  let

    e_e = (

      (Repeat(Try (Rewrite ''makex1_x''))) #>

      (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) #>

      (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>

      (Try (Rewrite_Set ''rooteq_simplify''))

      ) e_e

  in

    SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])

      [BOOL e_e, REAL v_v])"

method met_rooteq_norm : "RootEq/norm_sq_root_equation" =

  \<open>{rew_ord="termlessI", rls'=RootEq_erls, prog_rls=Rule_Set.empty, where_rls=RootEq_prls, calc =[],

    errpats = [], rew_rls = norm_Poly}\<close>

  Program: norm_sqrt_equ.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &

       Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  |

     ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &

       Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"

  Find: "solutions v_v'i'"

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

  where

"solve_sqrt_equ e_e v_v =

  (let

    e_e = (

      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) #> 

      (Try (Rewrite_Set         ''rooteq_simplify'')) #> 

      (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>

      (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;

    L_L =

     (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))               

      then

        SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], [''no_met''])

          [BOOL e_e, REAL v_v]

      else

        SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])

          [BOOL e_e, REAL v_v])

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

method met_rooteq_sq : "RootEq/solve_sq_root_equation" =

  \<open>{rew_ord="termlessI", rls'=RootEq_erls, prog_rls = rooteq_srls, where_rls = RootEq_prls, calc = [],

    errpats = [], rew_rls = norm_Poly}\<close>

  Program: solve_sqrt_equ.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "(((lhs e_e) is_sqrtTerm_in (v_v::real))     &

      ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |

     (((rhs e_e) is_sqrtTerm_in (v_v::real))     &

      ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"

  Find: "solutions v_v'i'"

    (*-- right 28.08.02 --*)

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

  where

"solve_sqrt_equ_right e_e v_v =

  (let

    e_e = (

      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) #>

      (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>

      (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e

  in

    if (rhs e_e) is_sqrtTerm_in v_v

    then

      SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])

        [BOOL e_e, REAL v_v]

    else

      SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])

        [BOOL e_e, REAL v_v])"

method met_rooteq_sq_right : "RootEq/solve_right_sq_root_equation" =

  \<open>{rew_ord = "termlessI", rls' = RootEq_erls, prog_rls = Rule_Set.empty, where_rls = RootEq_prls, calc = [],

    errpats = [], rew_rls = norm_Poly}\<close>

  Program: solve_sqrt_equ_right.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "(rhs e_e) is_sqrtTerm_in v_v"

  Find: "solutions v_v'i'"

    (*-- left 28.08.02 --*)

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

  where

"solve_sqrt_equ_left e_e v_v =

  (let

    e_e = (

      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #> 

      (Try (Rewrite_Set ''rooteq_simplify'')) #>

      (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>

      (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e

  in

    if (lhs e_e) is_sqrtTerm_in v_v

    then

      SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])

        [BOOL e_e, REAL v_v]

    else

      SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])

        [BOOL e_e, REAL v_v])"

method met_rooteq_sq_left : "RootEq/solve_left_sq_root_equation" =

  \<open>{rew_ord="termlessI", rls'=RootEq_erls, prog_rls=Rule_Set.empty, where_rls=RootEq_prls, calc =[],

    errpats = [], rew_rls = norm_Poly}\<close>

  Program: solve_sqrt_equ_left.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "(lhs e_e) is_sqrtTerm_in v_v"

  Find: "solutions v_v'i'"

ML \<open>

\<close> ML \<open>

\<close> 

end