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

 consts

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

   (*----------------------scripts-----------------------*)

   Solve'_rat'_equation

              :: "[bool,real, 

 		   bool list] => bool list"

                ("((Script Solve'_rat'_equation (_ _ =))// 

                   (_))" 9)

 axioms 

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

    real_rat_mult_2

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

    real_rat_mult_3

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

    real_rat_pow

    "(a/b)^^^2 = a^^^2/b^^^2"

    rat_double_rat_1

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

    rat_double_rat_2

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

    rat_double_rat_3

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

   (* equation to same denominator *)

   rat_mult_denominator_both

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

   rat_mult_denominator_left

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

   rat_mult_denominator_right

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

 ML {*

 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 coeff_in c v = member op = (vars c) v;

    	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")

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

 	  | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v

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

                                          orelse (finddivide t2 v)

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

 	  | finddivide _ _ = false;

      in

 	finddivide t v

     end;

 fun eval_is_ratequation_in _ _ 

        (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _  =

     if is_rateqation_in t v then 

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

 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))

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

 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

   | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);

 (*-------------------------rulse-----------------------*)

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

   append_rls "RatEq_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 ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),

 	      Calc ("op =",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})

 	      ];

 (*rls = merge_rls erls Poly_erls *)

 val rateq_erls = 

     remove_rls "rateq_erls"                                   (*WN: ein Hack*)

 	(merge_rls "is_ratequation_in" calculate_Rational

 		   (append_rls "is_ratequation_in"

 			Poly_erls

 			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)

 			 Calc ("RatEq.is'_ratequation'_in",

 			       eval_is_ratequation_in "")

 			 ]))

 	[Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)

 	 Thm ("or_commute",num_str @{thm or_commute})    (*WN: ein Hack*)

 	 ];

 ruleset' := overwritelthy @{theory} (!ruleset',

 			[("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)

 			 ]);

 val RatEq_crls = 

     remove_rls "RatEq_crls"                                   (*WN: ein Hack*)

 	(merge_rls "is_ratequation_in" calculate_Rational

 		   (append_rls "is_ratequation_in"

 			Poly_erls

 			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)

 			 Calc ("RatEq.is'_ratequation'_in",

 			       eval_is_ratequation_in "")

 			 ]))

 	[Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)

 	 Thm ("or_commute",num_str @{thm or_commute})    (*WN: ein Hack*)

 	 ];

 val RatEq_eliminate = prep_rls(

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

        rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls, 

        calc = [], 

        rules = [

 	    Thm("rat_mult_denominator_both",num_str @{thm rat_mult_denominator_both}), 

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

 	    Thm("rat_mult_denominator_left",num_str @{thm rat_mult_denominator_left}), 

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

 	    Thm("rat_mult_denominator_right",num_str @{thm rat_mult_denominator_right})

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

 	    ],

     scr = Script ((term_of o the o (parse thy)) "empty_script")

     }:rls);

 ruleset' := overwritelthy @{theory} (!ruleset',

 			[("RatEq_eliminate",RatEq_eliminate)

 			 ]);

 val RatEq_simplify = prep_rls(

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

       erls = rateq_erls, srls = Erls, calc = [], 

     rules = [

 	     Thm("real_rat_mult_1",num_str @{thm real_rat_mult_1}),

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

 	     Thm("real_rat_mult_2",num_str @{thm real_rat_mult_2}),

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

              Thm("real_rat_mult_3",num_str @{thm real_rat_mult_3}),

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

 	     Thm("real_rat_pow",num_str @{thm real_rat_pow}),

 	     (*(a/b)^^^2 = a^^^2/b^^^2*)

 	     Thm("real_diff_minus",num_str @{thm real_diff_minus}),

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

              Thm("rat_double_rat_1",num_str @{thm rat_double_rat_1}),

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

              Thm("rat_double_rat_2",num_str @{thm rat_double_rat_2}), 

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

              Thm("rat_double_rat_3",num_str @{thm rat_double_rat_3}) 

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

 	     ],

     scr = Script ((term_of o the o (parse thy)) "empty_script")

     }:rls);

 ruleset' := overwritelthy @{theory} (!ruleset',

 			[("RatEq_simplify",RatEq_simplify)

 			 ]);

 (*-------------------------Problem-----------------------*)

 (*

 (get_pbt ["rational","univariate","equation"]);

 show_ptyps(); 

 *)

 store_pbt

  (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID

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

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

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

    ("#Find"  ,["solutions v_i"]) 

   ],

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

   [["RatEq","solve_rat_equation"]]));

 (*-------------------------methods-----------------------*)

 store_met

  (prep_met thy "met_rateq" [] e_metID

  (["RatEq"],

    [],

    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

     crls=RatEq_crls, nrls=norm_Rational

     (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));

 store_met

  (prep_met thy "met_rat_eq" [] e_metID

  (["RatEq","solve_rat_equation"],

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

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

    ("#Find"  ,["solutions v_i"])

   ],

    {rew_ord'="termlessI",

     rls'=rateq_erls,

     srls=e_rls,

     prls=RatEq_prls,

     calc=[],

     crls=RatEq_crls, nrls=norm_Rational},

    "Script Solve_rat_equation  (e_e::bool) (v_::real) =                   " ^

     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^

     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^

     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^

     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_;" ^

     " (L_::bool list) =  (SubProblem (RatEq_,[univariate,equation],      " ^

     "                [no_met]) [bool_ e_e, real_ v_])                     " ^

     " in Check_elementwise L_ {(v_::real). Assumptions})"

    ));

 calclist':= overwritel (!calclist', 

    [("is_ratequation_in", ("RatEq.is_ratequation_in", 

 			   eval_is_ratequation_in ""))

     ]);

 *}

 end