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

(* 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 (\<^const_name>\<open>plus\<close>, _) $ t2 $ t3) v = 

        is_rootTerm_in t2 v orelse is_rootTerm_in t3 v

	    | rootadd (Const (\<^const_name>\<open>minus\<close>,_) $ 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 (\<^const_name>\<open>divide\<close>,_) $ _ $ 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 (\<^const_name>\<open>is_rootRatAddTerm_in\<close>,_) $ 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>

calculation is_rootRatAddTerm_in = \<open>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>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),

     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),

     \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),

     \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),

     \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),

     \<^rule_eval>\<open>is_rootRatAddTerm_in\<close> (eval_is_rootRatAddTerm_in ""),

     \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),

     \<^rule_thm>\<open>not_true\<close>,

     \<^rule_thm>\<open>not_false\<close>,

     \<^rule_thm>\<open>and_true\<close>,

     \<^rule_thm>\<open>and_false\<close>,

     \<^rule_thm>\<open>or_true\<close>,

     \<^rule_thm>\<open>or_false\<close>];

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>\<open>rootrat_equation_left_1\<close>,   

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

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

     \<^rule_thm>\<open>rootrat_equation_left_2\<close>,

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

     \<^rule_thm>\<open>rootrat_equation_right_1\<close>,

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

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

     \<^rule_thm>\<open>rootrat_equation_right_2\<close>

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

     ], scr = Rule.Empty_Prog});

\<close>

rule_set_knowledge

  RooRatEq_erls = RooRatEq_erls and

  rootrat_solve = rootrat_solve

subsection \<open>problems\<close>

problem pbl_equ_univ_root_sq_rat : "rat/sq/rootX/univariate/equation" =

  \<open>RootRatEq_prls\<close>

  Method: "RootRatEq/elim_rootrat_equation"

  CAS: "solve (e_e::bool, v_v)"

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

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

method met_rootrateq_elim : "RootRatEq/elim_rootrat_equation" =

  \<open>{rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule_Set.empty, prls=RootRatEq_prls, calc=[],

    crls=RootRatEq_crls, errpats = [], nrls = norm_Rational}\<close>

  Program: solve_rootrat_equ.simps

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

ML \<open>

\<close> ML \<open>

\<close>

end