1.1 --- a/src/Tools/isac/IsacKnowledge/RatEq.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,203 +0,0 @@
1.4 -(*.(c) by Richard Lang, 2003 .*)
1.5 -(* collecting all knowledge for RationalEquations
1.6 - created by: rlang
1.7 - date: 02.09
1.8 - changed by: rlang
1.9 - last change by: rlang
1.10 - date: 02.11.29
1.11 -*)
1.12 -
1.13 -(* use"IsacKnowledge/RatEq.ML";
1.14 - use"RatEq.ML";
1.15 - remove_thy"RatEq";
1.16 - use_thy"Isac";
1.17 -
1.18 - use"ROOT.ML";
1.19 - cd"IsacKnowledge";
1.20 - *)
1.21 -"******* RatEq.ML begin *******";
1.22 -
1.23 -theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]);
1.24 -
1.25 -(*-------------------------functions-----------------------*)
1.26 -(* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
1.27 -fun is_rateqation_in t v =
1.28 - let
1.29 - fun coeff_in c v = member op = (vars c) v;
1.30 - fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
1.31 - (* at the moment there is no term like this, but ....*)
1.32 - | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
1.33 - | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
1.34 - orelse (finddivide t2 v)
1.35 - | finddivide (_ $ t1) v = (finddivide t1 v)
1.36 - | finddivide _ _ = false;
1.37 - in
1.38 - finddivide t v
1.39 - end;
1.40 -
1.41 -fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
1.42 - if is_rateqation_in t v then
1.43 - SOME ((term2str p) ^ " = True",
1.44 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.45 - else SOME ((term2str p) ^ " = True",
1.46 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.47 - | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.48 -
1.49 -(*-------------------------rulse-----------------------*)
1.50 -val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
1.51 - append_rls "RatEq_prls" e_rls
1.52 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.53 - Calc ("Tools.matches",eval_matches ""),
1.54 - Calc ("Tools.lhs" ,eval_lhs ""),
1.55 - Calc ("Tools.rhs" ,eval_rhs ""),
1.56 - Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
1.57 - Calc ("op =",eval_equal "#equal_"),
1.58 - Thm ("not_true",num_str not_true),
1.59 - Thm ("not_false",num_str not_false),
1.60 - Thm ("and_true",num_str and_true),
1.61 - Thm ("and_false",num_str and_false),
1.62 - Thm ("or_true",num_str or_true),
1.63 - Thm ("or_false",num_str or_false)
1.64 - ];
1.65 -
1.66 -
1.67 -(*rls = merge_rls erls Poly_erls *)
1.68 -val rateq_erls =
1.69 - remove_rls "rateq_erls" (*WN: ein Hack*)
1.70 - (merge_rls "is_ratequation_in" calculate_Rational
1.71 - (append_rls "is_ratequation_in"
1.72 - Poly_erls
1.73 - [(*Calc ("HOL.divide", eval_cancel "#divide_"),*)
1.74 - Calc ("RatEq.is'_ratequation'_in",
1.75 - eval_is_ratequation_in "")
1.76 -
1.77 - ]))
1.78 - [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
1.79 - Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
1.80 - ];
1.81 -ruleset' := overwritelthy thy (!ruleset',
1.82 - [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
1.83 - ]);
1.84 -
1.85 -
1.86 -val RatEq_crls =
1.87 - remove_rls "RatEq_crls" (*WN: ein Hack*)
1.88 - (merge_rls "is_ratequation_in" calculate_Rational
1.89 - (append_rls "is_ratequation_in"
1.90 - Poly_erls
1.91 - [(*Calc ("HOL.divide", eval_cancel "#divide_"),*)
1.92 - Calc ("RatEq.is'_ratequation'_in",
1.93 - eval_is_ratequation_in "")
1.94 - ]))
1.95 - [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
1.96 - Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
1.97 - ];
1.98 -
1.99 -val RatEq_eliminate = prep_rls(
1.100 - Rls {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI",termlessI),
1.101 - erls = rateq_erls, srls = Erls, calc = [],
1.102 - (*asm_thm = [("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),
1.103 - ("rat_mult_denominator_right","")],*)
1.104 - rules = [
1.105 - Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both),
1.106 - (* a/b=c/d -> ad=cb *)
1.107 - Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left),
1.108 - (* a =c/d -> ad=c *)
1.109 - Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)
1.110 - (* a/b=c -> a=cb *)
1.111 - ],
1.112 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.113 - }:rls);
1.114 -ruleset' := overwritelthy thy (!ruleset',
1.115 - [("RatEq_eliminate",RatEq_eliminate)
1.116 - ]);
1.117 -
1.118 -
1.119 -
1.120 -
1.121 -val RatEq_simplify = prep_rls(
1.122 - Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI",termlessI),
1.123 - erls = rateq_erls, srls = Erls, calc = [],
1.124 - (*asm_thm = [("rat_double_rat_1",""),("rat_double_rat_2",""),
1.125 - ("rat_double_rat_3","")],*)
1.126 - rules = [
1.127 - Thm("real_rat_mult_1",num_str real_rat_mult_1),
1.128 - (*a*(b/c) = (a*b)/c*)
1.129 - Thm("real_rat_mult_2",num_str real_rat_mult_2),
1.130 - (*(a/b)*(c/d) = (a*c)/(b*d)*)
1.131 - Thm("real_rat_mult_3",num_str real_rat_mult_3),
1.132 - (* (a/b)*c = (a*c)/b*)
1.133 - Thm("real_rat_pow",num_str real_rat_pow),
1.134 - (*(a/b)^^^2 = a^^^2/b^^^2*)
1.135 - Thm("real_diff_minus",num_str real_diff_minus),
1.136 - (* a - b = a + (-1) * b *)
1.137 - Thm("rat_double_rat_1",num_str rat_double_rat_1),
1.138 - (* (a / (c/d) = (a*d) / c) *)
1.139 - Thm("rat_double_rat_2",num_str rat_double_rat_2),
1.140 - (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
1.141 - Thm("rat_double_rat_3",num_str rat_double_rat_3)
1.142 - (* ((a/b) / c = a / (b*c) ) *)
1.143 - ],
1.144 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.145 - }:rls);
1.146 -ruleset' := overwritelthy thy (!ruleset',
1.147 - [("RatEq_simplify",RatEq_simplify)
1.148 - ]);
1.149 -
1.150 -(*-------------------------Problem-----------------------*)
1.151 -(*
1.152 -(get_pbt ["rational","univariate","equation"]);
1.153 -show_ptyps();
1.154 -*)
1.155 -store_pbt
1.156 - (prep_pbt RatEq.thy "pbl_equ_univ_rat" [] e_pblID
1.157 - (["rational","univariate","equation"],
1.158 - [("#Given" ,["equality e_","solveFor v_"]),
1.159 - ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
1.160 - ("#Find" ,["solutions v_i_"])
1.161 - ],
1.162 -
1.163 - RatEq_prls, SOME "solve (e_::bool, v_)",
1.164 - [["RatEq","solve_rat_equation"]]));
1.165 -
1.166 -
1.167 -(*-------------------------methods-----------------------*)
1.168 -store_met
1.169 - (prep_met RatEq.thy "met_rateq" [] e_metID
1.170 - (["RatEq"],
1.171 - [],
1.172 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.173 - crls=RatEq_crls, nrls=norm_Rational
1.174 - (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.175 -store_met
1.176 - (prep_met RatEq.thy "met_rat_eq" [] e_metID
1.177 - (["RatEq","solve_rat_equation"],
1.178 - [("#Given" ,["equality e_","solveFor v_"]),
1.179 - ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
1.180 - ("#Find" ,["solutions v_i_"])
1.181 - ],
1.182 - {rew_ord'="termlessI",
1.183 - rls'=rateq_erls,
1.184 - srls=e_rls,
1.185 - prls=RatEq_prls,
1.186 - calc=[],
1.187 - crls=RatEq_crls, nrls=norm_Rational(*,
1.188 - asm_rls=[],
1.189 - asm_thm=[("rat_double_rat_1",""),("rat_double_rat_2",""),("rat_double_rat_3",""),
1.190 - ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),
1.191 - ("rat_mult_denominator_right","")]*)},
1.192 - "Script Solve_rat_equation (e_::bool) (v_::real) = \
1.193 - \(let e_ = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ \
1.194 - \ (Repeat(Try (Rewrite_Set norm_Rational False))) @@ \
1.195 - \ (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ \
1.196 - \ (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_;\
1.197 - \ (L_::bool list) = (SubProblem (RatEq_,[univariate,equation], \
1.198 - \ [no_met]) [bool_ e_, real_ v_]) \
1.199 - \ in Check_elementwise L_ {(v_::real). Assumptions})"
1.200 - ));
1.201 -
1.202 -calclist':= overwritel (!calclist',
1.203 - [("is_ratequation_in", ("RatEq.is_ratequation_in",
1.204 - eval_is_ratequation_in ""))
1.205 - ]);
1.206 -"******* RatEq.ML end *******";