(*.(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 {* 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.

*}

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

  (*----------------------scripts-----------------------*)

  Norm'_sq'_root'_equation

             :: "[bool,real, 

		   bool list] => bool list"

               ("((Script Norm'_sq'_root'_equation (_ _ =))// (_))" 9)

  Solve'_sq'_root'_equation

             :: "[bool,real, 

		   bool list] => bool list"

               ("((Script Solve'_sq'_root'_equation (_ _ =))// (_))" 9)

  Solve'_left'_sq'_root'_equation

             :: "[bool,real, 

		   bool list] => bool list"

               ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// (_))" 9)

  Solve'_right'_sq'_root'_equation

             :: "[bool,real, 

		   bool list] => bool list"

               ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// (_))" 9)

axiomatization where

(* normalize *)

  makex1_x:            "a^^^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)^^^2 = a" and

  sqrt_square_2:       "sqrt (a ^^^ 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 rootnormalize 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^^^2)))" and

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

   ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" and

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

   ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" and

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

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

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

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

   ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^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^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" and

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

   ( (a = sqrt (b)) = (a^^^2 = b))" and

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

   ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" and

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

   ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" and

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

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

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

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

   ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^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^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"

ML {*

val thy = @{theory};

(*-------------------------functions---------------------*)

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

fun is_rootTerm_in t v = 

    let 

	fun coeff_in c v = member op = (vars c) v;

   	fun findroot (_ $ _ $ _ $ _) v = error("is_rootTerm_in:")

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

	  | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v

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

	  | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v

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

	  | findroot _ _ = false;

     in

	findroot t v

    end;

 fun is_sqrtTerm_in t v = 

    let 

	fun coeff_in c v = member op = (vars c) v;

   	fun findsqrt (_ $ _ $ _ $ _) v = error("is_sqrteqation_in:")

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

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

	  | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v

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

 fun is_normSqrtTerm_in t v =

     let

	fun coeff_in c v = member op = (vars c) v;

        fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:")

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

          | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v

          | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v

          | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false

          | isnorm (Const ("Rings.divide_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 

                              (is_sqrtTerm_in t2 v)

          | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v

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

          | isnorm _ _ = false;

     in

         isnorm t v

     end;

fun eval_is_rootTerm_in _ _ 

       (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _  =

    if is_rootTerm_in t v then 

	SOME ((term2str p) ^ " = True",

	      Trueprop $ (mk_equality (p, @{term True})))

    else SOME ((term2str p) ^ " = True",

	       Trueprop $ (mk_equality (p, @{term False})))

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

fun eval_is_sqrtTerm_in _ _ 

       (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _  =

    if is_sqrtTerm_in t v then 

	SOME ((term2str p) ^ " = True",

	      Trueprop $ (mk_equality (p, @{term True})))

    else SOME ((term2str p) ^ " = True",

	       Trueprop $ (mk_equality (p, @{term False})))

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

fun eval_is_normSqrtTerm_in _ _ 

       (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _  =

    if is_normSqrtTerm_in t v then 

	SOME ((term2str p) ^ " = True",

	      Trueprop $ (mk_equality (p, @{term True})))

    else SOME ((term2str p) ^ " = True",

	       Trueprop $ (mk_equality (p, @{term False})))

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

(*-------------------------rulse-------------------------*)

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

  append_rls "RootEq_prls" e_rls 

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

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

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

	      Calc ("Tools.rhs"    ,eval_rhs ""),

	      Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),

	      Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),

	      Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),

	      Calc ("HOL.eq",eval_equal "#equal_"),

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

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

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

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

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

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

	      ];

val RootEq_erls =

     append_rls "RootEq_erls" Root_erls

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

           ];

val RootEq_crls = 

     append_rls "RootEq_crls" Root_crls

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

           ];

val rooteq_srls = 

     append_rls "rooteq_srls" e_rls

		[Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),

                 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),

                 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")

		 ];

*}

setup {* KEStore_Elems.add_rlss 

  [("RootEq_erls", (Context.theory_name @{theory}, RootEq_erls)), 

  ("rooteq_srls", (Context.theory_name @{theory}, rooteq_srls))] *}

ML {*

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

 val sqrt_isolate = prep_rls'(

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

       erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],

       rules = [

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

                     (* (sqrt a)^^^2 -> a *)

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

                     (* sqrt (a^^^2) -> a *)

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

            (* sqrt a sqrt b -> sqrt(ab) *)

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

            (* a sqrt b sqrt c -> a sqrt(bc) *)

       Thm("sqrt_square_equation_both_1",

           num_str @{thm sqrt_square_equation_both_1}),

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

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

       Thm("sqrt_square_equation_both_2",

            num_str @{thm sqrt_square_equation_both_2}),

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

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

       Thm("sqrt_square_equation_both_3",

            num_str @{thm sqrt_square_equation_both_3}),

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

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

       Thm("sqrt_square_equation_both_4",

            num_str @{thm sqrt_square_equation_both_4}),

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

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

       Thm("sqrt_isolate_l_add1",

            num_str @{thm sqrt_isolate_l_add1}), 

       (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)

       Thm("sqrt_isolate_l_add2",

            num_str @{thm sqrt_isolate_l_add2}), 

       (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)

       Thm("sqrt_isolate_l_add3",

            num_str @{thm sqrt_isolate_l_add3}), 

       (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)

       Thm("sqrt_isolate_l_add4",

            num_str @{thm sqrt_isolate_l_add4}), 

       (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)

       Thm("sqrt_isolate_l_add5",

            num_str @{thm sqrt_isolate_l_add5}), 

       (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)

       Thm("sqrt_isolate_l_add6",

            num_str @{thm sqrt_isolate_l_add6}), 

       (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)

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

         (* b*sqrt(x) = d sqrt(x) d/b *)

       Thm("sqrt_isolate_r_add1",

            num_str @{thm sqrt_isolate_r_add1}),

       (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)

       Thm("sqrt_isolate_r_add2",

            num_str @{thm sqrt_isolate_r_add2}),

       (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)

       Thm("sqrt_isolate_r_add3",

            num_str @{thm sqrt_isolate_r_add3}),

       (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)

       Thm("sqrt_isolate_r_add4",

            num_str @{thm sqrt_isolate_r_add4}),

       (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)

       Thm("sqrt_isolate_r_add5",

            num_str @{thm sqrt_isolate_r_add5}),

       (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)

       Thm("sqrt_isolate_r_add6",

            num_str @{thm sqrt_isolate_r_add6}),

       (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)

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

         (* a=e*sqrt(x) -> a/e = sqrt(x) *)

       Thm("sqrt_square_equation_left_1",

            num_str @{thm sqrt_square_equation_left_1}),   

       (* sqrt(x)=b -> x=b^2 *)

       Thm("sqrt_square_equation_left_2",

            num_str @{thm sqrt_square_equation_left_2}),   

       (* c*sqrt(x)=b -> c^2*x=b^2 *)

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

	      (* c/sqrt(x)=b -> c^2/x=b^2 *)

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

	      (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)

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

	      (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)

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

	      (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)

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

	      (* a=sqrt(x) ->a^2=x *)

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

	      (* a=c*sqrt(x) ->a^2=c^2*x *)

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

	      (* a=c/sqrt(x) ->a^2=c^2/x *)

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

	      (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)

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

	      (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)

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

	      (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)

       ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")

      }:rls);

*}

setup {* KEStore_Elems.add_rlss

  [("sqrt_isolate", (Context.theory_name @{theory}, sqrt_isolate))] *}

ML {*

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

 val l_sqrt_isolate = prep_rls'(

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

	  rew_ord = ("termlessI",termlessI), 

          erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],

     rules = [

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

                            (* (sqrt a)^^^2 -> a *)

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

                            (* sqrt (a^^^2) -> a *)

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

            (* sqrt a sqrt b -> sqrt(ab) *)

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

        (* a sqrt b sqrt c -> a sqrt(bc) *)

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

        (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)

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

        (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)

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

        (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)

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

        (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)

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

        (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)

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

        (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)

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

        (* b*sqrt(x) = d sqrt(x) d/b *)

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

	      (* sqrt(x)=b -> x=b^2 *)

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

	      (* a*sqrt(x)=b -> a^2*x=b^2*)

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

	      (* c/sqrt(x)=b -> c^2/x=b^2 *)

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

	      (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)

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

	      (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)

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

	      (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)

    ],

    scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")

   }:rls);

*}

setup {* KEStore_Elems.add_rlss

  [("l_sqrt_isolate", (Context.theory_name @{theory}, l_sqrt_isolate))] *}

ML {*

(* -- right 28.8.02--*)

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

 val r_sqrt_isolate = prep_rls'(

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

	  rew_ord = ("termlessI",termlessI), 

          erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],

     rules = [

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

                           (* (sqrt a)^^^2 -> a *)

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

                           (* sqrt (a^^^2) -> a *)

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

           (* sqrt a sqrt b -> sqrt(ab) *)

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

       (* a sqrt b sqrt c -> a sqrt(bc) *)

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

       (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)

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

       (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)

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

       (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)

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

       (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)

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

       (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)

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

       (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)

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

       (* a=e*sqrt(x) -> a/e = sqrt(x) *)

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

	      (* a=sqrt(x) ->a^2=x *)

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

	      (* a=c*sqrt(x) ->a^2=c^2*x *)

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

	      (* a=c/sqrt(x) ->a^2=c^2/x *)

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

	      (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)

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

	      (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)

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

	      (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)

    ],

    scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")

   }:rls);

*}

setup {* KEStore_Elems.add_rlss

  [("r_sqrt_isolate", (Context.theory_name @{theory}, r_sqrt_isolate))] *}

ML {*

val rooteq_simplify = prep_rls'(

  Rls {id = "rooteq_simplify", 

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

       erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],

       (*asm_thm = [("sqrt_square_1","")],*)

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

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

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

                             (* a*(b*c) = a*b*c *)

                Calc ("Groups.plus_class.plus",eval_binop "#add_"),

                Calc ("Groups.minus_class.minus",eval_binop "#sub_"),

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

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

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

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

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

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

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

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

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

                     (* sqrt b * sqrt c = sqrt(b*c) *)

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

                     (* a * sqrt a * sqrt b = a * sqrt(a*b) *)

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

                            (* sqrt (a^^^2) = a *)

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

                            (* sqrt a ^^^ 2 = a *)

                ],

       scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")

    }:rls);

*}

setup {* KEStore_Elems.add_rlss

  [("rooteq_simplify", (Context.theory_name @{theory}, rooteq_simplify))] *}

ML {*

(*-------------------------Problem-----------------------*)

(*

(get_pbt ["root'","univariate","equation"]);

show_ptyps(); 

*)

*}

setup {* KEStore_Elems.add_pbts

  (* ---------root----------- *)

  [(Specify.prep_pbt thy "pbl_equ_univ_root" [] e_pblID

      (["root'","univariate","equation"],

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

          ("#Where" ,["(lhs e_e) is_rootTerm_in  (v_v::real) | " ^

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

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

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

    (* ---------sqrt----------- *)

    (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID

      (["sq","root'","univariate","equation"],

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

          RootEq_prls,  SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])),

    (* ---------normalize----------- *)

    (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID

      (["normalize","root'","univariate","equation"],

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

        RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","norm_sq_root_equation"]]))] *}

(*-------------------------methods-----------------------*)

setup {* KEStore_Elems.add_mets

  [(* ---- root 20.8.02 ---*)

    Specify.prep_met thy "met_rooteq" [] e_metID

      (["RootEq"], [],

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

          crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"),

    (*-- normalize 20.10.02 --*)

    Specify.prep_met thy "met_rooteq_norm" [] e_metID

      (["RootEq","norm_sq_root_equation"],

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

        {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[],

          crls=RootEq_crls, errpats = [], nrls = norm_Poly},

        "Script Norm_sq_root_equation  (e_e::bool) (v_v::real)  =                " ^

          "(let e_e = ((Repeat(Try (Rewrite     makex1_x            False))) @@  " ^

          "           (Try (Repeat (Rewrite_Set expand_rootbinoms  False))) @@  " ^ 

          "           (Try (Rewrite_Set rooteq_simplify              True)) @@  " ^ 

          "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^

          "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^

          " in ((SubProblem (RootEq',[univariate,equation],                     " ^

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

(*----- broke at Isabelle2015 \<longrightarrow> Isabelle2017, reason unknown -----

,

    Specify.prep_met thy "met_rooteq_sq" [] e_metID

      (["RootEq","solve_sq_root_equation"],

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

        {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],

          crls=RootEq_crls, errpats = [], nrls = norm_Poly},

        "Script Solve_sq_root_equation  (e_e::bool) (v_v::real)  =               " ^

          "(let e_e =                                                              " ^

          "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@      " ^

          "   (Try (Rewrite_Set         rooteq_simplify True))             @@      " ^

          "   (Try (Repeat (Rewrite_Set expand_rootbinoms         False))) @@      " ^

          "   (Try (Repeat (Rewrite_Set make_rooteq               False))) @@      " ^

          "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^

          " (L_L::bool list) =                                                     " ^

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

          "    then (SubProblem (RootEq',[normalize,root',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})"),

    (*-- right 28.08.02 --*)

    Specify.prep_met thy "met_rooteq_sq_right" [] e_metID

      (["RootEq","solve_right_sq_root_equation"],

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

          ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),

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

        {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, prls = RootEq_prls, calc = [],

          crls = RootEq_crls, errpats = [], nrls = norm_Poly},

        "Script Solve_right_sq_root_equation  (e_e::bool) (v_v::real)  =           " ^

          "(let e_e =                                                               " ^

          "    ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate  False)) @@ " ^

          "    (Try (Rewrite_Set                       rooteq_simplify False)) @@   " ^

          "    (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@   " ^

          "    (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@   " ^

          "    (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^

          " in if ((rhs e_e) is_sqrtTerm_in v_v)                                    " ^

          " then (SubProblem (RootEq',[normalize,root',univariate,equation],       " ^

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

          " else ((SubProblem (RootEq',[univariate,equation],                      " ^

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

    (*-- left 28.08.02 --*)

    Specify.prep_met thy "met_rooteq_sq_left" [] e_metID

      (["RootEq","solve_left_sq_root_equation"],

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

          ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),

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

        {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[],

          crls=RootEq_crls, errpats = [], nrls = norm_Poly},

        "Script Solve_left_sq_root_equation  (e_e::bool) (v_v::real)  =          " ^

          "(let e_e =                                                             " ^

          "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate  False)) @@ " ^

          "  (Try (Rewrite_Set                       rooteq_simplify False)) @@  " ^

          "  (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@  " ^

          "  (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@  " ^

          "  (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^

          " in if ((lhs e_e) is_sqrtTerm_in v_v)                                   " ^ 

          " then (SubProblem (RootEq',[normalize,root',univariate,equation],      " ^

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

          " else ((SubProblem (RootEq',[univariate,equation],                    " ^

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

----- broke at Isabelle2015 \<longrightarrow> Isabelle2017, reason unknown  -------*)

] 

*}

setup {* KEStore_Elems.add_calcs

  [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),

    ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", eval_is_sqrtTerm_in"")),

    ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""))] *}

end