(* 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 \<open>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.

\<close>

subsection \<open>consts definition for predicates\<close>

consts

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

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

subsection \<open>theorems not yet adopted from Isabelle\<close>

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

subsection \<open>predicates\<close>

ML \<open>

val thy = @{theory};

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

        is_rootTerm_in t2 v orelse is_rootTerm_in t3 v

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

        is_rootTerm_in t2 v orelse is_rootTerm_in t3 v

	    | rootadd _ _ = false;

  	fun findrootrat (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_rootRatAddTerm_in", [t])

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

  	  | findrootrat (Const ("Rings.divide_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 ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

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

\<close>

setup \<open>KEStore_Elems.add_calcs

  [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))]\<close>

subsection \<open>rule-sets\<close>

ML \<open>

val RootRatEq_prls = 

  Rule_Set.append_rules "RootRatEq_prls" Rule_Set.empty

		[Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),

     Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),

     Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),

     Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),

     Rule.Eval ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in ""),

     Rule.Eval ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""),

     Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),

     Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

     Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),

     Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),

     Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),

     Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),

     Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})];

val RooRatEq_erls = 

  Rule_Set.merge "RooRatEq_erls" rootrat_erls

    (Rule_Set.merge "" RootEq_erls

     (Rule_Set.merge "" rateq_erls

      (Rule_Set.append_rules "" Rule_Set.empty

		[])));

val RootRatEq_crls = 

  Rule_Set.merge "RootRatEq_crls" rootrat_erls

    (Rule_Set.merge "" RootEq_erls

     (Rule_Set.merge "" rateq_erls

      (Rule_Set.append_rules "" Rule_Set.empty

		[])));

\<close> ML \<open>

(* Solves a rootrat Equation *)

val rootrat_solve = prep_rls'(

  Rule_Def.Repeat {id = "rootrat_solve", preconds = [], 

  rew_ord = ("termlessI",termlessI), 

    erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

    rules = 

    [Rule.Thm("rootrat_equation_left_1", ThmC.numerals_to_Free @{thm rootrat_equation_left_1}),   

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

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

     Rule.Thm("rootrat_equation_left_2",ThmC.numerals_to_Free @{thm rootrat_equation_left_2}),

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

     Rule.Thm("rootrat_equation_right_1",ThmC.numerals_to_Free @{thm rootrat_equation_right_1}),

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

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

     Rule.Thm("rootrat_equation_right_2",ThmC.numerals_to_Free @{thm rootrat_equation_right_2})

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

     ], scr = Rule.Empty_Prog});

\<close>

setup \<open>KEStore_Elems.add_rlss

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

   ("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))]\<close>

subsection \<open>problems\<close>

ML \<open>

(*

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

show_ptyps(); 

*)

\<close>

setup \<open>KEStore_Elems.add_pbts

  [(Problem.prep_input thy "pbl_equ_univ_root_sq_rat" [] Problem.id_empty

      (["rat", "sq", "rootX", "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"]]))]\<close>

subsection \<open>methods\<close>

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input @{theory LinEq} "met_rootrateq" [] MethodC.id_empty

      (["RootRatEq"], [],

        {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,

          crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]

\<close>

    (*-- left 20.10.02 --*)

partial_function (tailrec) solve_rootrat_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"

  where

"solve_rootrat_equ e_e v_v =          

  (let

    e_e = (

      (Try (Rewrite_Set ''expand_rootbinoms'')) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) #>

      (Try (Rewrite_Set ''make_rooteq'')) #>

      (Try (Rewrite_Set ''rooteq_simplify'')) #>

      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e

  in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input thy "met_rootrateq_elim" [] MethodC.id_empty

      (["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=Rule_Set.empty, prls=RootRatEq_prls, calc=[],

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

        @{thm solve_rootrat_equ.simps})]

\<close>

end