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

   (c) by Richard Lang, 2003

*)

theory RootRatEq imports RootEq RatEq RootRat begin 

consts

  is'_rootRatAddTerm'_in :: "[real, real] => bool" 

                             ("_ is'_rootRatAddTerm'_in _") (*RL DA*)

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

  Elim'_rootrat'_equation

             :: "[bool,real,  

		    bool list] => bool list"

               ("((Script Elim'_rootrat'_equation (_ _ =))//  

                   (_))" 9)

 (*-------------------- rules------------------------------------------------*)

axioms

  (* eliminate ratRootTerm *)

  rootrat_equation_left_1:

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

  rootrat_equation_left_2:

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

  rootrat_equation_right_2:

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

  rootrat_equation_right_1:

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

ML {*

val thy = @{theory};

(*-------------------------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 @{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 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 @{theory} (!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 @{thm }rootrat_equation_left_1),   

	        (* [|c is_rootTerm_in bdv|] ==> 

                                    ( (a + b/c = d) = ( b = (d - a) * c )) *)

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

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

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

		(* [|f is_rootTerm_in bdv|] ==> 

                                    ( (a = d + e/f) = ( (a - d) * f = e )) *)

	      Thm("rootrat_equation_right_2",num_str @{thm 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 @{theory} (!ruleset',

			[("rootrat_solve",rootrat_solve)

			 ]);

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

(*

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

show_ptyps(); 

*)

store_pbt

 (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID

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

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

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

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

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

   ],

  RootRatEq_prls, SOME "solve (e_e::bool, v_v)",

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

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

store_met

 (prep_met (theory "LinEq") "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}, "empty_script"));

(*-- left 20.10.02 --*)

store_met

 (prep_met thy "met_rootrateq_elim" [] e_metID

 (["RootRatEq","elim_rootrat_equation"],

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

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

	       "( (rhs e_e) is_rootRatAddTerm_in (v_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_e::bool) (v_v::real)  =      " ^

    "(let e_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_e " ^

    " in (SubProblem (RootEq_,[univariate,equation],            " ^

    "        [no_met]) [bool_ e_e, real_ v_]))"

   ));

calclist':= overwritel (!calclist', 

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

			      eval_is_rootRatAddTerm_in""))

    ]);

*}

end