neuper@52105
|
1 |
(* rationals, fractions of multivariate polynomials over the real field
|
neuper@37906
|
2 |
author: isac team
|
neuper@52105
|
3 |
Copyright (c) isac team 2002, 2013
|
neuper@37906
|
4 |
Use is subject to license terms.
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
depends on Poly (and not on Atools), because
|
wneuper@59370
|
7 |
fractions with _normalised_ polynomials are canceled, added, etc.
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@48884
|
10 |
theory Rational
|
wneuper@59553
|
11 |
imports Poly GCD_Poly_ML
|
neuper@48884
|
12 |
begin
|
neuper@37906
|
13 |
|
walther@60358
|
14 |
section \<open>Constants for evaluation by \ <^rule_eval>\<close>
|
neuper@37906
|
15 |
consts
|
neuper@37906
|
16 |
|
walther@60278
|
17 |
is_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
|
walther@60278
|
18 |
is_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
|
jan@42300
|
19 |
get_denominator :: "real => real"
|
walther@60017
|
20 |
get_numerator :: "real => real"
|
neuper@37906
|
21 |
|
wneuper@59472
|
22 |
ML \<open>
|
neuper@52105
|
23 |
(*.the expression contains + - * ^ / only ?.*)
|
neuper@52105
|
24 |
fun is_ratpolyexp (Free _) = true
|
wenzelm@60309
|
25 |
| is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true
|
wenzelm@60309
|
26 |
| is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true
|
wenzelm@60309
|
27 |
| is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true
|
wenzelm@60309
|
28 |
| is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free _) = true
|
wenzelm@60309
|
29 |
| is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ Free _ $ Free _) = true
|
wenzelm@60309
|
30 |
| is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
|
neuper@52105
|
31 |
((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
|
wenzelm@60309
|
32 |
| is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ t1 $ t2) =
|
neuper@52105
|
33 |
((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
|
wenzelm@60309
|
34 |
| is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) =
|
neuper@52105
|
35 |
((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
|
wenzelm@60309
|
36 |
| is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ t1 $ t2) =
|
neuper@52105
|
37 |
((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
|
wenzelm@60309
|
38 |
| is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) =
|
neuper@52105
|
39 |
((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
|
walther@60355
|
40 |
| is_ratpolyexp t = if TermC.is_num t then true else false;
|
neuper@37950
|
41 |
|
walther@60278
|
42 |
(*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
|
neuper@52105
|
43 |
fun eval_is_ratpolyexp (thmid:string) _
|
walther@60335
|
44 |
(t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) thy =
|
neuper@52105
|
45 |
if is_ratpolyexp arg
|
walther@59870
|
46 |
then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
|
wneuper@59390
|
47 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59870
|
48 |
else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
|
wneuper@59390
|
49 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
neuper@52105
|
50 |
| eval_is_ratpolyexp _ _ _ _ = NONE;
|
neuper@52105
|
51 |
|
neuper@52105
|
52 |
(*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
|
neuper@52105
|
53 |
fun eval_get_denominator (thmid:string) _
|
walther@60335
|
54 |
(t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
|
wenzelm@60309
|
55 |
(Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
|
neuper@52105
|
56 |
denom)) thy =
|
walther@59870
|
57 |
SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
|
wneuper@59390
|
58 |
HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
|
neuper@52105
|
59 |
| eval_get_denominator _ _ _ _ = NONE;
|
neuper@52105
|
60 |
|
neuper@52105
|
61 |
(*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
|
neuper@52105
|
62 |
fun eval_get_numerator (thmid:string) _
|
walther@60335
|
63 |
(t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
|
wenzelm@60309
|
64 |
(Const (\<^const_name>\<open>divide\<close>, _) $num
|
neuper@52105
|
65 |
$denom )) thy =
|
walther@59870
|
66 |
SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
|
wneuper@59390
|
67 |
HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
|
neuper@52105
|
68 |
| eval_get_numerator _ _ _ _ = NONE;
|
wneuper@59472
|
69 |
\<close>
|
neuper@52105
|
70 |
|
wneuper@59472
|
71 |
section \<open>Theorems for rewriting\<close>
|
neuper@52105
|
72 |
|
neuper@52105
|
73 |
axiomatization (* naming due to Isabelle2002, but not contained in Isabelle2002;
|
neuper@52105
|
74 |
many thms are due to RL and can be removed with updating the equation solver;
|
neuper@52105
|
75 |
TODO: replace by equivalent thms in recent Isabelle201x *)
|
neuper@52105
|
76 |
where
|
neuper@52105
|
77 |
mult_cross: "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" and
|
neuper@52105
|
78 |
mult_cross1: " b ~= 0 ==> (a / b = c ) = (a = b * c)" and
|
neuper@52105
|
79 |
mult_cross2: " d ~= 0 ==> (a = c / d) = (a * d = c)" and
|
neuper@37950
|
80 |
|
neuper@52105
|
81 |
add_minus: "a + b - b = a"(*RL->Poly.thy*) and
|
neuper@52105
|
82 |
add_minus1: "a - b + b = a"(*RL->Poly.thy*) and
|
neuper@37950
|
83 |
|
neuper@52105
|
84 |
rat_mult: "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) and
|
neuper@52105
|
85 |
rat_mult2: "a / b * c = a * c / b "(*?Isa02*) and
|
t@42211
|
86 |
|
neuper@52105
|
87 |
rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" and
|
neuper@52105
|
88 |
rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" and
|
neuper@37906
|
89 |
|
neuper@37906
|
90 |
(*real_times_divide1_eq .. Isa02*)
|
neuper@52105
|
91 |
real_times_divide_1_eq: "-1 * (c / d) = -1 * c / d " and
|
neuper@52105
|
92 |
real_times_divide_num: "a is_const ==> a * (c / d) = a * c / d " and
|
t@42211
|
93 |
|
neuper@52105
|
94 |
real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and
|
neuper@37978
|
95 |
(*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
|
neuper@37906
|
96 |
|
neuper@52105
|
97 |
real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and
|
neuper@52105
|
98 |
real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and
|
neuper@37978
|
99 |
(*real_divide_divide2_eq: "x / y / z = x / (y * z)"..Isa02*)
|
neuper@37906
|
100 |
|
walther@60242
|
101 |
rat_power: "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
|
neuper@37978
|
102 |
|
neuper@37978
|
103 |
rat_add: "[| a is_const; b is_const; c is_const; d is_const |] ==>
|
neuper@52105
|
104 |
a / c + b / d = (a * d + b * c) / (c * d)" and
|
neuper@37978
|
105 |
rat_add_assoc: "[| a is_const; b is_const; c is_const; d is_const |] ==>
|
neuper@52105
|
106 |
a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
|
neuper@37978
|
107 |
rat_add1: "[| a is_const; b is_const; c is_const |] ==>
|
neuper@52105
|
108 |
a / c + b / c = (a + b) / c" and
|
neuper@37978
|
109 |
rat_add1_assoc: "[| a is_const; b is_const; c is_const |] ==>
|
neuper@52105
|
110 |
a / c + (b / c + e) = (a + b) / c + e" and
|
neuper@37978
|
111 |
rat_add2: "[| a is_const; b is_const; c is_const |] ==>
|
neuper@52105
|
112 |
a / c + b = (a + b * c) / c" and
|
neuper@37978
|
113 |
rat_add2_assoc: "[| a is_const; b is_const; c is_const |] ==>
|
neuper@52105
|
114 |
a / c + (b + e) = (a + b * c) / c + e" and
|
neuper@37978
|
115 |
rat_add3: "[| a is_const; b is_const; c is_const |] ==>
|
neuper@52105
|
116 |
a + b / c = (a * c + b) / c" and
|
neuper@37978
|
117 |
rat_add3_assoc: "[| a is_const; b is_const; c is_const |] ==>
|
neuper@37950
|
118 |
a + (b / c + e) = (a * c + b) / c + e"
|
neuper@37950
|
119 |
|
wneuper@59472
|
120 |
section \<open>Cancellation and addition of fractions\<close>
|
wneuper@59472
|
121 |
subsection \<open>Conversion term <--> poly\<close>
|
wneuper@59472
|
122 |
subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
|
wneuper@59472
|
123 |
ML \<open>
|
walther@60347
|
124 |
fun monom_of_term vs (_, es) (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
|
walther@60347
|
125 |
(0, list_update es (find_index (curry op = t) vs) 1)
|
walther@60347
|
126 |
| monom_of_term vs (c, es) (t as Const _) =
|
wneuper@59532
|
127 |
(c, list_update es (find_index (curry op = t) vs) 1)
|
walther@60335
|
128 |
| monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
|
walther@60319
|
129 |
(t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
|
walther@60335
|
130 |
| monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
|
walther@60319
|
131 |
(t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
|
walther@60318
|
132 |
| monom_of_term vs (c, es) (t as Free _) =
|
walther@60318
|
133 |
(c, list_update es (find_index (curry op = t) vs) 1)
|
walther@60347
|
134 |
| monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
|
walther@60335
|
135 |
(e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
|
walther@60319
|
136 |
(c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
|
walther@60347
|
137 |
| monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
|
walther@60335
|
138 |
(e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
|
walther@60319
|
139 |
(c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
|
walther@60331
|
140 |
|
wenzelm@60309
|
141 |
| monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
|
neuper@52087
|
142 |
let val (c', es') = monom_of_term vs (c, es) m1
|
neuper@52087
|
143 |
in monom_of_term vs (c', es') m2 end
|
walther@59868
|
144 |
| monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
|
neuper@52087
|
145 |
|
walther@60318
|
146 |
(*-------v------*)
|
walther@60347
|
147 |
fun monoms_of_term vs (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
|
walther@60347
|
148 |
[monom_of_term vs (0, replicate (length vs) 0) t]
|
walther@60347
|
149 |
| monoms_of_term vs (t as Const _) =
|
wneuper@59531
|
150 |
[monom_of_term vs (1, replicate (length vs) 0) t]
|
walther@60335
|
151 |
| monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
|
walther@60319
|
152 |
[monom_of_term vs (1, replicate (length vs) 0) t]
|
walther@60335
|
153 |
| monoms_of_term vs (t as Const (\<^const_name>\<open>uminus\<close>, _) $ _) =
|
walther@60319
|
154 |
[monom_of_term vs (1, replicate (length vs) 0) t]
|
wneuper@59531
|
155 |
| monoms_of_term vs (t as Free _) =
|
neuper@52087
|
156 |
[monom_of_term vs (1, replicate (length vs) 0) t]
|
wenzelm@60309
|
157 |
| monoms_of_term vs (t as Const (\<^const_name>\<open>powr\<close>, _) $ _ $ _) =
|
neuper@52087
|
158 |
[monom_of_term vs (1, replicate (length vs) 0) t]
|
wenzelm@60309
|
159 |
| monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $ _) =
|
neuper@52087
|
160 |
[monom_of_term vs (1, replicate (length vs) 0) t]
|
wenzelm@60309
|
161 |
| monoms_of_term vs (Const (\<^const_name>\<open>plus\<close>, _) $ ms1 $ ms2) =
|
neuper@52087
|
162 |
(monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
|
walther@59868
|
163 |
| monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
|
neuper@52087
|
164 |
|
neuper@52087
|
165 |
(* convert a term to the internal representation of a multivariate polynomial;
|
neuper@52087
|
166 |
the conversion is quite liberal, see test --- fun poly_of_term ---:
|
neuper@52087
|
167 |
* the order of variables and the parentheses within a monomial are arbitrary
|
neuper@52087
|
168 |
* the coefficient may be somewhere
|
neuper@52087
|
169 |
* he order and the parentheses within monomials are arbitrary
|
neuper@52087
|
170 |
But the term must be completely expand + over * (laws of distributivity are not applicable).
|
neuper@52087
|
171 |
|
neuper@52087
|
172 |
The function requires the free variables as strings already given,
|
neuper@52087
|
173 |
because the gcd involves 2 polynomials (with the same length for their list of exponents).
|
neuper@52087
|
174 |
*)
|
wenzelm@60309
|
175 |
fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
|
neuper@52101
|
176 |
(SOME (t |> monoms_of_term vs |> order)
|
neuper@52087
|
177 |
handle ERROR _ => NONE)
|
walther@60347
|
178 |
| poly_of_term vs t = (* 0 for zero polynomial *)
|
neuper@52101
|
179 |
(SOME [monom_of_term vs (1, replicate (length vs) 0) t]
|
neuper@52087
|
180 |
handle ERROR _ => NONE)
|
neuper@52087
|
181 |
|
neuper@52087
|
182 |
fun is_poly t =
|
wneuper@59532
|
183 |
let
|
wneuper@59532
|
184 |
val vs = TermC.vars_of t
|
neuper@52087
|
185 |
in
|
neuper@52087
|
186 |
case poly_of_term vs t of SOME _ => true | NONE => false
|
neuper@52087
|
187 |
end
|
neuper@52105
|
188 |
val is_expanded = is_poly (* TODO: check names *)
|
neuper@52105
|
189 |
val is_polynomial = is_poly (* TODO: check names *)
|
wneuper@59472
|
190 |
\<close>
|
neuper@52087
|
191 |
|
wneuper@59472
|
192 |
subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
|
wneuper@59472
|
193 |
ML \<open>
|
neuper@52087
|
194 |
fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
|
wneuper@59532
|
195 |
| term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
|
wneuper@59532
|
196 |
| term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
|
neuper@52087
|
197 |
| term_of_es baseT expT (v :: vs) (e :: es) =
|
walther@60335
|
198 |
Const (\<^const_name>\<open>Transcendental.powr\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
|
wneuper@59532
|
199 |
:: term_of_es baseT expT vs es
|
wneuper@59532
|
200 |
| term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
|
neuper@52087
|
201 |
|
neuper@52087
|
202 |
fun term_of_monom baseT expT vs ((c, es): monom) =
|
neuper@52087
|
203 |
let val es' = term_of_es baseT expT vs es
|
neuper@52087
|
204 |
in
|
neuper@52087
|
205 |
if c = 1
|
neuper@52087
|
206 |
then
|
neuper@52087
|
207 |
if es' = [] (*if es = [0,0,0,...]*)
|
walther@60317
|
208 |
then HOLogic.mk_number baseT c
|
neuper@52087
|
209 |
else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
|
walther@60317
|
210 |
else foldl (HOLogic.mk_binop "Groups.times_class.times")
|
walther@60317
|
211 |
(HOLogic.mk_number baseT c, es')
|
neuper@52087
|
212 |
end
|
neuper@52087
|
213 |
|
neuper@52087
|
214 |
fun term_of_poly baseT expT vs p =
|
wneuper@59190
|
215 |
let val monos = map (term_of_monom baseT expT vs) p
|
wenzelm@60309
|
216 |
in foldl (HOLogic.mk_binop \<^const_name>\<open>plus\<close>) (hd monos, tl monos) end
|
wneuper@59472
|
217 |
\<close>
|
neuper@52087
|
218 |
|
wneuper@59472
|
219 |
subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
|
wneuper@59472
|
220 |
ML \<open>
|
neuper@52091
|
221 |
fun mk_noteq_0 baseT t =
|
walther@60335
|
222 |
Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
|
walther@60335
|
223 |
(Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
|
neuper@52091
|
224 |
|
neuper@52094
|
225 |
fun mk_asms baseT ts =
|
wneuper@59389
|
226 |
let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
|
neuper@52094
|
227 |
in map (mk_noteq_0 baseT) as' end
|
wneuper@59472
|
228 |
\<close>
|
neuper@52094
|
229 |
|
wneuper@59472
|
230 |
subsubsection \<open>Factor out gcd for cancellation\<close>
|
wneuper@59472
|
231 |
ML \<open>
|
neuper@52091
|
232 |
fun check_fraction t =
|
walther@60269
|
233 |
case t of
|
wenzelm@60309
|
234 |
Const (\<^const_name>\<open>divide\<close>, _) $ numerator $ denominator
|
walther@60269
|
235 |
=> SOME (numerator, denominator)
|
walther@60269
|
236 |
| _ => NONE
|
neuper@52091
|
237 |
|
neuper@52091
|
238 |
(* prepare a term for cancellation by factoring out the gcd
|
neuper@52091
|
239 |
assumes: is a fraction with outmost "/"*)
|
neuper@52091
|
240 |
fun factout_p_ (thy: theory) t =
|
neuper@52091
|
241 |
let val opt = check_fraction t
|
neuper@52091
|
242 |
in
|
neuper@52091
|
243 |
case opt of
|
neuper@52091
|
244 |
NONE => NONE
|
neuper@52091
|
245 |
| SOME (numerator, denominator) =>
|
wneuper@59532
|
246 |
let
|
wneuper@59532
|
247 |
val vs = TermC.vars_of t
|
neuper@52091
|
248 |
val baseT = type_of numerator
|
neuper@52091
|
249 |
val expT = HOLogic.realT
|
neuper@52091
|
250 |
in
|
neuper@52091
|
251 |
case (poly_of_term vs numerator, poly_of_term vs denominator) of
|
neuper@52091
|
252 |
(SOME a, SOME b) =>
|
neuper@52091
|
253 |
let
|
neuper@52091
|
254 |
val ((a', b'), c) = gcd_poly a b
|
neuper@52096
|
255 |
val es = replicate (length vs) 0
|
neuper@52096
|
256 |
in
|
neuper@52096
|
257 |
if c = [(1, es)] orelse c = [(~1, es)]
|
neuper@52096
|
258 |
then NONE
|
neuper@52096
|
259 |
else
|
neuper@52096
|
260 |
let
|
neuper@52096
|
261 |
val b't = term_of_poly baseT expT vs b'
|
neuper@52096
|
262 |
val ct = term_of_poly baseT expT vs c
|
neuper@52096
|
263 |
val t' =
|
wenzelm@60309
|
264 |
HOLogic.mk_binop \<^const_name>\<open>divide\<close>
|
wenzelm@60309
|
265 |
(HOLogic.mk_binop \<^const_name>\<open>times\<close>
|
wneuper@59190
|
266 |
(term_of_poly baseT expT vs a', ct),
|
wenzelm@60309
|
267 |
HOLogic.mk_binop \<^const_name>\<open>times\<close> (b't, ct))
|
neuper@52105
|
268 |
in SOME (t', mk_asms baseT [b't, ct]) end
|
neuper@52096
|
269 |
end
|
neuper@52091
|
270 |
| _ => NONE : (term * term list) option
|
neuper@52091
|
271 |
end
|
neuper@52091
|
272 |
end
|
wneuper@59472
|
273 |
\<close>
|
neuper@52091
|
274 |
|
wneuper@59472
|
275 |
subsubsection \<open>Cancel a fraction\<close>
|
wneuper@59472
|
276 |
ML \<open>
|
neuper@52096
|
277 |
(* cancel a term by the gcd ("" denote terms with internal algebraic structure)
|
walther@60347
|
278 |
cancel_p_ : theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
|
neuper@52096
|
279 |
cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
|
neuper@52096
|
280 |
assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
|
neuper@52096
|
281 |
yields
|
neuper@52096
|
282 |
SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
|
neuper@52096
|
283 |
a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
|
neuper@52096
|
284 |
\<or> NONE *)
|
neuper@52101
|
285 |
fun cancel_p_ (_: theory) t =
|
neuper@52091
|
286 |
let val opt = check_fraction t
|
neuper@52091
|
287 |
in
|
neuper@52091
|
288 |
case opt of
|
neuper@52091
|
289 |
NONE => NONE
|
neuper@52091
|
290 |
| SOME (numerator, denominator) =>
|
wneuper@59532
|
291 |
let
|
wneuper@59532
|
292 |
val vs = TermC.vars_of t
|
neuper@52091
|
293 |
val baseT = type_of numerator
|
neuper@52091
|
294 |
val expT = HOLogic.realT
|
neuper@52091
|
295 |
in
|
neuper@52091
|
296 |
case (poly_of_term vs numerator, poly_of_term vs denominator) of
|
neuper@52091
|
297 |
(SOME a, SOME b) =>
|
neuper@52091
|
298 |
let
|
neuper@52091
|
299 |
val ((a', b'), c) = gcd_poly a b
|
neuper@52096
|
300 |
val es = replicate (length vs) 0
|
neuper@52096
|
301 |
in
|
neuper@52096
|
302 |
if c = [(1, es)] orelse c = [(~1, es)]
|
neuper@52096
|
303 |
then NONE
|
neuper@52096
|
304 |
else
|
neuper@52096
|
305 |
let
|
neuper@52096
|
306 |
val bt' = term_of_poly baseT expT vs b'
|
neuper@52096
|
307 |
val ct = term_of_poly baseT expT vs c
|
neuper@52096
|
308 |
val t' =
|
wenzelm@60309
|
309 |
HOLogic.mk_binop \<^const_name>\<open>divide\<close>
|
wneuper@59190
|
310 |
(term_of_poly baseT expT vs a', bt')
|
neuper@52096
|
311 |
val asm = mk_asms baseT [bt']
|
neuper@52096
|
312 |
in SOME (t', asm) end
|
neuper@52096
|
313 |
end
|
neuper@52091
|
314 |
| _ => NONE : (term * term list) option
|
neuper@52091
|
315 |
end
|
neuper@52091
|
316 |
end
|
wneuper@59472
|
317 |
\<close>
|
neuper@52091
|
318 |
|
wneuper@59472
|
319 |
subsubsection \<open>Factor out to a common denominator for addition\<close>
|
wneuper@59472
|
320 |
ML \<open>
|
neuper@52101
|
321 |
(* addition of fractions allows (at most) one non-fraction (a monomial) *)
|
neuper@52101
|
322 |
fun check_frac_sum
|
wenzelm@60309
|
323 |
(Const (\<^const_name>\<open>plus\<close>, _) $
|
wenzelm@60309
|
324 |
(Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
|
wenzelm@60309
|
325 |
(Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
|
neuper@52091
|
326 |
= SOME ((n1, d1), (n2, d2))
|
neuper@52101
|
327 |
| check_frac_sum
|
wenzelm@60309
|
328 |
(Const (\<^const_name>\<open>plus\<close>, _) $
|
neuper@52091
|
329 |
nofrac $
|
wenzelm@60309
|
330 |
(Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
|
walther@60347
|
331 |
= SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
|
neuper@52101
|
332 |
| check_frac_sum
|
wenzelm@60309
|
333 |
(Const (\<^const_name>\<open>plus\<close>, _) $
|
wenzelm@60309
|
334 |
(Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
|
neuper@52091
|
335 |
nofrac)
|
walther@60317
|
336 |
= SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
|
neuper@52101
|
337 |
| check_frac_sum _ = NONE
|
neuper@52091
|
338 |
|
neuper@52091
|
339 |
(* prepare a term for addition by providing the least common denominator as a product
|
neuper@52091
|
340 |
assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
|
neuper@52101
|
341 |
fun common_nominator_p_ (_: theory) t =
|
neuper@52101
|
342 |
let val opt = check_frac_sum t
|
neuper@52091
|
343 |
in
|
neuper@52091
|
344 |
case opt of
|
neuper@52091
|
345 |
NONE => NONE
|
neuper@52091
|
346 |
| SOME ((n1, d1), (n2, d2)) =>
|
wneuper@59532
|
347 |
let
|
wneuper@59532
|
348 |
val vs = TermC.vars_of t
|
neuper@52091
|
349 |
in
|
neuper@52091
|
350 |
case (poly_of_term vs d1, poly_of_term vs d2) of
|
neuper@52091
|
351 |
(SOME a, SOME b) =>
|
neuper@52091
|
352 |
let
|
neuper@52091
|
353 |
val ((a', b'), c) = gcd_poly a b
|
neuper@52101
|
354 |
val (baseT, expT) = (type_of n1, HOLogic.realT)
|
wneuper@59190
|
355 |
val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
|
neuper@52091
|
356 |
(*----- minimum of parentheses & nice result, but breaks tests: -------------
|
wenzelm@60309
|
357 |
val denom = HOLogic.mk_binop \<^const_name>\<open>times\<close>
|
wenzelm@60309
|
358 |
(HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2'), c') -------------*)
|
neuper@52101
|
359 |
val denom =
|
neuper@52101
|
360 |
if c = [(1, replicate (length vs) 0)]
|
wenzelm@60309
|
361 |
then HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')
|
neuper@52101
|
362 |
else
|
wenzelm@60309
|
363 |
HOLogic.mk_binop \<^const_name>\<open>times\<close> (c',
|
wenzelm@60309
|
364 |
HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')) (*--------------*)
|
neuper@52091
|
365 |
val t' =
|
wenzelm@60309
|
366 |
HOLogic.mk_binop \<^const_name>\<open>plus\<close>
|
wenzelm@60309
|
367 |
(HOLogic.mk_binop \<^const_name>\<open>divide\<close>
|
wenzelm@60309
|
368 |
(HOLogic.mk_binop \<^const_name>\<open>times\<close> (n1, d2'), denom),
|
wenzelm@60309
|
369 |
HOLogic.mk_binop \<^const_name>\<open>divide\<close>
|
wenzelm@60309
|
370 |
(HOLogic.mk_binop \<^const_name>\<open>times\<close> (n2, d1'), denom))
|
neuper@52094
|
371 |
val asm = mk_asms baseT [d1', d2', c']
|
neuper@52091
|
372 |
in SOME (t', asm) end
|
neuper@52091
|
373 |
| _ => NONE : (term * term list) option
|
neuper@52091
|
374 |
end
|
neuper@52091
|
375 |
end
|
wneuper@59472
|
376 |
\<close>
|
neuper@52105
|
377 |
|
wneuper@59472
|
378 |
subsubsection \<open>Addition of at least one fraction within a sum\<close>
|
wneuper@59472
|
379 |
ML \<open>
|
neuper@52091
|
380 |
(* add fractions
|
neuper@52100
|
381 |
assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
|
walther@60347
|
382 |
\<and> NONE of the summands is zero.
|
walther@60347
|
383 |
NOTE: the case "(_ + _) + _" need not be considered due to iterated addition *)
|
neuper@52105
|
384 |
fun add_fraction_p_ (_: theory) t =
|
neuper@52101
|
385 |
case check_frac_sum t of
|
neuper@52101
|
386 |
NONE => NONE
|
neuper@52101
|
387 |
| SOME ((n1, d1), (n2, d2)) =>
|
wneuper@59532
|
388 |
let
|
wneuper@59532
|
389 |
val vs = TermC.vars_of t
|
neuper@52101
|
390 |
in
|
neuper@52101
|
391 |
case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
|
neuper@52101
|
392 |
(SOME _, SOME a, SOME _, SOME b) =>
|
neuper@52101
|
393 |
let
|
neuper@52101
|
394 |
val ((a', b'), c) = gcd_poly a b
|
neuper@52101
|
395 |
val (baseT, expT) = (type_of n1, HOLogic.realT)
|
neuper@52101
|
396 |
val nomin = term_of_poly baseT expT vs
|
neuper@52101
|
397 |
(((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
|
neuper@52101
|
398 |
val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
|
wenzelm@60309
|
399 |
val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom)
|
neuper@52101
|
400 |
in SOME (t', mk_asms baseT [denom]) end
|
neuper@52101
|
401 |
| _ => NONE : (term * term list) option
|
neuper@52101
|
402 |
end
|
wneuper@59472
|
403 |
\<close>
|
neuper@52091
|
404 |
|
wneuper@59472
|
405 |
section \<open>Embed cancellation and addition into rewriting\<close>
|
wenzelm@60291
|
406 |
|
wneuper@59472
|
407 |
subsection \<open>Rulesets and predicate for embedding\<close>
|
wneuper@59472
|
408 |
ML \<open>
|
neuper@52105
|
409 |
(* evaluates conditions in calculate_Rational *)
|
neuper@52105
|
410 |
val calc_rat_erls =
|
s1210629013@55444
|
411 |
prep_rls'
|
walther@59857
|
412 |
(Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59852
|
413 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
414 |
rules = [
|
walther@60358
|
415 |
\<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
|
walther@60358
|
416 |
\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
|
walther@60358
|
417 |
\<^rule_eval>\<open>is_const\<close> (Prog_Expr.eval_const "#is_const_"),
|
walther@60358
|
418 |
\<^rule_thm>\<open>not_true\<close>,
|
walther@60358
|
419 |
\<^rule_thm>\<open>not_false\<close>],
|
walther@59878
|
420 |
scr = Rule.Empty_Prog});
|
neuper@37950
|
421 |
|
neuper@52105
|
422 |
(* simplifies expressions with numerals;
|
neuper@52105
|
423 |
does NOT rearrange the term by AC-rewriting; thus terms with variables
|
neuper@52105
|
424 |
need to have constants to be commuted together respectively *)
|
neuper@52105
|
425 |
val calculate_Rational =
|
walther@59852
|
426 |
prep_rls' (Rule_Set.merge "calculate_Rational"
|
walther@59857
|
427 |
(Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59851
|
428 |
erls = calc_rat_erls, srls = Rule_Set.Empty,
|
neuper@52105
|
429 |
calc = [], errpatts = [],
|
walther@60358
|
430 |
rules = [
|
walther@60358
|
431 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
neuper@37950
|
432 |
|
walther@60358
|
433 |
\<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
|
wenzelm@60297
|
434 |
\<^rule_thm>\<open>rat_add\<close>,
|
walther@60358
|
435 |
(*"[| a is_const; b is_const; c is_const; d is_const |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
|
walther@60358
|
436 |
\<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
|
walther@60358
|
437 |
\<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
|
walther@60358
|
438 |
\<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c" *)
|
neuper@52105
|
439 |
|
walther@60358
|
440 |
\<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
|
walther@60358
|
441 |
\<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
|
walther@60358
|
442 |
\<^rule_thm>\<open>times_divide_eq_left\<close>, (*?y / ?z * ?x = ?y * ?x / ?z*)
|
neuper@52105
|
443 |
|
walther@60358
|
444 |
\<^rule_thm>\<open>real_divide_divide1\<close>, (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
|
walther@60358
|
445 |
\<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
|
neuper@52105
|
446 |
|
walther@60358
|
447 |
\<^rule_thm>\<open>rat_power\<close>, (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
|
neuper@52105
|
448 |
|
walther@60358
|
449 |
\<^rule_thm>\<open>mult_cross\<close>, (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
|
walther@60358
|
450 |
\<^rule_thm>\<open>mult_cross1\<close>, (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
|
walther@60358
|
451 |
\<^rule_thm>\<open>mult_cross2\<close> (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
|
walther@59878
|
452 |
scr = Rule.Empty_Prog})
|
neuper@52105
|
453 |
calculate_Poly);
|
neuper@37950
|
454 |
|
walther@60278
|
455 |
(*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
|
neuper@37950
|
456 |
fun eval_is_expanded (thmid:string) _
|
walther@60335
|
457 |
(t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) thy =
|
neuper@37950
|
458 |
if is_expanded arg
|
walther@59870
|
459 |
then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
|
wneuper@59390
|
460 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59870
|
461 |
else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
|
wneuper@59390
|
462 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
s1210629013@52159
|
463 |
| eval_is_expanded _ _ _ _ = NONE;
|
wneuper@59472
|
464 |
\<close>
|
wenzelm@60313
|
465 |
calculation is_expanded = \<open>eval_is_expanded ""\<close>
|
wneuper@59472
|
466 |
ML \<open>
|
neuper@37950
|
467 |
val rational_erls =
|
walther@59852
|
468 |
Rule_Set.merge "rational_erls" calculate_Rational
|
walther@60358
|
469 |
(Rule_Set.append_rules "is_expanded" Atools_erls [
|
walther@60358
|
470 |
\<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
|
wneuper@59472
|
471 |
\<close>
|
neuper@37950
|
472 |
|
wneuper@59472
|
473 |
subsection \<open>Embed cancellation into rewriting\<close>
|
wneuper@59472
|
474 |
ML \<open>
|
walther@59603
|
475 |
(**)local (* cancel_p *)
|
neuper@37950
|
476 |
|
walther@59852
|
477 |
val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
|
neuper@37950
|
478 |
|
neuper@52105
|
479 |
fun init_state thy eval_rls ro t =
|
neuper@52105
|
480 |
let
|
neuper@52105
|
481 |
val SOME (t', _) = factout_p_ thy t;
|
neuper@52105
|
482 |
val SOME (t'', asm) = cancel_p_ thy t;
|
walther@59907
|
483 |
val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
|
neuper@52105
|
484 |
val der = der @
|
wenzelm@60297
|
485 |
[(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
|
walther@60017
|
486 |
val rs = (Rule.distinct' o (map #1)) der
|
walther@60017
|
487 |
val rs = filter_out (ThmC.member'
|
neuper@52105
|
488 |
["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
|
neuper@52105
|
489 |
in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
|
neuper@37950
|
490 |
|
neuper@52105
|
491 |
fun locate_rule thy eval_rls ro [rs] t r =
|
walther@59876
|
492 |
if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
|
neuper@52105
|
493 |
then
|
walther@59876
|
494 |
let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
|
neuper@52105
|
495 |
in
|
neuper@52105
|
496 |
case ropt of SOME ta => [(r, ta)]
|
walther@59733
|
497 |
| NONE => ((*tracing
|
walther@59876
|
498 |
("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) [])
|
neuper@52105
|
499 |
end
|
walther@59876
|
500 |
else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
|
walther@59962
|
501 |
| locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
|
neuper@37950
|
502 |
|
neuper@52105
|
503 |
fun next_rule thy eval_rls ro [rs] t =
|
neuper@52105
|
504 |
let
|
walther@59907
|
505 |
val der = Derive.do_one thy eval_rls rs ro NONE t;
|
neuper@52105
|
506 |
in case der of (_, r, _) :: _ => SOME r | _ => NONE end
|
walther@59962
|
507 |
| next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
|
neuper@37950
|
508 |
|
wneuper@59416
|
509 |
fun attach_form (_: Rule.rule list list) (_: term) (_: term) =
|
wneuper@59416
|
510 |
[(*TODO*)]: ( Rule.rule * (term * term list)) list;
|
neuper@37950
|
511 |
|
walther@59861
|
512 |
(**)in(**)
|
neuper@37950
|
513 |
|
neuper@52105
|
514 |
val cancel_p =
|
walther@59850
|
515 |
Rule_Set.Rrls {id = "cancel_p", prepat = [],
|
wenzelm@60291
|
516 |
rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>),
|
neuper@52105
|
517 |
erls = rational_erls,
|
neuper@52105
|
518 |
calc =
|
wenzelm@60309
|
519 |
[("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
|
wenzelm@60309
|
520 |
("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
|
wenzelm@60309
|
521 |
("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
|
wenzelm@60309
|
522 |
("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
|
neuper@52105
|
523 |
errpatts = [],
|
neuper@52105
|
524 |
scr =
|
wenzelm@60291
|
525 |
Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
|
wenzelm@60291
|
526 |
normal_form = cancel_p_ \<^theory>,
|
wenzelm@60291
|
527 |
locate_rule = locate_rule \<^theory> Atools_erls ro,
|
wenzelm@60291
|
528 |
next_rule = next_rule \<^theory> Atools_erls ro,
|
neuper@52105
|
529 |
attach_form = attach_form}}
|
walther@59861
|
530 |
(**)end(* local cancel_p *)
|
wneuper@59472
|
531 |
\<close>
|
neuper@37950
|
532 |
|
wneuper@59472
|
533 |
subsection \<open>Embed addition into rewriting\<close>
|
wneuper@59472
|
534 |
ML \<open>
|
walther@59861
|
535 |
(**)local (* add_fractions_p *)
|
neuper@37950
|
536 |
|
walther@59852
|
537 |
(*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls "make_polynomial");*)
|
walther@59852
|
538 |
val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
|
neuper@37950
|
539 |
|
neuper@52105
|
540 |
fun init_state thy eval_rls ro t =
|
neuper@52105
|
541 |
let
|
walther@60358
|
542 |
val SOME (t', _) = common_nominator_p_ thy t;
|
neuper@52105
|
543 |
val SOME (t'', asm) = add_fraction_p_ thy t;
|
walther@59907
|
544 |
val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
|
neuper@52105
|
545 |
val der = der @
|
wenzelm@60297
|
546 |
[(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
|
walther@60017
|
547 |
val rs = (Rule.distinct' o (map #1)) der;
|
walther@60017
|
548 |
val rs = filter_out (ThmC.member'
|
neuper@52105
|
549 |
["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
|
neuper@52105
|
550 |
in (t, t'', [rs(*here only _ONE_*)], der) end;
|
neuper@37950
|
551 |
|
neuper@52105
|
552 |
fun locate_rule thy eval_rls ro [rs] t r =
|
walther@59876
|
553 |
if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
|
neuper@52105
|
554 |
then
|
walther@59876
|
555 |
let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
|
neuper@52105
|
556 |
in
|
neuper@52105
|
557 |
case ropt of
|
neuper@52105
|
558 |
SOME ta => [(r, ta)]
|
neuper@52105
|
559 |
| NONE =>
|
walther@59876
|
560 |
((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
|
neuper@52105
|
561 |
[]) end
|
walther@59876
|
562 |
else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
|
walther@59962
|
563 |
| locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
|
neuper@37950
|
564 |
|
neuper@37950
|
565 |
fun next_rule thy eval_rls ro [rs] t =
|
walther@59907
|
566 |
let val der = Derive.do_one thy eval_rls rs ro NONE t;
|
neuper@52105
|
567 |
in
|
neuper@52105
|
568 |
case der of
|
neuper@52105
|
569 |
(_,r,_)::_ => SOME r
|
neuper@52105
|
570 |
| _ => NONE
|
neuper@37950
|
571 |
end
|
walther@59962
|
572 |
| next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
|
neuper@37950
|
573 |
|
wenzelm@60291
|
574 |
val pat0 = TermC.parse_patt \<^theory> "?r/?s+?u/?v :: real";
|
wenzelm@60291
|
575 |
val pat1 = TermC.parse_patt \<^theory> "?r/?s+?u :: real";
|
wenzelm@60291
|
576 |
val pat2 = TermC.parse_patt \<^theory> "?r +?u/?v :: real";
|
neuper@48760
|
577 |
val prepat = [([@{term True}], pat0),
|
neuper@48760
|
578 |
([@{term True}], pat1),
|
neuper@48760
|
579 |
([@{term True}], pat2)];
|
walther@59861
|
580 |
(**)in(**)
|
neuper@37950
|
581 |
|
neuper@52105
|
582 |
val add_fractions_p =
|
walther@59850
|
583 |
Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
|
wenzelm@60291
|
584 |
rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
|
neuper@52105
|
585 |
erls = rational_erls,
|
wenzelm@60309
|
586 |
calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
|
wenzelm@60309
|
587 |
("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
|
wenzelm@60309
|
588 |
("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
|
wenzelm@60309
|
589 |
("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
|
neuper@52105
|
590 |
errpatts = [],
|
wenzelm@60291
|
591 |
scr = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
|
wenzelm@60291
|
592 |
normal_form = add_fraction_p_ \<^theory>,
|
wenzelm@60291
|
593 |
locate_rule = locate_rule \<^theory> Atools_erls ro,
|
wenzelm@60291
|
594 |
next_rule = next_rule \<^theory> Atools_erls ro,
|
neuper@52105
|
595 |
attach_form = attach_form}}
|
walther@59861
|
596 |
(**)end(*local add_fractions_p *)
|
wneuper@59472
|
597 |
\<close>
|
neuper@37950
|
598 |
|
wneuper@59472
|
599 |
subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>
|
wneuper@59472
|
600 |
ML \<open>
|
neuper@52105
|
601 |
(*copying cancel_p_rls + add her caused error in interface.sml*)
|
wneuper@59472
|
602 |
\<close>
|
neuper@42451
|
603 |
|
wneuper@59472
|
604 |
section \<open>Rulesets for general simplification\<close>
|
wneuper@59472
|
605 |
ML \<open>
|
neuper@37950
|
606 |
(*.all powers over + distributed; atoms over * collected, other distributed
|
neuper@37950
|
607 |
contains absolute minimum of thms for context in norm_Rational .*)
|
s1210629013@55444
|
608 |
val powers = prep_rls'(
|
walther@59857
|
609 |
Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@59851
|
610 |
erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
611 |
rules = [
|
walther@60358
|
612 |
\<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
|
walther@60358
|
613 |
\<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
|
walther@60358
|
614 |
\<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*)
|
walther@60358
|
615 |
\<^rule_thm>\<open>realpow_minus_even\<close>, (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
|
walther@60358
|
616 |
\<^rule_thm>\<open>realpow_minus_odd\<close>, (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
|
neuper@37950
|
617 |
|
walther@60358
|
618 |
(*----- collect atoms over * -----*)
|
walther@60358
|
619 |
\<^rule_thm>\<open>realpow_two_atom\<close>, (*"r is_atom ==> r * r = r \<up> 2"*)
|
walther@60358
|
620 |
\<^rule_thm>\<open>realpow_plus_1\<close>, (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
|
walther@60358
|
621 |
\<^rule_thm>\<open>realpow_addI_atom\<close>, (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
|
walther@60358
|
622 |
|
walther@60358
|
623 |
(*----- distribute none-atoms -----*)
|
walther@60358
|
624 |
\<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
|
walther@60358
|
625 |
\<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*)
|
walther@60358
|
626 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
|
walther@60358
|
627 |
scr = Rule.Empty_Prog});
|
walther@60358
|
628 |
|
neuper@37950
|
629 |
(*.contains absolute minimum of thms for context in norm_Rational.*)
|
s1210629013@55444
|
630 |
val rat_mult_divide = prep_rls'(
|
walther@59851
|
631 |
Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
|
walther@59857
|
632 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59852
|
633 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
634 |
rules = [
|
walther@60358
|
635 |
\<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
|
walther@60358
|
636 |
\<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
|
walther@60358
|
637 |
otherwise inv.to a / b / c = ...*)
|
walther@60358
|
638 |
\<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
|
walther@60358
|
639 |
and does not commute a / b * c \<up> 2 !*)
|
neuper@37950
|
640 |
|
walther@60358
|
641 |
\<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
|
walther@60358
|
642 |
\<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
|
walther@60358
|
643 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
|
walther@60358
|
644 |
scr = Rule.Empty_Prog});
|
neuper@37979
|
645 |
|
neuper@37950
|
646 |
(*.contains absolute minimum of thms for context in norm_Rational.*)
|
s1210629013@55444
|
647 |
val reduce_0_1_2 = prep_rls'(
|
walther@59857
|
648 |
Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@60358
|
649 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
650 |
rules = [
|
walther@60358
|
651 |
(*\<^rule_thm>\<open>divide_1\<close>, "?x / 1 = ?x" unnecessary.for normalform*)
|
walther@60358
|
652 |
\<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
|
walther@60358
|
653 |
(*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
|
walther@60358
|
654 |
(*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, "- ?x * - ?y = ?x * ?y"*)
|
walther@60358
|
655 |
|
walther@60358
|
656 |
|
walther@60358
|
657 |
\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
|
walther@60358
|
658 |
\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
|
walther@60358
|
659 |
(*\<^rule_thm>\<open>right_minus\<close>, "?z + - ?z = 0"*)
|
walther@60358
|
660 |
|
walther@60358
|
661 |
\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
|
walther@60358
|
662 |
\<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
|
walther@60358
|
663 |
|
walther@60358
|
664 |
\<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
|
walther@60358
|
665 |
scr = Rule.Empty_Prog});
|
neuper@37950
|
666 |
|
neuper@37950
|
667 |
(*erls for calculate_Rational;
|
neuper@37950
|
668 |
make local with FIXX@ME result:term *term list WN0609???SKMG*)
|
s1210629013@55444
|
669 |
val norm_rat_erls = prep_rls'(
|
walther@59857
|
670 |
Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@60358
|
671 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
672 |
rules = [
|
walther@60358
|
673 |
\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
|
walther@60358
|
674 |
scr = Rule.Empty_Prog});
|
neuper@37979
|
675 |
|
neuper@52105
|
676 |
(* consists of rls containing the absolute minimum of thms *)
|
walther@60358
|
677 |
(*
|
walther@60358
|
678 |
which is now replaced by MGs version "norm_Rational" below
|
walther@60358
|
679 |
*)
|
s1210629013@55444
|
680 |
val norm_Rational_min = prep_rls'(
|
walther@59857
|
681 |
Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@60358
|
682 |
erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
683 |
rules = [(*sequence given by operator precedence*)
|
walther@60358
|
684 |
Rule.Rls_ discard_minus,
|
walther@60358
|
685 |
Rule.Rls_ powers,
|
walther@60358
|
686 |
Rule.Rls_ rat_mult_divide,
|
walther@60358
|
687 |
Rule.Rls_ expand,
|
walther@60358
|
688 |
Rule.Rls_ reduce_0_1_2,
|
walther@60358
|
689 |
Rule.Rls_ order_add_mult,
|
walther@60358
|
690 |
Rule.Rls_ collect_numerals,
|
walther@60358
|
691 |
Rule.Rls_ add_fractions_p,
|
walther@60358
|
692 |
Rule.Rls_ cancel_p
|
walther@60358
|
693 |
],
|
walther@60358
|
694 |
scr = Rule.Empty_Prog});
|
neuper@37979
|
695 |
|
s1210629013@55444
|
696 |
val norm_Rational_parenthesized = prep_rls'(
|
walther@59878
|
697 |
Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
|
walther@60358
|
698 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@60358
|
699 |
erls = Atools_erls, srls = Rule_Set.Empty,
|
walther@60358
|
700 |
calc = [], errpatts = [],
|
walther@60358
|
701 |
rules = [
|
walther@60358
|
702 |
Rule.Rls_ norm_Rational_min,
|
walther@60358
|
703 |
Rule.Rls_ discard_parentheses],
|
walther@60358
|
704 |
scr = Rule.Empty_Prog});
|
neuper@37950
|
705 |
|
neuper@37950
|
706 |
(*WN030318???SK: simplifies all but cancel and common_nominator*)
|
neuper@37950
|
707 |
val simplify_rational =
|
walther@60358
|
708 |
Rule_Set.merge "simplify_rational" expand_binoms
|
walther@60358
|
709 |
(Rule_Set.append_rules "divide" calculate_Rational [
|
walther@60358
|
710 |
\<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
|
walther@60358
|
711 |
\<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
|
walther@60358
|
712 |
\<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
|
walther@60358
|
713 |
otherwise inv.to a / b / c = ...*)
|
walther@60358
|
714 |
\<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b"*)
|
walther@60358
|
715 |
\<^rule_thm>\<open>add_minus\<close>, (*"?a + ?b - ?b = ?a"*)
|
walther@60358
|
716 |
\<^rule_thm>\<open>add_minus1\<close>, (*"?a - ?b + ?b = ?a"*)
|
walther@60358
|
717 |
\<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]);
|
walther@60358
|
718 |
|
s1210629013@55444
|
719 |
val add_fractions_p_rls = prep_rls'(
|
walther@59857
|
720 |
Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59852
|
721 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
wneuper@59416
|
722 |
rules = [Rule.Rls_ add_fractions_p],
|
walther@59878
|
723 |
scr = Rule.Empty_Prog});
|
neuper@37950
|
724 |
|
walther@59851
|
725 |
(* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
|
s1210629013@55444
|
726 |
val cancel_p_rls = prep_rls'(
|
walther@59851
|
727 |
Rule_Def.Repeat
|
walther@59857
|
728 |
{id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59852
|
729 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
wneuper@59416
|
730 |
rules = [Rule.Rls_ cancel_p],
|
walther@59878
|
731 |
scr = Rule.Empty_Prog});
|
neuper@52105
|
732 |
|
neuper@37950
|
733 |
(*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
|
neuper@37950
|
734 |
used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
|
s1210629013@55444
|
735 |
val rat_mult_poly = prep_rls'(
|
walther@59857
|
736 |
Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@60358
|
737 |
erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [
|
walther@60358
|
738 |
\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
|
walther@59851
|
739 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
740 |
rules = [
|
walther@60358
|
741 |
\<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
|
walther@60358
|
742 |
\<^rule_thm>\<open>rat_mult_poly_r\<close> (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)],
|
walther@59878
|
743 |
scr = Rule.Empty_Prog});
|
neuper@37979
|
744 |
|
neuper@37950
|
745 |
(*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
|
neuper@37950
|
746 |
used in looping part norm_Rational_rls, see example DA-M02-main.p.60
|
walther@59852
|
747 |
.. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule_Set.empty,
|
wneuper@59416
|
748 |
I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
|
neuper@37950
|
749 |
... WN0609???MG.*)
|
s1210629013@55444
|
750 |
val rat_mult_div_pow = prep_rls'(
|
walther@59857
|
751 |
Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@59852
|
752 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
753 |
rules = [
|
walther@60358
|
754 |
\<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
|
walther@60358
|
755 |
\<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
|
walther@60358
|
756 |
\<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
|
neuper@52105
|
757 |
|
walther@60358
|
758 |
\<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
|
walther@60358
|
759 |
\<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
|
walther@60358
|
760 |
\<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
|
wenzelm@60294
|
761 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
neuper@52105
|
762 |
|
walther@60358
|
763 |
\<^rule_thm>\<open>rat_power\<close> (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)],
|
walther@59878
|
764 |
scr = Rule.Empty_Prog});
|
neuper@37950
|
765 |
|
s1210629013@55444
|
766 |
val rat_reduce_1 = prep_rls'(
|
walther@59857
|
767 |
Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59852
|
768 |
erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
769 |
rules = [
|
walther@60358
|
770 |
\<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
|
walther@60358
|
771 |
\<^rule_thm>\<open>mult_1_left\<close> (*"1 * z = z"*)],
|
walther@59878
|
772 |
scr = Rule.Empty_Prog});
|
neuper@52105
|
773 |
|
neuper@52105
|
774 |
(* looping part of norm_Rational *)
|
s1210629013@55444
|
775 |
val norm_Rational_rls = prep_rls' (
|
walther@59857
|
776 |
Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@59851
|
777 |
erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
778 |
rules = [
|
walther@60358
|
779 |
Rule.Rls_ add_fractions_p_rls,
|
wneuper@59416
|
780 |
Rule.Rls_ rat_mult_div_pow,
|
wneuper@59416
|
781 |
Rule.Rls_ make_rat_poly_with_parentheses,
|
wneuper@59416
|
782 |
Rule.Rls_ cancel_p_rls,
|
walther@60358
|
783 |
Rule.Rls_ rat_reduce_1],
|
walther@59878
|
784 |
scr = Rule.Empty_Prog});
|
neuper@52105
|
785 |
|
s1210629013@55444
|
786 |
val norm_Rational = prep_rls' (
|
walther@59878
|
787 |
Rule_Set.Sequence
|
walther@59857
|
788 |
{id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59851
|
789 |
erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
790 |
rules = [
|
walther@60358
|
791 |
Rule.Rls_ discard_minus,
|
wneuper@59416
|
792 |
Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
|
wneuper@59416
|
793 |
Rule.Rls_ make_rat_poly_with_parentheses,
|
wneuper@59416
|
794 |
Rule.Rls_ cancel_p_rls,
|
wneuper@59416
|
795 |
Rule.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
|
walther@60358
|
796 |
Rule.Rls_ discard_parentheses1], (* mult only *)
|
walther@59878
|
797 |
scr = Rule.Empty_Prog});
|
wneuper@59472
|
798 |
\<close>
|
neuper@52125
|
799 |
|
wenzelm@60289
|
800 |
rule_set_knowledge
|
wenzelm@60286
|
801 |
calculate_Rational = calculate_Rational and
|
wenzelm@60286
|
802 |
calc_rat_erls = calc_rat_erls and
|
wenzelm@60286
|
803 |
rational_erls = rational_erls and
|
wenzelm@60286
|
804 |
cancel_p = cancel_p and
|
wenzelm@60286
|
805 |
add_fractions_p = add_fractions_p and
|
wenzelm@60286
|
806 |
|
wenzelm@60286
|
807 |
add_fractions_p_rls = add_fractions_p_rls and
|
wenzelm@60286
|
808 |
powers_erls = powers_erls and
|
wenzelm@60286
|
809 |
powers = powers and
|
wenzelm@60286
|
810 |
rat_mult_divide = rat_mult_divide and
|
wenzelm@60286
|
811 |
reduce_0_1_2 = reduce_0_1_2 and
|
wenzelm@60286
|
812 |
|
wenzelm@60286
|
813 |
rat_reduce_1 = rat_reduce_1 and
|
wenzelm@60286
|
814 |
norm_rat_erls = norm_rat_erls and
|
wenzelm@60286
|
815 |
norm_Rational = norm_Rational and
|
wenzelm@60286
|
816 |
norm_Rational_rls = norm_Rational_rls and
|
wenzelm@60286
|
817 |
norm_Rational_min = norm_Rational_min and
|
wenzelm@60286
|
818 |
norm_Rational_parenthesized = norm_Rational_parenthesized and
|
wenzelm@60286
|
819 |
|
wenzelm@60286
|
820 |
rat_mult_poly = rat_mult_poly and
|
wenzelm@60286
|
821 |
rat_mult_div_pow = rat_mult_div_pow and
|
wenzelm@60286
|
822 |
cancel_p_rls = cancel_p_rls
|
neuper@37950
|
823 |
|
wneuper@59472
|
824 |
section \<open>A problem for simplification of rationals\<close>
|
wenzelm@60306
|
825 |
|
wenzelm@60306
|
826 |
problem pbl_simp_rat : "rational/simplification" =
|
wenzelm@60306
|
827 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
|
wenzelm@60306
|
828 |
Method: "simplification/of_rationals"
|
wenzelm@60306
|
829 |
CAS: "Simplify t_t"
|
wenzelm@60306
|
830 |
Given: "Term t_t"
|
wenzelm@60306
|
831 |
Where: "t_t is_ratpolyexp"
|
wenzelm@60306
|
832 |
Find: "normalform n_n"
|
neuper@37950
|
833 |
|
wneuper@59472
|
834 |
section \<open>A methods for simplification of rationals\<close>
|
s1210629013@55373
|
835 |
(*WN061025 this methods script is copied from (auto-generated) script
|
s1210629013@55373
|
836 |
of norm_Rational in order to ease repair on inform*)
|
wneuper@59545
|
837 |
|
wneuper@59504
|
838 |
partial_function (tailrec) simplify :: "real \<Rightarrow> real"
|
wneuper@59504
|
839 |
where
|
walther@59716
|
840 |
"simplify term = (
|
walther@59637
|
841 |
(Try (Rewrite_Set ''discard_minus'') #>
|
walther@59637
|
842 |
Try (Rewrite_Set ''rat_mult_poly'') #>
|
walther@59637
|
843 |
Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
|
walther@59637
|
844 |
Try (Rewrite_Set ''cancel_p_rls'') #>
|
walther@59635
|
845 |
(Repeat (
|
walther@59637
|
846 |
Try (Rewrite_Set ''add_fractions_p_rls'') #>
|
walther@59637
|
847 |
Try (Rewrite_Set ''rat_mult_div_pow'') #>
|
walther@59637
|
848 |
Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
|
walther@59637
|
849 |
Try (Rewrite_Set ''cancel_p_rls'') #>
|
walther@59637
|
850 |
Try (Rewrite_Set ''rat_reduce_1''))) #>
|
walther@59635
|
851 |
Try (Rewrite_Set ''discard_parentheses1''))
|
walther@59716
|
852 |
term)"
|
wenzelm@60303
|
853 |
|
wenzelm@60303
|
854 |
|
wenzelm@60303
|
855 |
method met_simp_rat : "simplification/of_rationals" =
|
wenzelm@60303
|
856 |
\<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
|
wenzelm@60303
|
857 |
prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
|
wenzelm@60303
|
858 |
[(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
|
wenzelm@60303
|
859 |
crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}\<close>
|
wenzelm@60303
|
860 |
Program: simplify.simps
|
wenzelm@60303
|
861 |
Given: "Term t_t"
|
wenzelm@60303
|
862 |
Where: "t_t is_ratpolyexp"
|
wenzelm@60303
|
863 |
Find: "normalform n_n"
|
wenzelm@60303
|
864 |
ML \<open>
|
walther@60278
|
865 |
\<close> ML \<open>
|
wneuper@59472
|
866 |
\<close>
|
neuper@52105
|
867 |
end
|