
neuper@37906: (*.(c) by Richard Lang, 2003 .*)
neuper@37906: (* collecting all knowledge for Root Equations
neuper@37906:    created by: rlang 
neuper@37906:          date: 02.08
neuper@37906:    changed by: rlang
neuper@37906:    last change by: rlang
neuper@37906:              date: 02.11.14
neuper@37906: *)
neuper@37906: 
neuper@37985: theory RootEq imports Root begin
neuper@37906: 
neuper@37906: consts
neuper@37985: 
neuper@37985:   is'_rootTerm'_in     :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
neuper@37950:   is'_sqrtTerm'_in     :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _") 
neuper@37950:   is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _") 
neuper@37950: 
neuper@37906:   (*----------------------scripts-----------------------*)
neuper@37906:   Norm'_sq'_root'_equation
neuper@37950:              :: "[bool,real, 
neuper@37950: 		   bool list] => bool list"
neuper@37950:                ("((Script Norm'_sq'_root'_equation (_ _ =))// 
neuper@37950:                   (_))" 9)
neuper@37906:   Solve'_sq'_root'_equation
neuper@37950:              :: "[bool,real, 
neuper@37950: 		   bool list] => bool list"
neuper@37950:                ("((Script Solve'_sq'_root'_equation (_ _ =))// 
neuper@37950:                   (_))" 9)
neuper@37906:   Solve'_left'_sq'_root'_equation
neuper@37950:              :: "[bool,real, 
neuper@37950: 		   bool list] => bool list"
neuper@37950:                ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// 
neuper@37950:                   (_))" 9)
neuper@37906:   Solve'_right'_sq'_root'_equation
neuper@37950:              :: "[bool,real, 
neuper@37950: 		   bool list] => bool list"
neuper@37950:                ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// 
neuper@37950:                   (_))" 9)
neuper@37906:  
neuper@37950: axioms 
neuper@37906: 
neuper@37906: (* normalize *)
neuper@37983:   makex1_x:            "a^^^1  = a"  
neuper@37983:   real_assoc_1:        "a+(b+c) = a+b+c"
neuper@37983:   real_assoc_2:        "a*(b*c) = a*b*c"
neuper@37906: 
neuper@37906:   (* simplification of root*)
neuper@37983:   sqrt_square_1:       "[|0 <= a|] ==>  (sqrt a)^^^2 = a"
neuper@37983:   sqrt_square_2:       "sqrt (a ^^^ 2) = a"
neuper@37983:   sqrt_times_root_1:   "sqrt a * sqrt b = sqrt(a*b)"
neuper@37983:   sqrt_times_root_2:   "a * sqrt b * sqrt c = a * sqrt(b*c)"
neuper@37906: 
neuper@37906:   (* isolate one root on the LEFT or RIGHT hand side of the equation *)
neuper@37983:   sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==> 
neuper@37950:    (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
neuper@37983:   sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
neuper@37950:    (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
neuper@37983:   sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
neuper@37950:    (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)"
neuper@37983:   sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
neuper@37950:    (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)"
neuper@37983:   sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
neuper@37950:    (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
neuper@37983:   sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
neuper@37950:    (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
neuper@37983:   sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
neuper@37950:    (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
neuper@37983:   sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
neuper@37950:    (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
neuper@37906:  (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
neuper@37983:   sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
neuper@37950:    (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
neuper@37983:   sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
neuper@37950:    (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
neuper@37983:   sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
neuper@37950:    (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
neuper@37983:   sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
neuper@37950:    (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
neuper@37906:  
neuper@37906:   (* eliminate isolates sqrt *)
neuper@37983:   sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==> 
neuper@37950:    ( (sqrt a + sqrt b         = sqrt c + sqrt d) = 
neuper@37950:      (a+2*sqrt(a)*sqrt(b)+b  = c+2*sqrt(c)*sqrt(d)+d))"
neuper@37983:   sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==> 
neuper@37950:    ( (sqrt a - sqrt b           = sqrt c + sqrt d) = 
neuper@37950:      (a - 2*sqrt(a)*sqrt(b)+b  = c+2*sqrt(c)*sqrt(d)+d))"
neuper@37983:   sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==> 
neuper@37950:    ( (sqrt a + sqrt b           = sqrt c - sqrt d) = 
neuper@37950:      (a + 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))"
neuper@37983:   sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==> 
neuper@37950:    ( (sqrt a - sqrt b           = sqrt c - sqrt d) = 
neuper@37950:      (a - 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))"
neuper@37983:   sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
neuper@37950:    ( (sqrt (a) = b) = (a = (b^^^2)))"
neuper@37983:   sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> 
neuper@37950:    ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
neuper@37983:   sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> 
neuper@37950:    ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
neuper@37906:   (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
neuper@37983:   sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> 
neuper@37950:    ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
neuper@37983:   sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> 
neuper@37950:    ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
neuper@37983:   sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> 
neuper@37950:    ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
neuper@37983:   sqrt_square_equation_right_1:  "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> 
neuper@37950:    ( (a = sqrt (b)) = (a^^^2 = b))"
neuper@37983:   sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> 
neuper@37950:    ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
neuper@37983:   sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> 
neuper@37950:    ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
neuper@37906:  (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
neuper@37983:   sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> 
neuper@37950:    ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
neuper@37983:   sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> 
neuper@37950:    ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
neuper@37983:   sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> 
neuper@37950:    ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
neuper@37950: 
neuper@37950: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37950: (*-------------------------functions---------------------*)
neuper@37950: (* true if bdv is under sqrt of a Equation*)
neuper@37950: fun is_rootTerm_in t v = 
neuper@37950:     let 
neuper@37950: 	fun coeff_in c v = member op = (vars c) v;
neuper@37950:    	fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
neuper@37950: 	  (* at the moment there is no term like this, but ....*)
neuper@37950: 	  | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
neuper@37950: 	  | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
neuper@37982: 	  | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v
neuper@37950: 	  | findroot (_ $ t2) v = (findroot t2 v)
neuper@37950: 	  | findroot _ _ = false;
neuper@37950:      in
neuper@37950: 	findroot t v
neuper@37950:     end;
neuper@37950: 
neuper@37950:  fun is_sqrtTerm_in t v = 
neuper@37950:     let 
neuper@37950: 	fun coeff_in c v = member op = (vars c) v;
neuper@37950:    	fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
neuper@37950: 	  (* at the moment there is no term like this, but ....*)
neuper@37950: 	  | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
neuper@37982: 	  | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v
neuper@37950: 	  | findsqrt (_ $ t1) v = (findsqrt t1 v)
neuper@37950: 	  | findsqrt _ _ = false;
neuper@37950:      in
neuper@37950: 	findsqrt t v
neuper@37950:     end;
neuper@37950: 
neuper@37950: (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
neuper@37950: and the subterm ist connected with + or * --> is normalized*)
neuper@37950:  fun is_normSqrtTerm_in t v =
neuper@37950:      let
neuper@37950: 	fun coeff_in c v = member op = (vars c) v;
neuper@37950:         fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
neuper@37950: 	  (* at the moment there is no term like this, but ....*)
neuper@37950:           | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
neuper@37950:           | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
neuper@37950:           | isnorm (Const ("op -",_) $ _ $ _) v = false
neuper@37950:           | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse 
neuper@37950:                               (is_sqrtTerm_in t2 v)
neuper@37982:           | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
neuper@37950:  	  | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
neuper@37950:           | isnorm _ _ = false;
neuper@37950:      in
neuper@37950:          isnorm t v
neuper@37950:      end;
neuper@37950: 
neuper@37950: fun eval_is_rootTerm_in _ _ 
neuper@37950:        (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _  =
neuper@37950:     if is_rootTerm_in t v then 
neuper@37950: 	SOME ((term2str p) ^ " = True",
neuper@37950: 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = True",
neuper@37950: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:   | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
neuper@37950: 
neuper@37950: fun eval_is_sqrtTerm_in _ _ 
neuper@37950:        (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _  =
neuper@37950:     if is_sqrtTerm_in t v then 
neuper@37950: 	SOME ((term2str p) ^ " = True",
neuper@37950: 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = True",
neuper@37950: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:   | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
neuper@37950: 
neuper@37950: fun eval_is_normSqrtTerm_in _ _ 
neuper@37950:        (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _  =
neuper@37950:     if is_normSqrtTerm_in t v then 
neuper@37950: 	SOME ((term2str p) ^ " = True",
neuper@37950: 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = True",
neuper@37950: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:   | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
neuper@37950: 
neuper@37950: (*-------------------------rulse-------------------------*)
neuper@37950: val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
neuper@37950:   append_rls "RootEq_prls" e_rls 
neuper@37950: 	     [Calc ("Atools.ident",eval_ident "#ident_"),
neuper@37950: 	      Calc ("Tools.matches",eval_matches ""),
neuper@37950: 	      Calc ("Tools.lhs"    ,eval_lhs ""),
neuper@37950: 	      Calc ("Tools.rhs"    ,eval_rhs ""),
neuper@37950: 	      Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
neuper@37950: 	      Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
neuper@37950: 	      Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
neuper@37950: 	      Calc ("op =",eval_equal "#equal_"),
neuper@37969: 	      Thm ("not_true",num_str @{thm not_true}),
neuper@37969: 	      Thm ("not_false",num_str @{thm not_false}),
neuper@37969: 	      Thm ("and_true",num_str @{thm and_true}),
neuper@37969: 	      Thm ("and_false",num_str @{thm and_false}),
neuper@37969: 	      Thm ("or_true",num_str @{thm or_true}),
neuper@37969: 	      Thm ("or_false",num_str @{thm or_false})
neuper@37950: 	      ];
neuper@37950: 
neuper@37950: val RootEq_erls =
neuper@37950:      append_rls "RootEq_erls" Root_erls
neuper@37965:           [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
neuper@37950:            ];
neuper@37950: 
neuper@37950: val RootEq_crls = 
neuper@37950:      append_rls "RootEq_crls" Root_crls
neuper@37965:           [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
neuper@37950:            ];
neuper@37950: 
neuper@37950: val rooteq_srls = 
neuper@37950:      append_rls "rooteq_srls" e_rls
neuper@37950: 		[Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
neuper@37950:                  Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),
neuper@37950:                  Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
neuper@37950: 		 ];
neuper@37950: 
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37950: 			[("RootEq_erls",RootEq_erls),
neuper@37950:                                              (*FIXXXME:del with rls.rls'*)
neuper@37950: 			 ("rooteq_srls",rooteq_srls)
neuper@37950:                          ]);
neuper@37950: 
neuper@37950: (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
neuper@37950:  val sqrt_isolate = prep_rls(
neuper@37950:   Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37950:        erls = RootEq_erls, srls = Erls, calc = [], 
neuper@37950:        rules = [
neuper@37969:        Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
neuper@37950:                      (* (sqrt a)^^^2 -> a *)
neuper@37969:        Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
neuper@37950:                      (* sqrt (a^^^2) -> a *)
neuper@37969:        Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
neuper@37950:             (* sqrt a sqrt b -> sqrt(ab) *)
neuper@37969:        Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
neuper@37950:             (* a sqrt b sqrt c -> a sqrt(bc) *)
neuper@37950:        Thm("sqrt_square_equation_both_1",
neuper@37969:            num_str @{thm sqrt_square_equation_both_1}),
neuper@37950:        (* (sqrt a + sqrt b  = sqrt c + sqrt d) -> 
neuper@37950:             (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
neuper@37950:        Thm("sqrt_square_equation_both_2",
neuper@37969:             num_str @{thm sqrt_square_equation_both_2}),
neuper@37950:        (* (sqrt a - sqrt b  = sqrt c + sqrt d) -> 
neuper@37950:             (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
neuper@37950:        Thm("sqrt_square_equation_both_3",
neuper@37969:             num_str @{thm sqrt_square_equation_both_3}),
neuper@37950:        (* (sqrt a + sqrt b  = sqrt c - sqrt d) -> 
neuper@37950:             (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
neuper@37950:        Thm("sqrt_square_equation_both_4",
neuper@37969:             num_str @{thm sqrt_square_equation_both_4}),
neuper@37950:        (* (sqrt a - sqrt b  = sqrt c - sqrt d) -> 
neuper@37950:             (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
neuper@37950:        Thm("sqrt_isolate_l_add1",
neuper@37969:             num_str @{thm sqrt_isolate_l_add1}), 
neuper@37950:        (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
neuper@37950:        Thm("sqrt_isolate_l_add2",
neuper@37969:             num_str @{thm sqrt_isolate_l_add2}), 
neuper@37950:        (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)
neuper@37950:        Thm("sqrt_isolate_l_add3",
neuper@37969:             num_str @{thm sqrt_isolate_l_add3}), 
neuper@37950:        (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
neuper@37950:        Thm("sqrt_isolate_l_add4",
neuper@37969:             num_str @{thm sqrt_isolate_l_add4}), 
neuper@37950:        (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
neuper@37950:        Thm("sqrt_isolate_l_add5",
neuper@37969:             num_str @{thm sqrt_isolate_l_add5}), 
neuper@37950:        (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
neuper@37950:        Thm("sqrt_isolate_l_add6",
neuper@37969:             num_str @{thm sqrt_isolate_l_add6}), 
neuper@37950:        (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
neuper@37969:        (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*)
neuper@37950:          (* b*sqrt(x) = d sqrt(x) d/b *)
neuper@37950:        Thm("sqrt_isolate_r_add1",
neuper@37969:             num_str @{thm sqrt_isolate_r_add1}),
neuper@37950:        (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
neuper@37950:        Thm("sqrt_isolate_r_add2",
neuper@37969:             num_str @{thm sqrt_isolate_r_add2}),
neuper@37950:        (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)
neuper@37950:        Thm("sqrt_isolate_r_add3",
neuper@37969:             num_str @{thm sqrt_isolate_r_add3}),
neuper@37950:        (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
neuper@37950:        Thm("sqrt_isolate_r_add4",
neuper@37969:             num_str @{thm sqrt_isolate_r_add4}),
neuper@37950:        (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
neuper@37950:        Thm("sqrt_isolate_r_add5",
neuper@37969:             num_str @{thm sqrt_isolate_r_add5}),
neuper@37950:        (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
neuper@37950:        Thm("sqrt_isolate_r_add6",
neuper@37969:             num_str @{thm sqrt_isolate_r_add6}),
neuper@37950:        (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
neuper@37969:        (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*)
neuper@37950:          (* a=e*sqrt(x) -> a/e = sqrt(x) *)
neuper@37950:        Thm("sqrt_square_equation_left_1",
neuper@37969:             num_str @{thm sqrt_square_equation_left_1}),   
neuper@37950:        (* sqrt(x)=b -> x=b^2 *)
neuper@37950:        Thm("sqrt_square_equation_left_2",
neuper@37969:             num_str @{thm sqrt_square_equation_left_2}),   
neuper@37950:        (* c*sqrt(x)=b -> c^2*x=b^2 *)
neuper@37969:        Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}),  
neuper@37950: 	      (* c/sqrt(x)=b -> c^2/x=b^2 *)
neuper@37969:        Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}),
neuper@37950: 	      (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
neuper@37969:        Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}),
neuper@37950: 	      (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
neuper@37969:        Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6}),
neuper@37950: 	      (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
neuper@37969:        Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}),
neuper@37950: 	      (* a=sqrt(x) ->a^2=x *)
neuper@37969:        Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}),
neuper@37950: 	      (* a=c*sqrt(x) ->a^2=c^2*x *)
neuper@37969:        Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}),
neuper@37950: 	      (* a=c/sqrt(x) ->a^2=c^2/x *)
neuper@37969:        Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}),
neuper@37950: 	      (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
neuper@37969:        Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}),
neuper@37950: 	      (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
neuper@37969:        Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
neuper@37950: 	      (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
neuper@37950:        ],scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37950:       }:rls);
neuper@37950: 
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37950: 			[("sqrt_isolate",sqrt_isolate)
neuper@37950: 			 ]);
neuper@37950: (* -- left 28.08.02--*)
neuper@37950: (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
neuper@37950:  val l_sqrt_isolate = prep_rls(
neuper@37950:      Rls {id = "l_sqrt_isolate", preconds = [], 
neuper@37950: 	  rew_ord = ("termlessI",termlessI), 
neuper@37950:           erls = RootEq_erls, srls = Erls, calc = [], 
neuper@37950:      rules = [
neuper@37969:      Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
neuper@37950:                             (* (sqrt a)^^^2 -> a *)
neuper@37969:      Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
neuper@37950:                             (* sqrt (a^^^2) -> a *)
neuper@37969:      Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
neuper@37950:             (* sqrt a sqrt b -> sqrt(ab) *)
neuper@37969:      Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
neuper@37950:         (* a sqrt b sqrt c -> a sqrt(bc) *)
neuper@37969:      Thm("sqrt_isolate_l_add1",num_str @{thm sqrt_isolate_l_add1}),
neuper@37950:         (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
neuper@37969:      Thm("sqrt_isolate_l_add2",num_str @{thm sqrt_isolate_l_add2}),
neuper@37950:         (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)
neuper@37969:      Thm("sqrt_isolate_l_add3",num_str @{thm sqrt_isolate_l_add3}),
neuper@37950:         (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
neuper@37969:      Thm("sqrt_isolate_l_add4",num_str @{thm sqrt_isolate_l_add4}),
neuper@37950:         (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
neuper@37969:      Thm("sqrt_isolate_l_add5",num_str @{thm sqrt_isolate_l_add5}),
neuper@37950:         (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
neuper@37969:      Thm("sqrt_isolate_l_add6",num_str @{thm sqrt_isolate_l_add6}),
neuper@37950:         (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
neuper@37969:    (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*)
neuper@37950:         (* b*sqrt(x) = d sqrt(x) d/b *)
neuper@37969:      Thm("sqrt_square_equation_left_1",num_str @{thm sqrt_square_equation_left_1}),
neuper@37950: 	      (* sqrt(x)=b -> x=b^2 *)
neuper@37969:      Thm("sqrt_square_equation_left_2",num_str @{thm sqrt_square_equation_left_2}),
neuper@37950: 	      (* a*sqrt(x)=b -> a^2*x=b^2*)
neuper@37969:      Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}),   
neuper@37950: 	      (* c/sqrt(x)=b -> c^2/x=b^2 *)
neuper@37969:      Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}),   
neuper@37950: 	      (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
neuper@37969:      Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}),   
neuper@37950: 	      (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
neuper@37969:      Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6})  
neuper@37950: 	      (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
neuper@37950:     ],
neuper@37950:     scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37950:    }:rls);
neuper@37950: 
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37950: 			[("l_sqrt_isolate",l_sqrt_isolate)
neuper@37950: 			 ]);
neuper@37950: 
neuper@37950: (* -- right 28.8.02--*)
neuper@37950: (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
neuper@37950:  val r_sqrt_isolate = prep_rls(
neuper@37950:      Rls {id = "r_sqrt_isolate", preconds = [], 
neuper@37950: 	  rew_ord = ("termlessI",termlessI), 
neuper@37950:           erls = RootEq_erls, srls = Erls, calc = [], 
neuper@37950:      rules = [
neuper@37969:      Thm("sqrt_square_1",num_str @{thm sqrt_square_1}),
neuper@37950:                            (* (sqrt a)^^^2 -> a *)
neuper@37969:      Thm("sqrt_square_2",num_str @{thm sqrt_square_2}), 
neuper@37950:                            (* sqrt (a^^^2) -> a *)
neuper@37969:      Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}),
neuper@37950:            (* sqrt a sqrt b -> sqrt(ab) *)
neuper@37969:      Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
neuper@37950:        (* a sqrt b sqrt c -> a sqrt(bc) *)
neuper@37969:      Thm("sqrt_isolate_r_add1",num_str @{thm sqrt_isolate_r_add1}),
neuper@37950:        (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
neuper@37969:      Thm("sqrt_isolate_r_add2",num_str @{thm sqrt_isolate_r_add2}),
neuper@37950:        (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)
neuper@37969:      Thm("sqrt_isolate_r_add3",num_str @{thm sqrt_isolate_r_add3}),
neuper@37950:        (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
neuper@37969:      Thm("sqrt_isolate_r_add4",num_str @{thm sqrt_isolate_r_add4}),
neuper@37950:        (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
neuper@37969:      Thm("sqrt_isolate_r_add5",num_str @{thm sqrt_isolate_r_add5}),
neuper@37950:        (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
neuper@37969:      Thm("sqrt_isolate_r_add6",num_str @{thm sqrt_isolate_r_add6}),
neuper@37950:        (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
neuper@37969:    (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*)
neuper@37950:        (* a=e*sqrt(x) -> a/e = sqrt(x) *)
neuper@37969:      Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}),
neuper@37950: 	      (* a=sqrt(x) ->a^2=x *)
neuper@37969:      Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}),
neuper@37950: 	      (* a=c*sqrt(x) ->a^2=c^2*x *)
neuper@37969:      Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}),
neuper@37950: 	      (* a=c/sqrt(x) ->a^2=c^2/x *)
neuper@37969:      Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}), 
neuper@37950: 	      (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
neuper@37969:      Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}),
neuper@37950: 	      (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
neuper@37969:      Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
neuper@37950: 	      (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
neuper@37950:     ],
neuper@37950:     scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37950:    }:rls);
neuper@37950: 
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37950: 			[("r_sqrt_isolate",r_sqrt_isolate)
neuper@37950: 			 ]);
neuper@37950: 
neuper@37950: val rooteq_simplify = prep_rls(
neuper@37950:   Rls {id = "rooteq_simplify", 
neuper@37950:        preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37950:        erls = RootEq_erls, srls = Erls, calc = [], 
neuper@37950:        (*asm_thm = [("sqrt_square_1","")],*)
neuper@37969:        rules = [Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),
neuper@37950:                              (* a+(b+c) = a+b+c *)
neuper@37969:                 Thm  ("real_assoc_2",num_str @{thm real_assoc_2}),
neuper@37950:                              (* a*(b*c) = a*b*c *)
neuper@37950:                 Calc ("op +",eval_binop "#add_"),
neuper@37950:                 Calc ("op -",eval_binop "#sub_"),
neuper@37950:                 Calc ("op *",eval_binop "#mult_"),
neuper@37981:                 Calc ("HOL.divide", eval_cancel "#divide_e"),
neuper@37982:                 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
neuper@37950:                 Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37969:                 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
neuper@37969:                 Thm("real_minus_binom_pow2",num_str @{thm real_minus_binom_pow2}),
neuper@37969:                 Thm("realpow_mul",num_str @{thm realpow_mul}),    
neuper@37950:                      (* (a * b)^n = a^n * b^n*)
neuper@37969:                 Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}), 
neuper@37950:                      (* sqrt b * sqrt c = sqrt(b*c) *)
neuper@37969:                 Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}),
neuper@37950:                      (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
neuper@37969:                 Thm("sqrt_square_2",num_str @{thm sqrt_square_2}),
neuper@37950:                             (* sqrt (a^^^2) = a *)
neuper@37969:                 Thm("sqrt_square_1",num_str @{thm sqrt_square_1}) 
neuper@37950:                             (* sqrt a ^^^ 2 = a *)
neuper@37950:                 ],
neuper@37950:        scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37950:     }:rls);
neuper@37967:   ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37950:                           [("rooteq_simplify",rooteq_simplify)
neuper@37950:                            ]);
neuper@37950:   
neuper@37950: (*-------------------------Problem-----------------------*)
neuper@37950: (*
neuper@37950: (get_pbt ["root","univariate","equation"]);
neuper@37950: show_ptyps(); 
neuper@37950: *)
neuper@37950: (* ---------root----------- *)
neuper@37950: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equ_univ_root" [] e_pblID
neuper@37950:  (["root","univariate","equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982:    ("#Where" ,["(lhs e_e) is_rootTerm_in  (v_v::real) | " ^
neuper@37982: 	       "(rhs e_e) is_rootTerm_in  (v_v::real)"]),
neuper@37981:    ("#Find"  ,["solutions v_i"]) 
neuper@37950:   ],
neuper@37981:   RootEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37950:   []));
neuper@37950: (* ---------sqrt----------- *)
neuper@37950: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
neuper@37950:  (["sq","root","univariate","equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982:    ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
neuper@37982:                "  ((lhs e_e) is_normSqrtTerm_in (v_v::real))   )  |" ^
neuper@37982: 	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
neuper@37982:                "  ((rhs e_e) is_normSqrtTerm_in (v_v::real))   )"]),
neuper@37981:    ("#Find"  ,["solutions v_i"]) 
neuper@37950:   ],
neuper@37981:   RootEq_prls,  SOME "solve (e_e::bool, v_v)",
neuper@37950:   [["RootEq","solve_sq_root_equation"]]));
neuper@37950: (* ---------normalize----------- *)
neuper@37950: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
neuper@37950:  (["normalize","root","univariate","equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982:    ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
neuper@37982:                "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
neuper@37982: 	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
neuper@37982:                "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
neuper@37981:    ("#Find"  ,["solutions v_i"]) 
neuper@37950:   ],
neuper@37981:   RootEq_prls,  SOME "solve (e_e::bool, v_v)",
neuper@37950:   [["RootEq","norm_sq_root_equation"]]));
neuper@37950: 
neuper@37950: (*-------------------------methods-----------------------*)
neuper@37950: (* ---- root 20.8.02 ---*)
neuper@37950: store_met
neuper@37972:  (prep_met thy "met_rooteq" [] e_metID
neuper@37950:  (["RootEq"],
neuper@37950:    [],
neuper@37950:    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37950:     crls=RootEq_crls, nrls=norm_Poly(*,
neuper@37950:     asm_rls=[],asm_thm=[]*)}, "empty_script"));
neuper@37985: 
neuper@37950: (*-- normalize 20.10.02 --*)
neuper@37950: store_met
neuper@37972:  (prep_met thy "met_rooteq_norm" [] e_metID
neuper@37950:  (["RootEq","norm_sq_root_equation"],
neuper@37981:    [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982:     ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
neuper@37982:                "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
neuper@37982: 	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
neuper@37982:                "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
neuper@37981:     ("#Find"  ,["solutions v_i"])
neuper@37950:    ],
neuper@37985:    {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
neuper@37985:     calc=[], crls=RootEq_crls, nrls=norm_Poly},
neuper@37982:    "Script Norm_sq_root_equation  (e_e::bool) (v_v::real)  =                " ^
neuper@37981:     "(let e_e = ((Repeat(Try (Rewrite     makex1_x            False))) @@  " ^
neuper@37950:     "           (Try (Repeat (Rewrite_Set expand_rootbinoms  False))) @@  " ^ 
neuper@37950:     "           (Try (Rewrite_Set rooteq_simplify              True)) @@  " ^ 
neuper@37950:     "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^
neuper@37981:     "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^
neuper@37985:     " in ((SubProblem (RootEq_',[univariate,equation],                     " ^
neuper@37985:     "      [no_met]) [BOOL e_e, REAL v_v])))"
neuper@37950:    ));
neuper@37950: 
neuper@37985: *}
neuper@37985: 
neuper@37985: ML {* (*-----del------------------------------------------------del-----*)
neuper@37985: Toplevel.debug := true;
neuper@37985: val scr = 
neuper@37985: "Script Solve_sq_root_equation  (e_e::bool) (v_v::real)  =               " ^
neuper@37985: "(let e_e =                                                              " ^
neuper@37985: "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@      " ^
neuper@37985: "   (Try (Rewrite_Set         rooteq_simplify True))             @@      " ^
neuper@37985: "   (Try (Repeat (Rewrite_Set expand_rootbinoms         False))) @@      " ^
neuper@37985: "   (Try (Repeat (Rewrite_Set make_rooteq               False))) @@      " ^
neuper@37985: "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^
neuper@37985: " (L_L::bool list) =                                                     " ^
neuper@37985: "   (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
neuper@37985: "    then (SubProblem (RootEq_',[normalize,root',univariate,equation],   " ^
neuper@37985: "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
neuper@37985: "    else (SubProblem (RootEq_',[univariate,equation], [no_met])         " ^
neuper@37985: "                     [BOOL e_e, REAL v_v]))                             " ^
neuper@37985: "in Check_elementwise L_L {(v_v::real). Assumptions})";
neuper@37985: val sss = ( term_of o the o (parse thy)) scr;
neuper@37985: *}
neuper@37985: 
neuper@37985: ML {*
neuper@37985: val -------------------------------------------------- = "00000";
neuper@37950: store_met
neuper@37972:  (prep_met thy "met_rooteq_sq" [] e_metID
neuper@37950:  (["RootEq","solve_sq_root_equation"],
neuper@37985:    [("#Given" ,["equality e_e", "solveFor v_v"]),
neuper@37985:     ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real))     & " ^
neuper@37985:                 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
neuper@37985: 	        "(((rhs e_e) is_sqrtTerm_in (v_v::real))     & " ^
neuper@37985:                 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
neuper@37981:     ("#Find"  ,["solutions v_i"])
neuper@37950:    ],
neuper@37985:    {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
neuper@37985:     prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
neuper@37985: "Script Solve_sq_root_equation  (e_e::bool) (v_v::real)  =               " ^
neuper@37985: "(let e_e =                                                              " ^
neuper@37985: "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@      " ^
neuper@37985: "   (Try (Rewrite_Set         rooteq_simplify True))             @@      " ^
neuper@37985: "   (Try (Repeat (Rewrite_Set expand_rootbinoms         False))) @@      " ^
neuper@37985: "   (Try (Repeat (Rewrite_Set make_rooteq               False))) @@      " ^
neuper@37985: "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^
neuper@37985: " (L_L::bool list) =                                                     " ^
neuper@37985: "   (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
neuper@37985: "    then (SubProblem (RootEq_',[normalize,root',univariate,equation],   " ^
neuper@37985: "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
neuper@37985: "    else (SubProblem (RootEq_',[univariate,equation], [no_met])         " ^
neuper@37985: "                     [BOOL e_e, REAL v_v]))                             " ^
neuper@37985: "in Check_elementwise L_L {(v_v::real). Assumptions})"
neuper@37950:  ));
neuper@37985: *}
neuper@37950: 
neuper@37985: ML {*
neuper@37950: (*-- right 28.08.02 --*)
neuper@37950: store_met
neuper@37972:  (prep_met thy "met_rooteq_sq_right" [] e_metID
neuper@37950:  (["RootEq","solve_right_sq_root_equation"],
neuper@37981:    [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981:     ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
neuper@37981:     ("#Find"  ,["solutions v_i"])
neuper@37950:    ],
neuper@37985:    {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, 
neuper@37985:     prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
neuper@37985:   "Script Solve_right_sq_root_equation  (e_e::bool) (v_v::real)  =           " ^
neuper@37985:    "(let e_e =                                                               " ^
neuper@37985:    "    ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate  False)) @@ " ^
neuper@37985:    "    (Try (Rewrite_Set                       rooteq_simplify False)) @@   " ^
neuper@37985:    "    (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@   " ^
neuper@37985:    "    (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@   " ^
neuper@37981:    "    (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
neuper@37985:    " in if ((rhs e_e) is_sqrtTerm_in v_v)                                    " ^
neuper@37985:    " then (SubProblem (RootEq_',[normalize,root',univariate,equation],       " ^
neuper@37985:    "       [no_met]) [BOOL e_e, REAL v_v])                                   " ^
neuper@37985:    " else ((SubProblem (RootEq_',[univariate,equation],                      " ^
neuper@37985:    "        [no_met]) [BOOL e_e, REAL v_v])))"
neuper@37950:  ));
neuper@37985: val --------------------------------------------------+++ = "33333";
neuper@37950: 
neuper@37950: (*-- left 28.08.02 --*)
neuper@37950: store_met
neuper@37972:  (prep_met thy "met_rooteq_sq_left" [] e_metID
neuper@37950:  (["RootEq","solve_left_sq_root_equation"],
neuper@37981:    [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981:     ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
neuper@37981:     ("#Find"  ,["solutions v_i"])
neuper@37950:    ],
neuper@37950:    {rew_ord'="termlessI",
neuper@37950:     rls'=RootEq_erls,
neuper@37950:     srls=e_rls,
neuper@37950:     prls=RootEq_prls,
neuper@37950:     calc=[],
neuper@37950:     crls=RootEq_crls, nrls=norm_Poly},
neuper@37982:     "Script Solve_left_sq_root_equation  (e_e::bool) (v_v::real)  =          " ^
neuper@37981:     "(let e_e =                                                             " ^
neuper@37985:     "  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate  False)) @@ " ^
neuper@37950:     "  (Try (Rewrite_Set                       rooteq_simplify False)) @@  " ^
neuper@37950:     "  (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@  " ^
neuper@37950:     "  (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@  " ^
neuper@37981:     "  (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
neuper@37981:     " in if ((lhs e_e) is_sqrtTerm_in v_v)                                   " ^ 
neuper@37985:     " then (SubProblem (RootEq_',[normalize,root',univariate,equation],      " ^
neuper@37985:     "       [no_met]) [BOOL e_e, REAL v_v])                                " ^
neuper@37985:     " else ((SubProblem (RootEq_',[univariate,equation],                    " ^
neuper@37985:     "        [no_met]) [BOOL e_e, REAL v_v])))"
neuper@37950:    ));
neuper@37985: val --------------------------------------------------++++ = "44444";
neuper@37950: 
neuper@37950: calclist':= overwritel (!calclist', 
neuper@37950:    [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", 
neuper@37950: 			eval_is_rootTerm_in"")),
neuper@37950:     ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", 
neuper@37950: 			eval_is_sqrtTerm_in"")),
neuper@37950:     ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", 
neuper@37950: 				 eval_is_normSqrtTerm_in""))
neuper@37950:     ]);(*("", ("", "")),*)
neuper@37950: *}
neuper@37950: 
neuper@37906: end




