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