(* 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 @{context} p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

     else SOME ((UnparseC.term @{context} 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), 

     asm_rls = Rule_Set.empty, prog_rls = 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 ))*)

     program = 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_Ref: "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>

 method "met_rootrateq" : "RootRatEq" =

  \<open>{rew_ord="tless_true",rls'=Atools_erls,calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,

   errpats = [], rew_rls = norm_Rational}\<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, prog_rls=Rule_Set.empty, where_rls=RootRatEq_prls, calc=[],

     errpats = [], rew_rls = 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