(* (c) by Richard Lang

    collecting all knowledge for RationalEquations

    created by: rlang 

          date: 02.09

    changed by: rlang

    last change by: rlang

              date: 02.11.29

 *)

 (* use"knowledge/RatEq.ML";

    use"RatEq.ML";

    remove_thy"RatEq";

    use_thy"Isac";

    use"ROOT.ML";

    cd"knowledge";

    *)

 "******* RatEq.ML begin *******";

 theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]);

 (*-------------------------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 = v mem (vars c);

    	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 not_true),

 	      Thm ("not_false",num_str not_false),

 	      Thm ("and_true",num_str and_true),

 	      Thm ("and_false",num_str and_false),

 	      Thm ("or_true",num_str or_true),

 	      Thm ("or_false",num_str or_false),

 	      Thm ("and_commute",num_str and_commute),

 	      Thm ("or_commute",num_str or_commute)

 	      ];

 (*rls = merge_rls erls poly_erls *)

     remove_rls "no_commute"                                   (*ein Hack*)

     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_"),*)

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

 			       eval_is_ratequation_in "")

 	[Thm ("and_commute",num_str and_commute), (*ein Hack*)

 	 Thm ("or_commute",num_str or_commute)    (*ein Hack*)

 	 Thm ("or_commute",num_str or_commute)    (*WN: ein Hack*)

 	 ];

 ruleset' := overwritel (!ruleset',

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

 			 ]);

 val rat_eliminate = 

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

                   ("rat_mult_denominator_right","")],

     rules = [

 	     Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both), 

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

 	     Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left), 

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

 	     Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)

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

 	     ],

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

     }:rls;

 ruleset' := overwritel (!ruleset',

 			[("rat_eliminate",rat_eliminate)

 			 ]);

 val rat_simplify = 

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

                   ("rat_double_rat_3","")],

     rules = [

 	     Thm("real_rat_mult_1",num_str real_rat_mult_1),

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

 	     Thm("real_rat_mult_2",num_str real_rat_mult_2),

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

              Thm("real_rat_mult_3",num_str real_rat_mult_3),

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

 	     Thm("real_rat_pow",num_str real_rat_pow),

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

 	     Thm("real_diff_minus",num_str real_diff_minus),

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

              Thm("rat_double_rat_1",num_str rat_double_rat_1),

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

              Thm("rat_double_rat_2",num_str rat_double_rat_2), 

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

              Thm("rat_double_rat_3",num_str rat_double_rat_3) 

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

 	     ],

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

     }:rls;

 ruleset' := overwritel (!ruleset',

 			[("rat_simplify",rat_simplify)

 			 ]);

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

 (*

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

 show_ptyps(); 

 *)

 store_pbt

  (prep_pbt RatEq.thy

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

   [("#Given" ,["equality e_","solveFor v_"]),

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

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

   ],

   [("RatEq.thy","solve_rat_equation")]));

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

 methods:= overwritel (!methods,

 [ 

  prep_met 

  (("RatEq.thy","solve_rat_equation"),

  (["RatEq","solve_rat_equation"],

    [("#Given" ,["equality e_","solveFor v_"]),

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

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

   ],

    {rew_ord'="termlessI",

     rls'=rateq_erls,

     srls=e_rls,

     prls=rateq_prls,

     asm_rls=["rat_simplify","rat_eliminate"],

     asm_rls=[],

     asm_thm=[("rat_double_rat_1",""),("rat_double_rat_2",""),("rat_double_rat_3",""),

              ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),

              ("rat_mult_denominator_right","")]},

    "Script Solve_rat_equation  (e_::bool) (v_::real) =                   \

     \(let e_ = ((Repeat(Try (Rewrite_Set rat_simplify       True))) @@   \

     \           (Repeat(Try (Rewrite_Set make_polynomial    False))) @@  \

     \           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  \

     \           (Repeat(Try (Rewrite_Set rat_eliminate       True)))) e_;\

     \                (RatEq_,no_met)) [bool_ e_, real_ v_])              \

     \                [no_met]) [bool_ e_, real_ v_])              \

    )

 ]);

    ));

 "******* RatEq.ML end *******";