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

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

   *)

"******* 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 = 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 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)

	      ];

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

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

			       eval_is_ratequation_in "")

			 ]))

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

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

	 ];

ruleset' := overwritelthy thy (!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_"),*)

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

			       eval_is_ratequation_in "")

			 ]))

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

	 Thm ("or_commute",num_str 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 = [], 

       (*asm_thm = [("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),

                  ("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' := overwritelthy thy (!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 = [], 

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

                  ("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' := overwritelthy thy (!ruleset',

			[("RatEq_simplify",RatEq_simplify)

			 ]);

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

(*

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

show_ptyps(); 

*)

store_pbt

 (prep_pbt RatEq.thy "pbl_equ_univ_rat" [] e_pblID

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

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

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

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

  ],

  RatEq_prls, SOME "solve (e_::bool, v_)",

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

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

store_met

 (prep_met RatEq.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 RatEq.thy "met_rat_eq" [] e_metID

 (["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,

    calc=[],

    crls=RatEq_crls, nrls=norm_Rational(*,

    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 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_, real_ v_])                     \

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

   ));

calclist':= overwritel (!calclist', 

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

			   eval_is_ratequation_in ""))

    ]);

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