infix mem union --> member union op = ...
\\ --> subtract op = [4,5,6,7] [1,2,3,4,5] -> [1, 2, 3]
missed due to problem with grep '\\'
1 (*.(c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for RationalEquations
10 (* use"IsacKnowledge/RatEq.ML";
18 "******* RatEq.ML begin *******";
20 theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]);
22 (*-------------------------functions-----------------------*)
23 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
24 fun is_rateqation_in t v =
26 fun coeff_in c v = member op = v (vars c);
27 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
28 (* at the moment there is no term like this, but ....*)
29 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
30 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
31 orelse (finddivide t2 v)
32 | finddivide (_ $ t1) v = (finddivide t1 v)
33 | finddivide _ _ = false;
38 fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
39 if is_rateqation_in t v then
40 SOME ((term2str p) ^ " = True",
41 Trueprop $ (mk_equality (p, HOLogic.true_const)))
42 else SOME ((term2str p) ^ " = True",
43 Trueprop $ (mk_equality (p, HOLogic.false_const)))
44 | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
46 (*-------------------------rulse-----------------------*)
47 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
48 append_rls "RatEq_prls" e_rls
49 [Calc ("Atools.ident",eval_ident "#ident_"),
50 Calc ("Tools.matches",eval_matches ""),
51 Calc ("Tools.lhs" ,eval_lhs ""),
52 Calc ("Tools.rhs" ,eval_rhs ""),
53 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
54 Calc ("op =",eval_equal "#equal_"),
55 Thm ("not_true",num_str not_true),
56 Thm ("not_false",num_str not_false),
57 Thm ("and_true",num_str and_true),
58 Thm ("and_false",num_str and_false),
59 Thm ("or_true",num_str or_true),
60 Thm ("or_false",num_str or_false)
64 (*rls = merge_rls erls Poly_erls *)
66 remove_rls "rateq_erls" (*WN: ein Hack*)
67 (merge_rls "is_ratequation_in" calculate_Rational
68 (append_rls "is_ratequation_in"
70 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*)
71 Calc ("RatEq.is'_ratequation'_in",
72 eval_is_ratequation_in "")
75 [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
76 Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
78 ruleset' := overwritelthy thy (!ruleset',
79 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
84 remove_rls "RatEq_crls" (*WN: ein Hack*)
85 (merge_rls "is_ratequation_in" calculate_Rational
86 (append_rls "is_ratequation_in"
88 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*)
89 Calc ("RatEq.is'_ratequation'_in",
90 eval_is_ratequation_in "")
92 [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
93 Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
96 val RatEq_eliminate = prep_rls(
97 Rls {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI",termlessI),
98 erls = rateq_erls, srls = Erls, calc = [],
99 (*asm_thm = [("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),
100 ("rat_mult_denominator_right","")],*)
102 Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both),
103 (* a/b=c/d -> ad=cb *)
104 Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left),
106 Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)
109 scr = Script ((term_of o the o (parse thy)) "empty_script")
111 ruleset' := overwritelthy thy (!ruleset',
112 [("RatEq_eliminate",RatEq_eliminate)
118 val RatEq_simplify = prep_rls(
119 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI",termlessI),
120 erls = rateq_erls, srls = Erls, calc = [],
121 (*asm_thm = [("rat_double_rat_1",""),("rat_double_rat_2",""),
122 ("rat_double_rat_3","")],*)
124 Thm("real_rat_mult_1",num_str real_rat_mult_1),
125 (*a*(b/c) = (a*b)/c*)
126 Thm("real_rat_mult_2",num_str real_rat_mult_2),
127 (*(a/b)*(c/d) = (a*c)/(b*d)*)
128 Thm("real_rat_mult_3",num_str real_rat_mult_3),
129 (* (a/b)*c = (a*c)/b*)
130 Thm("real_rat_pow",num_str real_rat_pow),
131 (*(a/b)^^^2 = a^^^2/b^^^2*)
132 Thm("real_diff_minus",num_str real_diff_minus),
133 (* a - b = a + (-1) * b *)
134 Thm("rat_double_rat_1",num_str rat_double_rat_1),
135 (* (a / (c/d) = (a*d) / c) *)
136 Thm("rat_double_rat_2",num_str rat_double_rat_2),
137 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
138 Thm("rat_double_rat_3",num_str rat_double_rat_3)
139 (* ((a/b) / c = a / (b*c) ) *)
141 scr = Script ((term_of o the o (parse thy)) "empty_script")
143 ruleset' := overwritelthy thy (!ruleset',
144 [("RatEq_simplify",RatEq_simplify)
147 (*-------------------------Problem-----------------------*)
149 (get_pbt ["rational","univariate","equation"]);
153 (prep_pbt RatEq.thy "pbl_equ_univ_rat" [] e_pblID
154 (["rational","univariate","equation"],
155 [("#Given" ,["equality e_","solveFor v_"]),
156 ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
157 ("#Find" ,["solutions v_i_"])
160 RatEq_prls, SOME "solve (e_::bool, v_)",
161 [["RatEq","solve_rat_equation"]]));
164 (*-------------------------methods-----------------------*)
166 (prep_met RatEq.thy "met_rateq" [] e_metID
169 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
170 crls=RatEq_crls, nrls=norm_Rational
171 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
173 (prep_met RatEq.thy "met_rat_eq" [] e_metID
174 (["RatEq","solve_rat_equation"],
175 [("#Given" ,["equality e_","solveFor v_"]),
176 ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
177 ("#Find" ,["solutions v_i_"])
179 {rew_ord'="termlessI",
184 crls=RatEq_crls, nrls=norm_Rational(*,
186 asm_thm=[("rat_double_rat_1",""),("rat_double_rat_2",""),("rat_double_rat_3",""),
187 ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""),
188 ("rat_mult_denominator_right","")]*)},
189 "Script Solve_rat_equation (e_::bool) (v_::real) = \
190 \(let e_ = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ \
191 \ (Repeat(Try (Rewrite_Set norm_Rational False))) @@ \
192 \ (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ \
193 \ (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_;\
194 \ (L_::bool list) = (SubProblem (RatEq_,[univariate,equation], \
195 \ [no_met]) [bool_ e_, real_ v_]) \
196 \ in Check_elementwise L_ {(v_::real). Assumptions})"
199 calclist':= overwritel (!calclist',
200 [("is_ratequation_in", ("RatEq.is_ratequation_in",
201 eval_is_ratequation_in ""))
203 "******* RatEq.ML end *******";