(*.(c) by Richard Lang, 2003 .*)

(* theory collecting all knowledge for RationalEquations

   created by: rlang 

         date: 02.08.12

   changed by: rlang

   last change by: rlang

             date: 02.11.28

*)

theory RatEq imports Rational LinEq begin

text \<open>univariate equations over multivariate rational terms:

  In 2003 this type has been integrated into ISAC's equation solver

  by Richard Lang; the root for the solver is Equation.thy.

  The migration Isabelle2002 --> 2011 found that application of theorems like 

  rat_mult_denominator_right: "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"

  in rule-sets does not transfer "d ~= 0" to the assumptions; see

  test --- repair NO asms from rls RatEq_eliminate ---.

  Thus the migration dropped update of Check_elementwise, which would require

  these assumptions; see 

  test --- pbl: rational, univariate, equation ---, --- x / (x ^ 2 - 6 * x + 9) - 1 /...

\<close>

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

consts

  is_ratequation_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")

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

axiomatization where

   (* FIXME also in Poly.thy def. --> FIXED*)

   (*real_diff_minus            

   "a - b = a + (-1) * b"*)

   real_rat_mult_1:   "a*(b/c) = (a*b)/c" and

   real_rat_mult_2:   "(a/b)*(c/d) = (a*c)/(b*d)" and

   real_rat_mult_3:   "(a/b)*c = (a*c)/b" and

   real_rat_pow:      "(a/b) \<up> 2 = a \<up> 2/b \<up> 2" and

   rat_double_rat_1:   "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" and

   rat_double_rat_2:   "[|Not(b=0);Not(c=0); Not(d=0)|] ==> 

                                           ((a/b) / (c/d) = (a*d) / (b*c))" and

   rat_double_rat_3:   "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" and

  (* equation to same denominator *)

  rat_mult_denominator_both:

   "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" and

  rat_mult_denominator_left:

   "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" and

  rat_mult_denominator_right:

   "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"

subsection \<open>predicates\<close>

ML \<open>

val thy = @{theory};

(*-------------------------functions-----------------------*)

(* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)

fun is_rateqation_in t v = 

  let 

   	fun finddivide (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_rateqation_in", [t]) 

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

	  | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = Prog_Expr.occurs_in v b

	  | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v

	  | finddivide (_ $ t1) v = finddivide t1 v

	  | finddivide _ _ = false;

  in

	  finddivide t v

  end;

\<close>

subsection \<open>evaluations functions\<close>

ML \<open>

fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is_ratequation_in",_) $ t $ v)) _ =

    if is_rateqation_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_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);

\<close>

setup \<open>KEStore_Elems.add_calcs

  [("is_ratequation_in", ("RatEq.is_ratequation_in", eval_is_ratequation_in ""))]\<close>

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

ML \<open>

val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)

  Rule_Set.append_rules "RatEq_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 ("RatEq.is_ratequation_in", eval_is_ratequation_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})

	      ];

\<close> ML \<open>

(*rls = Rule_Set.merge erls Poly_erls *)

val rateq_erls = 

  Rule_Set.keep_unique_rules "rateq_erls"                             (*WN: ein Hack*)

	  (Rule_Set.merge "is_ratequation_in" calculate_Rational

		  (Rule_Set.append_rules "is_ratequation_in"

			  Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)

			    Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))

 [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)

	Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})];  (*WN: ein Hack*)

\<close> ML \<open>

val RatEq_crls = 

  Rule_Set.keep_unique_rules "RatEq_crls"                              (*WN: ein Hack*)

	  (Rule_Set.merge "is_ratequation_in" calculate_Rational

		  (Rule_Set.append_rules "is_ratequation_in"

			  Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)

			    Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))

 [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)

	Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})];  (*WN: ein Hack*)

val RatEq_eliminate = prep_rls'(

  Rule_Def.Repeat

    {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,

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

     rules = [

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

	     (* a/b=c/d -> ad=cb *)

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

	     (* a  =c/d -> ad=c  *)

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

	     (* a/b=c   ->  a=cb *)

	     ],

    scr = Rule.Empty_Prog});

\<close> ML \<open>

val RatEq_simplify = prep_rls'(

  Rule_Def.Repeat

    {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,

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

     rules = [

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

	     (*a*(b/c) = (a*b)/c*)

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

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

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

       (* (a/b)*c = (a*c)/b*)

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

	     (*(a/b) \<up> 2 = a \<up> 2/b \<up> 2*)

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

	     (* a - b = a + (-1) * b *)

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

       (* (a / (c/d) = (a*d) / c) *)

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

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

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

       (* ((a/b) / c = a / (b*c) ) *)],

     scr = Rule.Empty_Prog});

\<close>

setup \<open>KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))]\<close>

setup \<open>KEStore_Elems.add_rlss [("RatEq_eliminate", (Context.theory_name @{theory}, RatEq_eliminate))]\<close>

setup \<open>KEStore_Elems.add_rlss [("RatEq_simplify", (Context.theory_name @{theory}, RatEq_simplify))]\<close>

subsection \<open>problems\<close>

setup \<open>KEStore_Elems.add_pbts

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

    (["rational", "univariate", "equation"],

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

        ("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),

        ("#Find", ["solutions v_v'i'"])],

      RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq", "solve_rat_equation"]]))]\<close>

subsection \<open>methods\<close>

setup \<open>KEStore_Elems.add_mets

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

      (["RatEq"], [],

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

          crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>

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

  where

"solve_rational_equ e_e v_v =

  (let

    e_e = (

      (Repeat (Try (Rewrite_Set ''RatEq_simplify''))) #>

      (Repeat (Try (Rewrite_Set ''norm_Rational''))) #>

      (Repeat (Try (Rewrite_Set ''add_fractions_p''))) #>

      (Repeat (Try (Rewrite_Set ''RatEq_eliminate''))) ) e_e;

    L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v]

  in

    Check_elementwise L_L {(v_v::real). Assumptions})"

setup \<open>KEStore_Elems.add_mets

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

      (["RatEq", "solve_rat_equation"],

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

          ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),

          ("#Find"  ,["solutions v_v'i'"])],

        {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule_Set.empty, prls=RatEq_prls, calc=[],

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

        @{thm solve_rational_equ.simps})]

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end