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

(* collecting all knowledge for Root and Rational Equations

   created by: rlang 

         date: 02.10

   changed by: rlang

   last change by: rlang

             date: 02.11.04

*)

(* use"knowledge/RootRatEq.ML";

   use"RootRatEq.ML";

   use"ROOT.ML";

   cd"knowledge";

   remove_thy"RootRatEq";

   use_thy"Isac";

   *)

"******* RootRatEq.ML begin *******";

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

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

(* true if denominator contains (sq)root in + or - term 

   1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true

   if false then (term)^2 contains no (sq)root *)

fun is_rootRatAddTerm_in t v = 

    let 

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

	fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse 

	                                                    (is_rootTerm_in t3 v)

	  | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse 

                                                            (is_rootTerm_in t3 v)

	  | rootadd _ _ = false;

	fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")

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

	  | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = 

	               if (is_rootTerm_in t3 v) then rootadd t3 v else false

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

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

	  | findrootrat _ _ = false;

     in

	findrootrat t v

    end;

fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _  =

    if is_rootRatAddTerm_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_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);

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

val RootRatEq_prls = 

    append_rls "RootRatEq_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'_rootTerm'_in",eval_is_rootTerm_in ""),

                 Calc ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_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 RooRatEq_erls = 

    merge_rls "RooRatEq_erls" rootrat_erls

    (merge_rls "" RootEq_erls

     (merge_rls "" rateq_erls

      (append_rls "" e_rls

		[])));

val RootRatEq_crls = 

    merge_rls "RootRatEq_crls" rootrat_erls

    (merge_rls "" RootEq_erls

     (merge_rls "" rateq_erls

      (append_rls "" e_rls

		[])));

ruleset' := overwritelthy thy (!ruleset',

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

			 ]);

(* Solves a rootrat Equation *)

 val rootrat_solve = prep_rls(

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

	  rew_ord = ("termlessI",termlessI), 

     erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

     rules = [  Thm("rootrat_equation_left_1",num_str rootrat_equation_left_1),   

	        (* [|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c )) *)

                Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2),   

	        (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)

	        Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1),   

		(* [|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e )) *)

	        Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2)   

		(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e )) *)

	      ],

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

         }:rls);

ruleset' := overwritelthy thy (!ruleset',

			[("rootrat_solve",rootrat_solve)

			 ]);

(*-----------------------probleme------------------------*)

(*

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

show_ptyps(); 

*)

store_pbt

 (prep_pbt RootRatEq.thy "pbl_equ_univ_root_sq_rat" [] e_pblID

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

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

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

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

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

   ],

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

  [["RootRatEq","elim_rootrat_equation"]]));

(*-------------------------Methode-----------------------*)

store_met

 (prep_met LinEq.thy "met_rootrateq" [] e_metID

 (["RootRatEq"],

   [],

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

    crls=Atools_erls, nrls=norm_Rational(*,

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

(*-- left 20.10.02 --*)

store_met

 (prep_met RootRatEq.thy "met_rootrateq_elim" [] e_metID

 (["RootRatEq","elim_rootrat_equation"],

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

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

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

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

   ],

   {rew_ord'="termlessI",

    rls'=RooRatEq_erls,

    srls=e_rls,

    prls=RootRatEq_prls,

    calc=[],

    crls=RootRatEq_crls, nrls=norm_Rational(*,

    asm_rls=[],

    asm_thm=[]*)},

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

    \(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@  \ 

    \           (Try (Rewrite_Set rooteq_simplify   False)) @@  \ 

    \           (Try (Rewrite_Set make_rooteq       False)) @@  \

    \           (Try (Rewrite_Set rooteq_simplify   False)) @@  \

    \           (Try (Rewrite_Set_Inst [(bdv,v_)]               \

    \                                  rootrat_solve False))) e_ \

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

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

   ));

calclist':= overwritel (!calclist', 

   [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", 

			      eval_is_rootRatAddTerm_in""))

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

"******* RootRatEq.ML end *******";