neuper@37906: (*.(c) by Richard Lang, 2003 .*)
neuper@37906: (* theory collecting all knowledge for RationalEquations
neuper@37906:    created by: rlang 
neuper@37906:          date: 02.08.12
neuper@37906:    changed by: rlang
neuper@37906:    last change by: rlang
neuper@37906:              date: 02.11.28
neuper@37906: *)
neuper@37906: 
neuper@37954: theory RatEq imports Rational begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
neuper@37906: 
neuper@37906:   (*----------------------scripts-----------------------*)
neuper@37906:   Solve'_rat'_equation
neuper@37954:              :: "[bool,real, 
neuper@37954: 		   bool list] => bool list"
neuper@37954:                ("((Script Solve'_rat'_equation (_ _ =))// 
neuper@37954:                   (_))" 9)
neuper@37906: 
neuper@37954: axioms 
neuper@37906:    (* FIXME also in Poly.thy def. --> FIXED*)
neuper@37906:    (*real_diff_minus            
neuper@37906:    "a - b = a + (-1) * b"*)
neuper@37983:    real_rat_mult_1:   "a*(b/c) = (a*b)/c"
neuper@37983:    real_rat_mult_2:   "(a/b)*(c/d) = (a*c)/(b*d)"
neuper@37983:    real_rat_mult_3:   "(a/b)*c = (a*c)/b"
neuper@37983:    real_rat_pow:      "(a/b)^^^2 = a^^^2/b^^^2"
neuper@37906: 
neuper@37983:    rat_double_rat_1:   "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
neuper@37983:    rat_double_rat_2:   "[|Not(b=0);Not(c=0); Not(d=0)|] ==> 
neuper@37983:                                            ((a/b) / (c/d) = (a*d) / (b*c))"
neuper@37983:    rat_double_rat_3:   "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
neuper@37906: 
neuper@37906:   (* equation to same denominator *)
neuper@37983:   rat_mult_denominator_both:
neuper@37906:    "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
neuper@37983:   rat_mult_denominator_left:
neuper@37906:    "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
neuper@37983:   rat_mult_denominator_right:
neuper@37906:    "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
neuper@37906: 
neuper@37954: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37954: (*-------------------------functions-----------------------*)
neuper@37954: (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
neuper@37954: fun is_rateqation_in t v = 
neuper@37954:     let 
neuper@37954: 	fun coeff_in c v = member op = (vars c) v;
neuper@37954:    	fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
neuper@37954: 	    (* at the moment there is no term like this, but ....*)
neuper@37954: 	  | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
neuper@37954: 	  | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) 
neuper@37954:                                          orelse (finddivide t2 v)
neuper@37954: 	  | finddivide (_ $ t1) v = (finddivide t1 v)
neuper@37954: 	  | finddivide _ _ = false;
neuper@37954:      in
neuper@37954: 	finddivide t v
neuper@37954:     end;
neuper@37954:     
neuper@37954: fun eval_is_ratequation_in _ _ 
neuper@37954:        (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _  =
neuper@37954:     if is_rateqation_in t v then 
neuper@37954: 	SOME ((term2str p) ^ " = True",
neuper@37954: 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37954:     else SOME ((term2str p) ^ " = True",
neuper@37954: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37954:   | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
neuper@37954: 
neuper@37954: (*-------------------------rulse-----------------------*)
neuper@37954: val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
neuper@37954:   append_rls "RatEq_prls" e_rls 
neuper@37954: 	     [Calc ("Atools.ident",eval_ident "#ident_"),
neuper@37954: 	      Calc ("Tools.matches",eval_matches ""),
neuper@37954: 	      Calc ("Tools.lhs"    ,eval_lhs ""),
neuper@37954: 	      Calc ("Tools.rhs"    ,eval_rhs ""),
neuper@37954: 	      Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
neuper@37954: 	      Calc ("op =",eval_equal "#equal_"),
neuper@37969: 	      Thm ("not_true",num_str @{thm not_true}),
neuper@37969: 	      Thm ("not_false",num_str @{thm not_false}),
neuper@37969: 	      Thm ("and_true",num_str @{thm and_true}),
neuper@37969: 	      Thm ("and_false",num_str @{thm and_false}),
neuper@37969: 	      Thm ("or_true",num_str @{thm or_true}),
neuper@37969: 	      Thm ("or_false",num_str @{thm or_false})
neuper@37954: 	      ];
neuper@37954: 
neuper@37954: 
neuper@37954: (*rls = merge_rls erls Poly_erls *)
neuper@37954: val rateq_erls = 
neuper@37954:     remove_rls "rateq_erls"                                   (*WN: ein Hack*)
neuper@37954: 	(merge_rls "is_ratequation_in" calculate_Rational
neuper@37954: 		   (append_rls "is_ratequation_in"
neuper@37954: 			Poly_erls
neuper@37981: 			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)
neuper@37954: 			 Calc ("RatEq.is'_ratequation'_in",
neuper@37954: 			       eval_is_ratequation_in "")
neuper@37954: 
neuper@37954: 			 ]))
neuper@37969: 	[Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)
neuper@37969: 	 Thm ("or_commute",num_str @{thm or_commute})    (*WN: ein Hack*)
neuper@37954: 	 ];
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954: 			[("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
neuper@37954: 			 ]);
neuper@37954: 
neuper@37954: 
neuper@37954: val RatEq_crls = 
neuper@37954:     remove_rls "RatEq_crls"                                   (*WN: ein Hack*)
neuper@37954: 	(merge_rls "is_ratequation_in" calculate_Rational
neuper@37954: 		   (append_rls "is_ratequation_in"
neuper@37954: 			Poly_erls
neuper@37981: 			[(*Calc ("HOL.divide", eval_cancel "#divide_e"),*)
neuper@37954: 			 Calc ("RatEq.is'_ratequation'_in",
neuper@37954: 			       eval_is_ratequation_in "")
neuper@37954: 			 ]))
neuper@37969: 	[Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)
neuper@37969: 	 Thm ("or_commute",num_str @{thm or_commute})    (*WN: ein Hack*)
neuper@37954: 	 ];
neuper@37954: 
neuper@37954: val RatEq_eliminate = prep_rls(
neuper@37954:   Rls {id = "RatEq_eliminate", preconds = [],
neuper@37954:        rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls, 
neuper@37954:        calc = [], 
neuper@37954:        rules = [
neuper@37969: 	    Thm("rat_mult_denominator_both",num_str @{thm rat_mult_denominator_both}), 
neuper@37954: 	     (* a/b=c/d -> ad=cb *)
neuper@37969: 	    Thm("rat_mult_denominator_left",num_str @{thm rat_mult_denominator_left}), 
neuper@37954: 	     (* a  =c/d -> ad=c  *)
neuper@37969: 	    Thm("rat_mult_denominator_right",num_str @{thm rat_mult_denominator_right})
neuper@37954: 	     (* a/b=c   ->  a=cb *)
neuper@37954: 	    ],
neuper@37954:     scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954:     }:rls);
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954: 			[("RatEq_eliminate",RatEq_eliminate)
neuper@37954: 			 ]);
neuper@37954: 
neuper@37954: val RatEq_simplify = prep_rls(
neuper@37954:   Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
neuper@37954:       erls = rateq_erls, srls = Erls, calc = [], 
neuper@37954:     rules = [
neuper@37969: 	     Thm("real_rat_mult_1",num_str @{thm real_rat_mult_1}),
neuper@37954: 	     (*a*(b/c) = (a*b)/c*)
neuper@37969: 	     Thm("real_rat_mult_2",num_str @{thm real_rat_mult_2}),
neuper@37954: 	     (*(a/b)*(c/d) = (a*c)/(b*d)*)
neuper@37969:              Thm("real_rat_mult_3",num_str @{thm real_rat_mult_3}),
neuper@37954:              (* (a/b)*c = (a*c)/b*)
neuper@37969: 	     Thm("real_rat_pow",num_str @{thm real_rat_pow}),
neuper@37954: 	     (*(a/b)^^^2 = a^^^2/b^^^2*)
neuper@37969: 	     Thm("real_diff_minus",num_str @{thm real_diff_minus}),
neuper@37954: 	     (* a - b = a + (-1) * b *)
neuper@37969:              Thm("rat_double_rat_1",num_str @{thm rat_double_rat_1}),
neuper@37954:              (* (a / (c/d) = (a*d) / c) *)
neuper@37969:              Thm("rat_double_rat_2",num_str @{thm rat_double_rat_2}), 
neuper@37954:              (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
neuper@37969:              Thm("rat_double_rat_3",num_str @{thm rat_double_rat_3}) 
neuper@37954:              (* ((a/b) / c = a / (b*c) ) *)
neuper@37954: 	     ],
neuper@37954:     scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954:     }:rls);
neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954: 			[("RatEq_simplify",RatEq_simplify)
neuper@37954: 			 ]);
neuper@37954: 
neuper@37954: (*-------------------------Problem-----------------------*)
neuper@37954: (*
neuper@37954: (get_pbt ["rational","univariate","equation"]);
neuper@37954: show_ptyps(); 
neuper@37954: *)
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
neuper@37954:  (["rational","univariate","equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982:    ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
neuper@37981:    ("#Find"  ,["solutions v_i"]) 
neuper@37954:   ],
neuper@37954: 
neuper@37981:   RatEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954:   [["RatEq","solve_rat_equation"]]));
neuper@37988: *}
neuper@37954: 
neuper@37988: ML {*
neuper@37954: (*-------------------------methods-----------------------*)
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_rateq" [] e_metID
neuper@37954:  (["RatEq"],
neuper@37954:    [],
neuper@37954:    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37954:     crls=RatEq_crls, nrls=norm_Rational
neuper@37954:     (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
neuper@37988: *}
neuper@37988: 
neuper@37988: ML {*
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_rat_eq" [] e_metID
neuper@37954:  (["RatEq","solve_rat_equation"],
neuper@37981:    [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982:    ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
neuper@37981:    ("#Find"  ,["solutions v_i"])
neuper@37954:   ],
neuper@37954:    {rew_ord'="termlessI",
neuper@37954:     rls'=rateq_erls,
neuper@37954:     srls=e_rls,
neuper@37954:     prls=RatEq_prls,
neuper@37954:     calc=[],
neuper@37954:     crls=RatEq_crls, nrls=norm_Rational},
neuper@37982:    "Script Solve_rat_equation  (e_e::bool) (v_v::real) =                   " ^
neuper@37981:     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^
neuper@37954:     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
neuper@37954:     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^
neuper@37988:     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^
neuper@37988:     " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
neuper@37988:     "                    [BOOL e_e, REAL v_v])                     " ^
neuper@37991:     " in Check_elementwise L_LL {(v_v::real). Assumptions})"
neuper@37954:    ));
neuper@37988: *}
neuper@37954: 
neuper@37988: ML {*
neuper@37954: calclist':= overwritel (!calclist', 
neuper@37954:    [("is_ratequation_in", ("RatEq.is_ratequation_in", 
neuper@37954: 			   eval_is_ratequation_in ""))
neuper@37954:     ]);
neuper@37954: *}
neuper@37906: 
neuper@37906: end