1 (*.(c) by Richard Lang, 2003 .*) |
|
2 (* collecting all knowledge for RationalEquations |
|
3 created by: rlang |
|
4 date: 02.09 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.11.29 |
|
8 *) |
|
9 |
|
10 (* use"IsacKnowledge/RatEq.ML"; |
|
11 use"RatEq.ML"; |
|
12 remove_thy"RatEq"; |
|
13 use_thy"Isac"; |
|
14 |
|
15 use"ROOT.ML"; |
|
16 cd"IsacKnowledge"; |
|
17 *) |
|
18 "******* RatEq.ML begin *******"; |
|
19 |
|
20 theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]); |
|
21 |
|
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 = |
|
25 let |
|
26 fun coeff_in c v = member op = (vars c) v; |
|
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; |
|
34 in |
|
35 finddivide t v |
|
36 end; |
|
37 |
|
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); |
|
45 |
|
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) |
|
61 ]; |
|
62 |
|
63 |
|
64 (*rls = merge_rls erls Poly_erls *) |
|
65 val rateq_erls = |
|
66 remove_rls "rateq_erls" (*WN: ein Hack*) |
|
67 (merge_rls "is_ratequation_in" calculate_Rational |
|
68 (append_rls "is_ratequation_in" |
|
69 Poly_erls |
|
70 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) |
|
71 Calc ("RatEq.is'_ratequation'_in", |
|
72 eval_is_ratequation_in "") |
|
73 |
|
74 ])) |
|
75 [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*) |
|
76 Thm ("or_commute",num_str or_commute) (*WN: ein Hack*) |
|
77 ]; |
|
78 ruleset' := overwritelthy thy (!ruleset', |
|
79 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*) |
|
80 ]); |
|
81 |
|
82 |
|
83 val RatEq_crls = |
|
84 remove_rls "RatEq_crls" (*WN: ein Hack*) |
|
85 (merge_rls "is_ratequation_in" calculate_Rational |
|
86 (append_rls "is_ratequation_in" |
|
87 Poly_erls |
|
88 [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) |
|
89 Calc ("RatEq.is'_ratequation'_in", |
|
90 eval_is_ratequation_in "") |
|
91 ])) |
|
92 [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*) |
|
93 Thm ("or_commute",num_str or_commute) (*WN: ein Hack*) |
|
94 ]; |
|
95 |
|
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","")],*) |
|
101 rules = [ |
|
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), |
|
105 (* a =c/d -> ad=c *) |
|
106 Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right) |
|
107 (* a/b=c -> a=cb *) |
|
108 ], |
|
109 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
110 }:rls); |
|
111 ruleset' := overwritelthy thy (!ruleset', |
|
112 [("RatEq_eliminate",RatEq_eliminate) |
|
113 ]); |
|
114 |
|
115 |
|
116 |
|
117 |
|
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","")],*) |
|
123 rules = [ |
|
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) ) *) |
|
140 ], |
|
141 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
142 }:rls); |
|
143 ruleset' := overwritelthy thy (!ruleset', |
|
144 [("RatEq_simplify",RatEq_simplify) |
|
145 ]); |
|
146 |
|
147 (*-------------------------Problem-----------------------*) |
|
148 (* |
|
149 (get_pbt ["rational","univariate","equation"]); |
|
150 show_ptyps(); |
|
151 *) |
|
152 store_pbt |
|
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_"]) |
|
158 ], |
|
159 |
|
160 RatEq_prls, SOME "solve (e_::bool, v_)", |
|
161 [["RatEq","solve_rat_equation"]])); |
|
162 |
|
163 |
|
164 (*-------------------------methods-----------------------*) |
|
165 store_met |
|
166 (prep_met RatEq.thy "met_rateq" [] e_metID |
|
167 (["RatEq"], |
|
168 [], |
|
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")); |
|
172 store_met |
|
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_"]) |
|
178 ], |
|
179 {rew_ord'="termlessI", |
|
180 rls'=rateq_erls, |
|
181 srls=e_rls, |
|
182 prls=RatEq_prls, |
|
183 calc=[], |
|
184 crls=RatEq_crls, nrls=norm_Rational(*, |
|
185 asm_rls=[], |
|
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})" |
|
197 )); |
|
198 |
|
199 calclist':= overwritel (!calclist', |
|
200 [("is_ratequation_in", ("RatEq.is_ratequation_in", |
|
201 eval_is_ratequation_in "")) |
|
202 ]); |
|
203 "******* RatEq.ML end *******"; |
|