neuper@37906
|
1 |
(*.(c) by Richard Lang, 2003 .*)
|
neuper@37906
|
2 |
(* theory collecting all knowledge for RationalEquations
|
neuper@37906
|
3 |
created by: rlang
|
neuper@37906
|
4 |
date: 02.08.12
|
neuper@37906
|
5 |
changed by: rlang
|
neuper@37906
|
6 |
last change by: rlang
|
neuper@37906
|
7 |
date: 02.11.28
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
s1210629013@55339
|
10 |
theory RatEq imports Rational Equation begin
|
neuper@37906
|
11 |
|
neuper@42398
|
12 |
text {* univariate equations over multivariate rational terms:
|
neuper@42398
|
13 |
In 2003 this type has been integrated into ISAC's equation solver
|
neuper@42398
|
14 |
by Richard Lang; the root for the solver is Equation.thy.
|
neuper@42398
|
15 |
The migration Isabelle2002 --> 2011 found that application of theorems like
|
neuper@42398
|
16 |
rat_mult_denominator_right: "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
|
neuper@42398
|
17 |
in rule-sets does not transfer "d ~= 0" to the assumptions; see
|
neuper@42398
|
18 |
test --- repair NO asms from rls RatEq_eliminate ---.
|
neuper@42398
|
19 |
Thus the migration dropped update of Check_elementwise, which would require
|
neuper@42398
|
20 |
these assumptions; see
|
neuper@42398
|
21 |
test --- pbl: rational, univariate, equation ---, --- x / (x ^ 2 - 6 * x + 9) - 1 /...
|
neuper@42398
|
22 |
*}
|
neuper@42398
|
23 |
|
neuper@37906
|
24 |
consts
|
neuper@37906
|
25 |
|
neuper@37906
|
26 |
is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*----------------------scripts-----------------------*)
|
neuper@37906
|
29 |
Solve'_rat'_equation
|
neuper@37954
|
30 |
:: "[bool,real,
|
neuper@37954
|
31 |
bool list] => bool list"
|
wneuper@59334
|
32 |
("((Script Solve'_rat'_equation (_ _ =))// (_))" 9)
|
neuper@37906
|
33 |
|
neuper@52148
|
34 |
axiomatization where
|
neuper@37906
|
35 |
(* FIXME also in Poly.thy def. --> FIXED*)
|
neuper@37906
|
36 |
(*real_diff_minus
|
neuper@37906
|
37 |
"a - b = a + (-1) * b"*)
|
neuper@52148
|
38 |
real_rat_mult_1: "a*(b/c) = (a*b)/c" and
|
neuper@52148
|
39 |
real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" and
|
neuper@52148
|
40 |
real_rat_mult_3: "(a/b)*c = (a*c)/b" and
|
neuper@52148
|
41 |
real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" and
|
neuper@37906
|
42 |
|
neuper@52148
|
43 |
rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" and
|
neuper@37983
|
44 |
rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==>
|
neuper@52148
|
45 |
((a/b) / (c/d) = (a*d) / (b*c))" and
|
neuper@52148
|
46 |
rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" and
|
neuper@37906
|
47 |
|
neuper@37906
|
48 |
(* equation to same denominator *)
|
neuper@37983
|
49 |
rat_mult_denominator_both:
|
neuper@52148
|
50 |
"[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" and
|
neuper@37983
|
51 |
rat_mult_denominator_left:
|
neuper@52148
|
52 |
"[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" and
|
neuper@37983
|
53 |
rat_mult_denominator_right:
|
neuper@37906
|
54 |
"[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
|
neuper@37906
|
55 |
|
neuper@37954
|
56 |
ML {*
|
neuper@37972
|
57 |
val thy = @{theory};
|
neuper@37972
|
58 |
|
neuper@37954
|
59 |
(*-------------------------functions-----------------------*)
|
neuper@37954
|
60 |
(* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
|
neuper@37954
|
61 |
fun is_rateqation_in t v =
|
neuper@37954
|
62 |
let
|
wneuper@59389
|
63 |
fun coeff_in c v = member op = (TermC.vars c) v;
|
neuper@38031
|
64 |
fun finddivide (_ $ _ $ _ $ _) v = error("is_rateqation_in:")
|
neuper@37954
|
65 |
(* at the moment there is no term like this, but ....*)
|
wneuper@59360
|
66 |
| finddivide (t as (Const ("Rings.divide_class.divide",_) $ _ $ b)) v = coeff_in b v
|
neuper@37954
|
67 |
| finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
|
neuper@37954
|
68 |
orelse (finddivide t2 v)
|
neuper@37954
|
69 |
| finddivide (_ $ t1) v = (finddivide t1 v)
|
neuper@37954
|
70 |
| finddivide _ _ = false;
|
neuper@37954
|
71 |
in
|
neuper@37954
|
72 |
finddivide t v
|
neuper@37954
|
73 |
end;
|
neuper@37954
|
74 |
|
neuper@37954
|
75 |
fun eval_is_ratequation_in _ _
|
neuper@37954
|
76 |
(p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
|
neuper@37954
|
77 |
if is_rateqation_in t v then
|
wneuper@59406
|
78 |
SOME ((Celem.term2str p) ^ " = True",
|
wneuper@59390
|
79 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
wneuper@59406
|
80 |
else SOME ((Celem.term2str p) ^ " = True",
|
wneuper@59390
|
81 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@38015
|
82 |
| eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
|
neuper@37954
|
83 |
|
neuper@37954
|
84 |
(*-------------------------rulse-----------------------*)
|
neuper@37954
|
85 |
val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
|
wneuper@59406
|
86 |
Celem.append_rls "RatEq_prls" Celem.e_rls
|
wneuper@59406
|
87 |
[Celem.Calc ("Atools.ident",eval_ident "#ident_"),
|
wneuper@59406
|
88 |
Celem.Calc ("Tools.matches",eval_matches ""),
|
wneuper@59406
|
89 |
Celem.Calc ("Tools.lhs" ,eval_lhs ""),
|
wneuper@59406
|
90 |
Celem.Calc ("Tools.rhs" ,eval_rhs ""),
|
wneuper@59406
|
91 |
Celem.Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
|
wneuper@59406
|
92 |
Celem.Calc ("HOL.eq",eval_equal "#equal_"),
|
wneuper@59406
|
93 |
Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
|
wneuper@59406
|
94 |
Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
|
wneuper@59406
|
95 |
Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
|
wneuper@59406
|
96 |
Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
|
wneuper@59406
|
97 |
Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
|
wneuper@59406
|
98 |
Celem.Thm ("or_false",TermC.num_str @{thm or_false})
|
neuper@37954
|
99 |
];
|
neuper@37954
|
100 |
|
neuper@37954
|
101 |
|
wneuper@59406
|
102 |
(*rls = Celem.merge_rls erls Poly_erls *)
|
neuper@37954
|
103 |
val rateq_erls =
|
wneuper@59406
|
104 |
Celem.remove_rls "rateq_erls" (*WN: ein Hack*)
|
wneuper@59406
|
105 |
(Celem.merge_rls "is_ratequation_in" calculate_Rational
|
wneuper@59406
|
106 |
(Celem.append_rls "is_ratequation_in"
|
neuper@37954
|
107 |
Poly_erls
|
wneuper@59406
|
108 |
[(*Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
|
wneuper@59406
|
109 |
Celem.Calc ("RatEq.is'_ratequation'_in",
|
neuper@37954
|
110 |
eval_is_ratequation_in "")
|
neuper@37954
|
111 |
|
neuper@37954
|
112 |
]))
|
wneuper@59406
|
113 |
[Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
|
wneuper@59406
|
114 |
Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}) (*WN: ein Hack*)
|
neuper@37954
|
115 |
];
|
neuper@52125
|
116 |
*}
|
neuper@52125
|
117 |
setup {* KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))] *}
|
neuper@52125
|
118 |
ML {*
|
neuper@37954
|
119 |
|
neuper@37954
|
120 |
val RatEq_crls =
|
wneuper@59406
|
121 |
Celem.remove_rls "RatEq_crls" (*WN: ein Hack*)
|
wneuper@59406
|
122 |
(Celem.merge_rls "is_ratequation_in" calculate_Rational
|
wneuper@59406
|
123 |
(Celem.append_rls "is_ratequation_in"
|
neuper@37954
|
124 |
Poly_erls
|
wneuper@59406
|
125 |
[(*Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
|
wneuper@59406
|
126 |
Celem.Calc ("RatEq.is'_ratequation'_in",
|
neuper@37954
|
127 |
eval_is_ratequation_in "")
|
neuper@37954
|
128 |
]))
|
wneuper@59406
|
129 |
[Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
|
wneuper@59406
|
130 |
Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}) (*WN: ein Hack*)
|
neuper@37954
|
131 |
];
|
neuper@37954
|
132 |
|
s1210629013@55444
|
133 |
val RatEq_eliminate = prep_rls'(
|
wneuper@59406
|
134 |
Celem.Rls {id = "RatEq_eliminate", preconds = [],
|
wneuper@59406
|
135 |
rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Celem.Erls,
|
neuper@42451
|
136 |
calc = [], errpatts = [],
|
neuper@37954
|
137 |
rules = [
|
wneuper@59406
|
138 |
Celem.Thm("rat_mult_denominator_both",TermC.num_str @{thm rat_mult_denominator_both}),
|
neuper@37954
|
139 |
(* a/b=c/d -> ad=cb *)
|
wneuper@59406
|
140 |
Celem.Thm("rat_mult_denominator_left",TermC.num_str @{thm rat_mult_denominator_left}),
|
neuper@37954
|
141 |
(* a =c/d -> ad=c *)
|
wneuper@59406
|
142 |
Celem.Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right})
|
neuper@37954
|
143 |
(* a/b=c -> a=cb *)
|
neuper@37954
|
144 |
],
|
wneuper@59406
|
145 |
scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
|
wneuper@59406
|
146 |
});
|
neuper@52125
|
147 |
*}
|
neuper@52125
|
148 |
setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",
|
neuper@52125
|
149 |
(Context.theory_name @{theory}, RatEq_eliminate))] *}
|
neuper@52125
|
150 |
ML {*
|
neuper@37954
|
151 |
|
s1210629013@55444
|
152 |
val RatEq_simplify = prep_rls'(
|
wneuper@59406
|
153 |
Celem.Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
|
wneuper@59406
|
154 |
erls = rateq_erls, srls = Celem.Erls, calc = [], errpatts = [],
|
neuper@37954
|
155 |
rules = [
|
wneuper@59406
|
156 |
Celem.Thm("real_rat_mult_1",TermC.num_str @{thm real_rat_mult_1}),
|
neuper@37954
|
157 |
(*a*(b/c) = (a*b)/c*)
|
wneuper@59406
|
158 |
Celem.Thm("real_rat_mult_2",TermC.num_str @{thm real_rat_mult_2}),
|
neuper@37954
|
159 |
(*(a/b)*(c/d) = (a*c)/(b*d)*)
|
wneuper@59406
|
160 |
Celem.Thm("real_rat_mult_3",TermC.num_str @{thm real_rat_mult_3}),
|
neuper@37954
|
161 |
(* (a/b)*c = (a*c)/b*)
|
wneuper@59406
|
162 |
Celem.Thm("real_rat_pow",TermC.num_str @{thm real_rat_pow}),
|
neuper@37954
|
163 |
(*(a/b)^^^2 = a^^^2/b^^^2*)
|
wneuper@59406
|
164 |
Celem.Thm("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
|
neuper@37954
|
165 |
(* a - b = a + (-1) * b *)
|
wneuper@59406
|
166 |
Celem.Thm("rat_double_rat_1",TermC.num_str @{thm rat_double_rat_1}),
|
neuper@37954
|
167 |
(* (a / (c/d) = (a*d) / c) *)
|
wneuper@59406
|
168 |
Celem.Thm("rat_double_rat_2",TermC.num_str @{thm rat_double_rat_2}),
|
neuper@37954
|
169 |
(* ((a/b) / (c/d) = (a*d) / (b*c)) *)
|
wneuper@59406
|
170 |
Celem.Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3})
|
neuper@37954
|
171 |
(* ((a/b) / c = a / (b*c) ) *)
|
neuper@37954
|
172 |
],
|
wneuper@59406
|
173 |
scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
|
wneuper@59406
|
174 |
});
|
neuper@52125
|
175 |
*}
|
neuper@52125
|
176 |
setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
|
neuper@52125
|
177 |
(Context.theory_name @{theory}, RatEq_simplify))] *}
|
neuper@52125
|
178 |
ML {*
|
neuper@37954
|
179 |
(*-------------------------Problem-----------------------*)
|
neuper@37954
|
180 |
(*
|
neuper@37954
|
181 |
(get_pbt ["rational","univariate","equation"]);
|
neuper@37954
|
182 |
show_ptyps();
|
neuper@37954
|
183 |
*)
|
neuper@37988
|
184 |
*}
|
s1210629013@55359
|
185 |
setup {* KEStore_Elems.add_pbts
|
wneuper@59406
|
186 |
[(Specify.prep_pbt thy "pbl_equ_univ_rat" [] Celem.e_pblID
|
s1210629013@55339
|
187 |
(["rational","univariate","equation"],
|
s1210629013@55339
|
188 |
[("#Given", ["equality e_e","solveFor v_v"]),
|
s1210629013@55339
|
189 |
("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),
|
s1210629013@55339
|
190 |
("#Find", ["solutions v_v'i'"])],
|
s1210629013@55339
|
191 |
RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq","solve_rat_equation"]]))] *}
|
neuper@37954
|
192 |
|
s1210629013@55373
|
193 |
(*-------------------------methods-----------------------*)
|
s1210629013@55373
|
194 |
setup {* KEStore_Elems.add_mets
|
wneuper@59406
|
195 |
[Specify.prep_met thy "met_rateq" [] Celem.e_metID
|
s1210629013@55373
|
196 |
(["RatEq"], [],
|
wneuper@59406
|
197 |
{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
|
s1210629013@55373
|
198 |
crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"),
|
wneuper@59406
|
199 |
Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
|
s1210629013@55373
|
200 |
(["RatEq", "solve_rat_equation"],
|
s1210629013@55373
|
201 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
s1210629013@55373
|
202 |
("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
|
s1210629013@55373
|
203 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59406
|
204 |
{rew_ord'="termlessI", rls'=rateq_erls, srls=Celem.e_rls, prls=RatEq_prls, calc=[],
|
s1210629013@55373
|
205 |
crls=RatEq_crls, errpats = [], nrls = norm_Rational},
|
s1210629013@55373
|
206 |
"Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
|
s1210629013@55373
|
207 |
"(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^
|
s1210629013@55373
|
208 |
" (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^
|
s1210629013@55373
|
209 |
" (Repeat(Try (Rewrite_Set add_fractions_p False))) @@ " ^
|
s1210629013@55373
|
210 |
" (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^
|
s1210629013@55373
|
211 |
" (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
|
s1210629013@55373
|
212 |
" [BOOL e_e, REAL v_v]) " ^
|
s1210629013@55373
|
213 |
" in Check_elementwise L_L {(v_v::real). Assumptions})")]
|
s1210629013@55373
|
214 |
*}
|
neuper@37954
|
215 |
|
s1210629013@52145
|
216 |
setup {* KEStore_Elems.add_calcs
|
s1210629013@52145
|
217 |
[("is_ratequation_in", ("RatEq.is_ratequation_in", eval_is_ratequation_in ""))] *}
|
neuper@37906
|
218 |
|
neuper@37906
|
219 |
end
|