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

(* theory collecting all knowledge for RootEquations

   created by: rlang 

         date: 02.09

   changed by: rlang

   last change by: rlang

             date: 02.11.14

*)

(* use"Knowledge/RootEq.ML";

   use"RootEq.ML";

   use"ROOT.ML";

   cd"knowledge";

   remove_thy"RootEq";

   use_thy"Knowledge/Isac";

   *)

"******* RootEq.ML begin *******";

theory' := overwritel (!theory', [("RootEq.thy",RootEq.thy)]);

(*-------------------------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 = raise 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 ("Root.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 = raise 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 ("Root.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 = raise error("is_normSqrtTerm_in:")

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

          | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v

          | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v

          | isnorm (Const ("op -",_) $ _ $ _) v = false

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

                              (is_sqrtTerm_in t2 v)

          | isnorm (Const ("Root.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, HOLogic.true_const)))

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

	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

  | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### 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, HOLogic.true_const)))

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

	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

  | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### 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, HOLogic.true_const)))

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

	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

  | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### 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 ("op =",eval_equal "#equal_"),

	      Thm ("not_true",num_str not_true),

	      Thm ("not_false",num_str not_false),

	      Thm ("and_true",num_str and_true),

	      Thm ("and_false",num_str and_false),

	      Thm ("or_true",num_str or_true),

	      Thm ("or_false",num_str or_false)

	      ];

val RootEq_erls =

     append_rls "RootEq_erls" Root_erls

          [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)

           ];

val RootEq_crls = 

     append_rls "RootEq_crls" Root_crls

          [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)

           ];

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

		 ];

ruleset' := overwritelthy thy (!ruleset',

			[("RootEq_erls",RootEq_erls), (*FIXXXME:del with rls.rls'*)

			 ("rooteq_srls",rooteq_srls)

                         ]);

(*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 = [], 

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

                  ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),

                  ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),

                  ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""),

                  ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),

                  ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),

                  ("sqrt_square_equation_right_6","")],*)

       rules = [

	      Thm("sqrt_square_1",num_str sqrt_square_1),                            (* (sqrt a)^^^2 -> a *)

	      Thm("sqrt_square_2",num_str sqrt_square_2),                            (* sqrt (a^^^2) -> a *)

	      Thm("sqrt_times_root_1",num_str sqrt_times_root_1),            (* sqrt a sqrt b -> sqrt(ab) *)

	      Thm("sqrt_times_root_2",num_str sqrt_times_root_2),        (* a sqrt b sqrt c -> a sqrt(bc) *)

              Thm("sqrt_square_equation_both_1",num_str 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 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 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 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 sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)

	      Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)

	      Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)

	      Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)

	      Thm("sqrt_isolate_l_add5",num_str 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 sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)

	      (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*)      (* b*sqrt(x) = d sqrt(x) d/b *)

	      Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1),  (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)

	      Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2),  (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)

	      Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3),  (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)

	      Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4),  (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)

	      Thm("sqrt_isolate_r_add5",num_str 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 sqrt_isolate_r_add6),  (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)

	      (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*)   (* a=e*sqrt(x) -> a/e = sqrt(x) *)

	      Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),   

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

	      Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),   

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

	      Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),   

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

	      Thm("sqrt_square_equation_left_4",num_str 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 sqrt_square_equation_left_5),   

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

	      Thm("sqrt_square_equation_left_6",num_str 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 sqrt_square_equation_right_1),   

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

	      Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),   

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

	      Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),   

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

	      Thm("sqrt_square_equation_right_4",num_str 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 sqrt_square_equation_right_5),   

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

	      Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)   

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

	      ],

	 scr = Script ((term_of o the o (parse thy)) "empty_script")

         }:rls);

ruleset' := overwritelthy thy (!ruleset',

			[("sqrt_isolate",sqrt_isolate)

			 ]);

(* -- left 28.08.02--*)

(*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 = [], 

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

                  ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),

                  ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),

                  ("sqrt_square_equation_left_6","")],*)

     rules = [

	      Thm("sqrt_square_1",num_str sqrt_square_1),                            (* (sqrt a)^^^2 -> a *)

	      Thm("sqrt_square_2",num_str sqrt_square_2),                            (* sqrt (a^^^2) -> a *)

	      Thm("sqrt_times_root_1",num_str sqrt_times_root_1),            (* sqrt a sqrt b -> sqrt(ab) *)

	      Thm("sqrt_times_root_2",num_str sqrt_times_root_2),        (* a sqrt b sqrt c -> a sqrt(bc) *)

	      Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)

	      Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)

	      Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)

	      Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)

	      Thm("sqrt_isolate_l_add5",num_str 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 sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)

	      (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*)      (* b*sqrt(x) = d sqrt(x) d/b *)

	      Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),

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

	      Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),

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

	      Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),   

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

	      Thm("sqrt_square_equation_left_4",num_str 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 sqrt_square_equation_left_5),   

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

	      Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6)  

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

	      ],

	 scr = Script ((term_of o the o (parse thy)) "empty_script")

         }:rls);

ruleset' := overwritelthy thy (!ruleset',

			[("l_sqrt_isolate",l_sqrt_isolate)

			 ]);

(* -- 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 = [], 

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

                  ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),

                  ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),

                  ("sqrt_square_equation_right_6","")],*)

     rules = [

	      Thm("sqrt_square_1",num_str sqrt_square_1),                           (* (sqrt a)^^^2 -> a *)

	      Thm("sqrt_square_2",num_str sqrt_square_2),                           (* sqrt (a^^^2) -> a *)

	      Thm("sqrt_times_root_1",num_str sqrt_times_root_1),           (* sqrt a sqrt b -> sqrt(ab) *)

	      Thm("sqrt_times_root_2",num_str sqrt_times_root_2),       (* a sqrt b sqrt c -> a sqrt(bc) *)

	      Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)

	      Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)

	      Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3),  (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)

	      Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4),  (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)

	      Thm("sqrt_isolate_r_add5",num_str 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 sqrt_isolate_r_add6),  (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)

	      (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*)  (* a=e*sqrt(x) -> a/e = sqrt(x) *)

	      Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),

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

	      Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),

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

	      Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),   

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

	      Thm("sqrt_square_equation_right_4",num_str 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 sqrt_square_equation_right_5),   

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

	      Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)   

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

	      ],

	 scr = Script ((term_of o the o (parse thy)) "empty_script")

         }:rls);

ruleset' := overwritelthy thy (!ruleset',

			[("r_sqrt_isolate",r_sqrt_isolate)

			 ]);

val rooteq_simplify = prep_rls(

  Rls {id = "rooteq_simplify", 

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

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

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

       rules = [Thm  ("real_assoc_1",num_str real_assoc_1),                             (* a+(b+c) = a+b+c *)

                Thm  ("real_assoc_2",num_str real_assoc_2),                             (* a*(b*c) = a*b*c *)

                Calc ("op +",eval_binop "#add_"),

                Calc ("op -",eval_binop "#sub_"),

                Calc ("op *",eval_binop "#mult_"),

                Calc ("HOL.divide", eval_cancel "#divide_"),

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

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

                Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2),

                Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2),

                Thm("realpow_mul",num_str realpow_mul),    (* (a * b)^n = a^n * b^n*)

                Thm("sqrt_times_root_1",num_str sqrt_times_root_1),         (* sqrt b * sqrt c = sqrt(b*c) *)

                Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a * sqrt a * sqrt b = a * sqrt(a*b) *)

                Thm("sqrt_square_2",num_str sqrt_square_2),                            (* sqrt (a^^^2) = a *)

                Thm("sqrt_square_1",num_str sqrt_square_1)                             (* sqrt a ^^^ 2 = a *)

                ],

       scr = Script ((term_of o the o (parse thy)) "empty_script")

    }:rls);

  ruleset' := overwritelthy thy (!ruleset',

                          [("rooteq_simplify",rooteq_simplify)

                           ]);

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

(*

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

show_ptyps(); 

*)

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

store_pbt

 (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID

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

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["(lhs e_) is_rootTerm_in  (v_::real) | \

	       \(rhs e_) is_rootTerm_in  (v_::real)"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  RootEq_prls, SOME "solve (e_::bool, v_)",

  []));

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

store_pbt

 (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID

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

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\

               \  ((lhs e_) is_normSqrtTerm_in (v_::real))   )  |\

	       \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\

               \  ((rhs e_) is_normSqrtTerm_in (v_::real))   )"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  RootEq_prls,  SOME "solve (e_::bool, v_)",

  [["RootEq","solve_sq_root_equation"]]));

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

store_pbt

 (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID

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

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\

               \  Not((lhs e_) is_normSqrtTerm_in (v_::real)))  | \

	       \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\

               \  Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),

   ("#Find"  ,["solutions v_i_"]) 

  ],

  RootEq_prls,  SOME "solve (e_::bool, v_)",

  [["RootEq","norm_sq_root_equation"]]));

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

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

store_met

 (prep_met RootEq.thy "met_rooteq" [] e_metID

 (["RootEq"],

   [],

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

    crls=RootEq_crls, nrls=norm_Poly(*,

    asm_rls=[],asm_thm=[]*)}, "empty_script"));

(*-- normalize 20.10.02 --*)

store_met

 (prep_met RootEq.thy "met_rooteq_norm" [] e_metID

 (["RootEq","norm_sq_root_equation"],

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\

               \  Not((lhs e_) is_normSqrtTerm_in (v_::real)))  | \

	       \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\

               \  Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),

    ("#Find"  ,["solutions v_i_"])

   ],

   {rew_ord'="termlessI",

    rls'=RootEq_erls,

    srls=e_rls,

    prls=RootEq_prls,

    calc=[],

    crls=RootEq_crls, nrls=norm_Poly(*,

    asm_rls=[],

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

   "Script Norm_sq_root_equation  (e_::bool) (v_::real)  =                \

    \(let 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_ \

    \ in ((SubProblem (RootEq_,[univariate,equation],                     \

    \      [no_met]) [bool_ e_, real_ v_])))"

   ));

store_met

 (prep_met RootEq.thy "met_rooteq_sq" [] e_metID

 (["RootEq","solve_sq_root_equation"],

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\

                \  ((lhs e_) is_normSqrtTerm_in (v_::real))   )  |\

	        \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\

                \  ((rhs e_) is_normSqrtTerm_in (v_::real))   )"]),

    ("#Find"  ,["solutions v_i_"])

   ],

   {rew_ord'="termlessI",

    rls'=RootEq_erls,

    srls = rooteq_srls,

    prls = RootEq_prls,

    calc = [],

    crls=RootEq_crls, nrls=norm_Poly(*,

    asm_rls = [],

    asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),

               ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),

               ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),

               ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""),

               ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),

               ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),

               ("sqrt_square_equation_right_6","")]*)},

"Script Solve_sq_root_equation  (e_::bool) (v_::real)  =             \

\(let e_ = \

\  ((Try (Rewrite_Set_Inst [(bdv,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_;\

\ (L_::bool list) =                                                   \

\    (if (((lhs e_) is_sqrtTerm_in v_) | ((rhs e_) is_sqrtTerm_in v_))\

\ then (SubProblem (RootEq_,[normalize,root,univariate,equation],          \

\       [no_met]) [bool_ e_, real_ v_])                                    \

\ else (SubProblem (RootEq_,[univariate,equation],                         \

\        [no_met]) [bool_ e_, real_ v_]))                                  \

\ in Check_elementwise L_ {(v_::real). Assumptions})"

 ));

(*-- right 28.08.02 --*)

store_met

 (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID

 (["RootEq","solve_right_sq_root_equation"],

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),

    ("#Find"  ,["solutions v_i_"])

   ],

   {rew_ord'="termlessI",

    rls'=RootEq_erls,

    srls=e_rls,

    prls=RootEq_prls,

    calc=[],

    crls=RootEq_crls, nrls=norm_Poly(*,

    asm_rls=[],

    asm_thm=[("sqrt_square_1",""),("sqrt_square_1",""),("sqrt_square_equation_right_1",""),

             ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),

             ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),

             ("sqrt_square_equation_right_6","")]*)},

  "Script Solve_right_sq_root_equation  (e_::bool) (v_::real)  =                   \

    \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,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_\

    \ in if ((rhs e_) is_sqrtTerm_in v_)                                     \ 

    \ then (SubProblem (RootEq_,[normalize,root,univariate,equation],            \

    \       [no_met]) [bool_ e_, real_ v_])                              \

    \ else ((SubProblem (RootEq_,[univariate,equation],                          \

    \        [no_met]) [bool_ e_, real_ v_])))"

 ));

(*-- left 28.08.02 --*)

store_met

 (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID

 (["RootEq","solve_left_sq_root_equation"],

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),

    ("#Find"  ,["solutions v_i_"])

   ],

   {rew_ord'="termlessI",

    rls'=RootEq_erls,

    srls=e_rls,

    prls=RootEq_prls,

    calc=[],

    crls=RootEq_crls, nrls=norm_Poly(*,

    asm_rls=[],

    asm_thm=[("sqrt_square_1",""),("sqrt_square_equation_left_1",""),

             ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),

             ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),

             ("sqrt_square_equation_left_6","")]*)},

    "Script Solve_left_sq_root_equation  (e_::bool) (v_::real)  =                  \

    \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,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_\

    \ in if ((lhs e_) is_sqrtTerm_in v_)                                           \ 

    \ then (SubProblem (RootEq_,[normalize,root,univariate,equation],              \

    \       [no_met]) [bool_ e_, real_ v_])                                        \

    \ else ((SubProblem (RootEq_,[univariate,equation],                            \

    \        [no_met]) [bool_ e_, real_ v_])))"

   ));

calclist':= overwritel (!calclist', 

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

    ]);(*("", ("", "")),*)

"******* RootEq.ML end *******";