(* 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 LinEq RootEq RatEq RootRat begin 

text {* univariate equations over rational terms containing real square roots:

  In 2003 this type has been developed as part of ISAC's equation solver

  by Richard Lang in 2003.

  The migration Isabelle2002 --> 2011 dropped this type of equation, see RootEq.thy.

*}

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

axiomatization where

  (* eliminate ratRootTerm *)

  rootrat_equation_left_1:

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

  rootrat_equation_left_2:

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

  rootrat_equation_right_2:

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

  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 ("Groups.plus_class.plus",_) $ t2 $ t3)) v = 

            (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)

	  | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v = 

            (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)

	  | rootadd _ _ = false;

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

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

	  | findrootrat (t as (Const ("Fields.inverse_class.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, @{term True})))

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

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

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

*}

ML {*

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

		[])));

*}

setup {* KEStore_Elems.add_rlss

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

ML {*

(* Solves a rootrat Equation *)

 val rootrat_solve = prep_rls(

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

	  rew_ord = ("termlessI",termlessI), 

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

     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 = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);

*}

setup {* KEStore_Elems.add_rlss

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

ML {*

(*-----------------------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_v'i'"])

   ],

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

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

*}

setup {* KEStore_Elems.add_pbts

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

        RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]]))] *}

ML {*

(*-------------------------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, errpats = [], 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_v'i'"])

   ],

   {rew_ord'="termlessI",

    rls'=RooRatEq_erls,

    srls=e_rls,

    prls=RootRatEq_prls,

    calc=[],

    crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},

   "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_v)]               " ^

    "                                  rootrat_solve False))) e_e " ^

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

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

   ));

*}

setup {* KEStore_Elems.add_calcs

  [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))] *}

end