|
1 (* Title: HOL/Decision_Procs/Reflective_Field.thy |
|
2 Author: Stefan Berghofer |
|
3 |
|
4 Reducing equalities in fields to equalities in rings. |
|
5 *) |
|
6 |
|
7 theory Reflective_Field |
|
8 imports Commutative_Ring |
|
9 begin |
|
10 |
|
11 datatype fexpr = |
|
12 FCnst int |
|
13 | FVar nat |
|
14 | FAdd fexpr fexpr |
|
15 | FSub fexpr fexpr |
|
16 | FMul fexpr fexpr |
|
17 | FNeg fexpr |
|
18 | FDiv fexpr fexpr |
|
19 | FPow fexpr nat |
|
20 |
|
21 fun (in field) nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where |
|
22 "nth_el [] n = \<zero>" |
|
23 | "nth_el (x # xs) 0 = x" |
|
24 | "nth_el (x # xs) (Suc n) = nth_el xs n" |
|
25 |
|
26 lemma (in field) nth_el_Cons: |
|
27 "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))" |
|
28 by (cases n) simp_all |
|
29 |
|
30 lemma (in field) nth_el_closed [simp]: |
|
31 "in_carrier xs \<Longrightarrow> nth_el xs n \<in> carrier R" |
|
32 by (induct xs n rule: nth_el.induct) (simp_all add: in_carrier_def) |
|
33 |
|
34 primrec (in field) feval :: "'a list \<Rightarrow> fexpr \<Rightarrow> 'a" |
|
35 where |
|
36 "feval xs (FCnst c) = \<guillemotleft>c\<guillemotright>" |
|
37 | "feval xs (FVar n) = nth_el xs n" |
|
38 | "feval xs (FAdd a b) = feval xs a \<oplus> feval xs b" |
|
39 | "feval xs (FSub a b) = feval xs a \<ominus> feval xs b" |
|
40 | "feval xs (FMul a b) = feval xs a \<otimes> feval xs b" |
|
41 | "feval xs (FNeg a) = \<ominus> feval xs a" |
|
42 | "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b" |
|
43 | "feval xs (FPow a n) = feval xs a (^) n" |
|
44 |
|
45 lemma (in field) feval_Cnst: |
|
46 "feval xs (FCnst 0) = \<zero>" |
|
47 "feval xs (FCnst 1) = \<one>" |
|
48 "feval xs (FCnst (numeral n)) = \<guillemotleft>numeral n\<guillemotright>" |
|
49 by simp_all |
|
50 |
|
51 datatype pexpr = |
|
52 PExpr1 pexpr1 |
|
53 | PExpr2 pexpr2 |
|
54 and pexpr1 = |
|
55 PCnst int |
|
56 | PVar nat |
|
57 | PAdd pexpr pexpr |
|
58 | PSub pexpr pexpr |
|
59 | PNeg pexpr |
|
60 and pexpr2 = |
|
61 PMul pexpr pexpr |
|
62 | PPow pexpr nat |
|
63 |
|
64 lemma pexpr_cases [case_names PCnst PVar PAdd PSub PNeg PMul PPow]: |
|
65 assumes |
|
66 "\<And>c. e = PExpr1 (PCnst c) \<Longrightarrow> P" |
|
67 "\<And>n. e = PExpr1 (PVar n) \<Longrightarrow> P" |
|
68 "\<And>e1 e2. e = PExpr1 (PAdd e1 e2) \<Longrightarrow> P" |
|
69 "\<And>e1 e2. e = PExpr1 (PSub e1 e2) \<Longrightarrow> P" |
|
70 "\<And>e'. e = PExpr1 (PNeg e') \<Longrightarrow> P" |
|
71 "\<And>e1 e2. e = PExpr2 (PMul e1 e2) \<Longrightarrow> P" |
|
72 "\<And>e' n. e = PExpr2 (PPow e' n) \<Longrightarrow> P" |
|
73 shows P |
|
74 proof (cases e) |
|
75 case (PExpr1 e') |
|
76 then show ?thesis |
|
77 apply (cases e') |
|
78 apply simp_all |
|
79 apply (erule assms)+ |
|
80 done |
|
81 next |
|
82 case (PExpr2 e') |
|
83 then show ?thesis |
|
84 apply (cases e') |
|
85 apply simp_all |
|
86 apply (erule assms)+ |
|
87 done |
|
88 qed |
|
89 |
|
90 lemmas pexpr_cases2 = pexpr_cases [case_product pexpr_cases] |
|
91 |
|
92 fun (in field) peval :: "'a list \<Rightarrow> pexpr \<Rightarrow> 'a" |
|
93 where |
|
94 "peval xs (PExpr1 (PCnst c)) = \<guillemotleft>c\<guillemotright>" |
|
95 | "peval xs (PExpr1 (PVar n)) = nth_el xs n" |
|
96 | "peval xs (PExpr1 (PAdd a b)) = peval xs a \<oplus> peval xs b" |
|
97 | "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b" |
|
98 | "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a" |
|
99 | "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b" |
|
100 | "peval xs (PExpr2 (PPow a n)) = peval xs a (^) n" |
|
101 |
|
102 lemma (in field) peval_Cnst: |
|
103 "peval xs (PExpr1 (PCnst 0)) = \<zero>" |
|
104 "peval xs (PExpr1 (PCnst 1)) = \<one>" |
|
105 "peval xs (PExpr1 (PCnst (numeral n))) = \<guillemotleft>numeral n\<guillemotright>" |
|
106 "peval xs (PExpr1 (PCnst (- numeral n))) = \<ominus> \<guillemotleft>numeral n\<guillemotright>" |
|
107 by simp_all |
|
108 |
|
109 lemma (in field) peval_closed [simp]: |
|
110 "in_carrier xs \<Longrightarrow> peval xs e \<in> carrier R" |
|
111 "in_carrier xs \<Longrightarrow> peval xs (PExpr1 e1) \<in> carrier R" |
|
112 "in_carrier xs \<Longrightarrow> peval xs (PExpr2 e2) \<in> carrier R" |
|
113 by (induct e and e1 and e2) simp_all |
|
114 |
|
115 definition npepow :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr" |
|
116 where |
|
117 "npepow e n = |
|
118 (if n = 0 then PExpr1 (PCnst 1) |
|
119 else if n = 1 then e |
|
120 else (case e of |
|
121 PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c ^ n)) |
|
122 | _ \<Rightarrow> PExpr2 (PPow e n)))" |
|
123 |
|
124 lemma (in field) npepow_correct: |
|
125 "in_carrier xs \<Longrightarrow> peval xs (npepow e n) = peval xs (PExpr2 (PPow e n))" |
|
126 by (cases e rule: pexpr_cases) |
|
127 (simp_all add: npepow_def) |
|
128 |
|
129 fun npemul :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" |
|
130 where |
|
131 "npemul x y = (case x of |
|
132 PExpr1 (PCnst c) \<Rightarrow> |
|
133 if c = 0 then x |
|
134 else if c = 1 then y else |
|
135 (case y of |
|
136 PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c * d)) |
|
137 | _ \<Rightarrow> PExpr2 (PMul x y)) |
|
138 | PExpr2 (PPow e1 n) \<Rightarrow> |
|
139 (case y of |
|
140 PExpr2 (PPow e2 m) \<Rightarrow> |
|
141 if n = m then npepow (npemul e1 e2) n |
|
142 else PExpr2 (PMul x y) |
|
143 | PExpr1 (PCnst d) \<Rightarrow> |
|
144 if d = 0 then y |
|
145 else if d = 1 then x |
|
146 else PExpr2 (PMul x y) |
|
147 | _ \<Rightarrow> PExpr2 (PMul x y)) |
|
148 | _ \<Rightarrow> (case y of |
|
149 PExpr1 (PCnst d) \<Rightarrow> |
|
150 if d = 0 then y |
|
151 else if d = 1 then x |
|
152 else PExpr2 (PMul x y) |
|
153 | _ \<Rightarrow> PExpr2 (PMul x y)))" |
|
154 |
|
155 lemma (in field) npemul_correct: |
|
156 "in_carrier xs \<Longrightarrow> peval xs (npemul e1 e2) = peval xs (PExpr2 (PMul e1 e2))" |
|
157 proof (induct e1 e2 rule: npemul.induct) |
|
158 case (1 x y) |
|
159 then show ?case |
|
160 proof (cases x y rule: pexpr_cases2) |
|
161 case (PPow_PPow e n e' m) |
|
162 then show ?thesis |
|
163 by (simp add: 1 npepow_correct nat_pow_distr |
|
164 npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"] |
|
165 del: npemul.simps) |
|
166 qed simp_all |
|
167 qed |
|
168 |
|
169 declare npemul.simps [simp del] |
|
170 |
|
171 definition npeadd :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" |
|
172 where |
|
173 "npeadd x y = (case x of |
|
174 PExpr1 (PCnst c) \<Rightarrow> |
|
175 if c = 0 then y else |
|
176 (case y of |
|
177 PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c + d)) |
|
178 | _ \<Rightarrow> PExpr1 (PAdd x y)) |
|
179 | _ \<Rightarrow> (case y of |
|
180 PExpr1 (PCnst d) \<Rightarrow> |
|
181 if d = 0 then x |
|
182 else PExpr1 (PAdd x y) |
|
183 | _ \<Rightarrow> PExpr1 (PAdd x y)))" |
|
184 |
|
185 lemma (in field) npeadd_correct: |
|
186 "in_carrier xs \<Longrightarrow> peval xs (npeadd e1 e2) = peval xs (PExpr1 (PAdd e1 e2))" |
|
187 by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npeadd_def) |
|
188 |
|
189 definition npesub :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" |
|
190 where |
|
191 "npesub x y = (case y of |
|
192 PExpr1 (PCnst d) \<Rightarrow> |
|
193 if d = 0 then x else |
|
194 (case x of |
|
195 PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c - d)) |
|
196 | _ \<Rightarrow> PExpr1 (PSub x y)) |
|
197 | _ \<Rightarrow> (case x of |
|
198 PExpr1 (PCnst c) \<Rightarrow> |
|
199 if c = 0 then PExpr1 (PNeg y) |
|
200 else PExpr1 (PSub x y) |
|
201 | _ \<Rightarrow> PExpr1 (PSub x y)))" |
|
202 |
|
203 lemma (in field) npesub_correct: |
|
204 "in_carrier xs \<Longrightarrow> peval xs (npesub e1 e2) = peval xs (PExpr1 (PSub e1 e2))" |
|
205 by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npesub_def) |
|
206 |
|
207 definition npeneg :: "pexpr \<Rightarrow> pexpr" |
|
208 where |
|
209 "npeneg e = (case e of |
|
210 PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (- c)) |
|
211 | _ \<Rightarrow> PExpr1 (PNeg e))" |
|
212 |
|
213 lemma (in field) npeneg_correct: |
|
214 "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))" |
|
215 by (cases e rule: pexpr_cases) (simp_all add: npeneg_def) |
|
216 |
|
217 lemma option_pair_cases [case_names None Some]: |
|
218 assumes |
|
219 "x = None \<Longrightarrow> P" |
|
220 "\<And>p q. x = Some (p, q) \<Longrightarrow> P" |
|
221 shows P |
|
222 proof (cases x) |
|
223 case None |
|
224 then show ?thesis by (rule assms) |
|
225 next |
|
226 case (Some r) |
|
227 then show ?thesis |
|
228 apply (cases r) |
|
229 apply simp |
|
230 by (rule assms) |
|
231 qed |
|
232 |
|
233 fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat * pexpr) option" |
|
234 where |
|
235 "isin e n (PExpr2 (PMul e1 e2)) m = |
|
236 (case isin e n e1 m of |
|
237 Some (k, e3) \<Rightarrow> |
|
238 if k = 0 then Some (0, npemul e3 (npepow e2 m)) |
|
239 else (case isin e k e2 m of |
|
240 Some (l, e4) \<Rightarrow> Some (l, npemul e3 e4) |
|
241 | None \<Rightarrow> Some (k, npemul e3 (npepow e2 m))) |
|
242 | None \<Rightarrow> (case isin e n e2 m of |
|
243 Some (k, e3) \<Rightarrow> Some (k, npemul (npepow e1 m) e3) |
|
244 | None \<Rightarrow> None))" |
|
245 | "isin e n (PExpr2 (PPow e' k)) m = |
|
246 (if k = 0 then None else isin e n e' (k * m))" |
|
247 | "isin (PExpr1 e) n (PExpr1 e') m = |
|
248 (if e = e' then |
|
249 if n >= m then Some (n - m, PExpr1 (PCnst 1)) |
|
250 else Some (0, npepow (PExpr1 e) (m - n)) |
|
251 else None)" |
|
252 | "isin (PExpr2 e) n (PExpr1 e') m = None" |
|
253 |
|
254 lemma (in field) isin_correct: |
|
255 assumes "in_carrier xs" |
|
256 and "isin e n e' m = Some (p, e'')" |
|
257 shows |
|
258 "peval xs (PExpr2 (PPow e' m)) = |
|
259 peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))" |
|
260 "p \<le> n" |
|
261 using assms |
|
262 by (induct e n e' m arbitrary: p e'' rule: isin.induct) |
|
263 (force |
|
264 simp add: |
|
265 nat_pow_distr nat_pow_pow nat_pow_mult m_ac |
|
266 npemul_correct npepow_correct |
|
267 split: option.split_asm prod.split_asm if_split_asm)+ |
|
268 |
|
269 lemma (in field) isin_correct': |
|
270 "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> |
|
271 peval xs e' = peval xs e (^) (n - p) \<otimes> peval xs e''" |
|
272 "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> p \<le> n" |
|
273 using isin_correct [where m=1] |
|
274 by simp_all |
|
275 |
|
276 fun split_aux :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr" |
|
277 where |
|
278 "split_aux (PExpr2 (PMul e1 e2)) n e = |
|
279 (let |
|
280 (left1, common1, right1) = split_aux e1 n e; |
|
281 (left2, common2, right2) = split_aux e2 n right1 |
|
282 in (npemul left1 left2, npemul common1 common2, right2))" |
|
283 | "split_aux (PExpr2 (PPow e' m)) n e = |
|
284 (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e) |
|
285 else split_aux e' (m * n) e)" |
|
286 | "split_aux (PExpr1 e') n e = |
|
287 (case isin (PExpr1 e') n e 1 of |
|
288 Some (m, e'') \<Rightarrow> |
|
289 (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'') |
|
290 else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e'')) |
|
291 | None \<Rightarrow> (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))" |
|
292 |
|
293 hide_const Left Right |
|
294 |
|
295 abbreviation Left :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where |
|
296 "Left e1 e2 \<equiv> fst (split_aux e1 (Suc 0) e2)" |
|
297 |
|
298 abbreviation Common :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where |
|
299 "Common e1 e2 \<equiv> fst (snd (split_aux e1 (Suc 0) e2))" |
|
300 |
|
301 abbreviation Right :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where |
|
302 "Right e1 e2 \<equiv> snd (snd (split_aux e1 (Suc 0) e2))" |
|
303 |
|
304 lemma split_aux_induct [case_names 1 2 3]: |
|
305 assumes I1: "\<And>e1 e2 n e. P e1 n e \<Longrightarrow> P e2 n (snd (snd (split_aux e1 n e))) \<Longrightarrow> |
|
306 P (PExpr2 (PMul e1 e2)) n e" |
|
307 and I2: "\<And>e' m n e. (m \<noteq> 0 \<Longrightarrow> P e' (m * n) e) \<Longrightarrow> P (PExpr2 (PPow e' m)) n e" |
|
308 and I3: "\<And>e' n e. P (PExpr1 e') n e" |
|
309 shows "P x y z" |
|
310 proof (induct x y z rule: split_aux.induct) |
|
311 case 1 |
|
312 from 1(1) 1(2) [OF refl prod.collapse prod.collapse] |
|
313 show ?case by (rule I1) |
|
314 next |
|
315 case 2 |
|
316 then show ?case by (rule I2) |
|
317 next |
|
318 case 3 |
|
319 then show ?case by (rule I3) |
|
320 qed |
|
321 |
|
322 lemma (in field) split_aux_correct: |
|
323 "in_carrier xs \<Longrightarrow> |
|
324 peval xs (PExpr2 (PPow e\<^sub>1 n)) = |
|
325 peval xs (PExpr2 (PMul (fst (split_aux e\<^sub>1 n e\<^sub>2)) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))" |
|
326 "in_carrier xs \<Longrightarrow> |
|
327 peval xs e\<^sub>2 = |
|
328 peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))" |
|
329 by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct) |
|
330 (auto simp add: split_beta |
|
331 nat_pow_distr nat_pow_pow nat_pow_mult m_ac |
|
332 npemul_correct npepow_correct isin_correct' |
|
333 split: option.split) |
|
334 |
|
335 lemma (in field) split_aux_correct': |
|
336 "in_carrier xs \<Longrightarrow> |
|
337 peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)" |
|
338 "in_carrier xs \<Longrightarrow> |
|
339 peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)" |
|
340 using split_aux_correct [where n=1] |
|
341 by simp_all |
|
342 |
|
343 fun fnorm :: "fexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list" |
|
344 where |
|
345 "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])" |
|
346 | "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])" |
|
347 | "fnorm (FAdd e1 e2) = |
|
348 (let |
|
349 (xn, xd, xc) = fnorm e1; |
|
350 (yn, yd, yc) = fnorm e2; |
|
351 (left, common, right) = split_aux xd 1 yd |
|
352 in |
|
353 (npeadd (npemul xn right) (npemul yn left), |
|
354 npemul left (npemul right common), |
|
355 List.union xc yc))" |
|
356 | "fnorm (FSub e1 e2) = |
|
357 (let |
|
358 (xn, xd, xc) = fnorm e1; |
|
359 (yn, yd, yc) = fnorm e2; |
|
360 (left, common, right) = split_aux xd 1 yd |
|
361 in |
|
362 (npesub (npemul xn right) (npemul yn left), |
|
363 npemul left (npemul right common), |
|
364 List.union xc yc))" |
|
365 | "fnorm (FMul e1 e2) = |
|
366 (let |
|
367 (xn, xd, xc) = fnorm e1; |
|
368 (yn, yd, yc) = fnorm e2; |
|
369 (left1, common1, right1) = split_aux xn 1 yd; |
|
370 (left2, common2, right2) = split_aux yn 1 xd |
|
371 in |
|
372 (npemul left1 left2, |
|
373 npemul right2 right1, |
|
374 List.union xc yc))" |
|
375 | "fnorm (FNeg e) = |
|
376 (let (n, d, c) = fnorm e |
|
377 in (npeneg n, d, c))" |
|
378 | "fnorm (FDiv e1 e2) = |
|
379 (let |
|
380 (xn, xd, xc) = fnorm e1; |
|
381 (yn, yd, yc) = fnorm e2; |
|
382 (left1, common1, right1) = split_aux xn 1 yn; |
|
383 (left2, common2, right2) = split_aux xd 1 yd |
|
384 in |
|
385 (npemul left1 right2, |
|
386 npemul left2 right1, |
|
387 List.insert yn (List.union xc yc)))" |
|
388 | "fnorm (FPow e m) = |
|
389 (let (n, d, c) = fnorm e |
|
390 in (npepow n m, npepow d m, c))" |
|
391 |
|
392 abbreviation Num :: "fexpr \<Rightarrow> pexpr" where |
|
393 "Num e \<equiv> fst (fnorm e)" |
|
394 |
|
395 abbreviation Denom :: "fexpr \<Rightarrow> pexpr" where |
|
396 "Denom e \<equiv> fst (snd (fnorm e))" |
|
397 |
|
398 abbreviation Cond :: "fexpr \<Rightarrow> pexpr list" where |
|
399 "Cond e \<equiv> snd (snd (fnorm e))" |
|
400 |
|
401 primrec (in field) nonzero :: "'a list \<Rightarrow> pexpr list \<Rightarrow> bool" |
|
402 where |
|
403 "nonzero xs [] = True" |
|
404 | "nonzero xs (p # ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)" |
|
405 |
|
406 lemma (in field) nonzero_singleton: |
|
407 "nonzero xs [p] = (peval xs p \<noteq> \<zero>)" |
|
408 by simp |
|
409 |
|
410 lemma (in field) nonzero_append: |
|
411 "nonzero xs (ps @ qs) = (nonzero xs ps \<and> nonzero xs qs)" |
|
412 by (induct ps) simp_all |
|
413 |
|
414 lemma (in field) nonzero_idempotent: |
|
415 "p \<in> set ps \<Longrightarrow> (peval xs p \<noteq> \<zero> \<and> nonzero xs ps) = nonzero xs ps" |
|
416 by (induct ps) auto |
|
417 |
|
418 lemma (in field) nonzero_insert: |
|
419 "nonzero xs (List.insert p ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)" |
|
420 by (simp add: List.insert_def nonzero_idempotent) |
|
421 |
|
422 lemma (in field) nonzero_union: |
|
423 "nonzero xs (List.union ps qs) = (nonzero xs ps \<and> nonzero xs qs)" |
|
424 by (induct ps rule: rev_induct) |
|
425 (auto simp add: List.union_def nonzero_insert nonzero_append) |
|
426 |
|
427 lemma (in field) fnorm_correct: |
|
428 assumes "in_carrier xs" |
|
429 and "nonzero xs (Cond e)" |
|
430 shows "feval xs e = peval xs (Num e) \<oslash> peval xs (Denom e)" |
|
431 and "peval xs (Denom e) \<noteq> \<zero>" |
|
432 using assms |
|
433 proof (induct e) |
|
434 case (FCnst c) { |
|
435 case 1 |
|
436 show ?case by simp |
|
437 next |
|
438 case 2 |
|
439 show ?case by simp |
|
440 } |
|
441 next |
|
442 case (FVar n) { |
|
443 case 1 |
|
444 then show ?case by simp |
|
445 next |
|
446 case 2 |
|
447 show ?case by simp |
|
448 } |
|
449 next |
|
450 case (FAdd e1 e2) |
|
451 note split = split_aux_correct' [where xs=xs and |
|
452 e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"] |
|
453 { |
|
454 case 1 |
|
455 let ?left = "peval xs (Left (Denom e1) (Denom e2))" |
|
456 let ?common = "peval xs (Common (Denom e1) (Denom e2))" |
|
457 let ?right = "peval xs (Right (Denom e1) (Denom e2))" |
|
458 from 1 FAdd |
|
459 have "feval xs (FAdd e1 e2) = |
|
460 (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<oplus> peval xs (Num e2) \<otimes> ?left)) \<oslash> |
|
461 (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))" |
|
462 by (simp add: split_beta split nonzero_union |
|
463 add_frac_eq r_distr m_ac) |
|
464 also from 1 FAdd have "\<dots> = |
|
465 peval xs (Num (FAdd e1 e2)) \<oslash> peval xs (Denom (FAdd e1 e2))" |
|
466 by (simp add: split_beta split nonzero_union npeadd_correct npemul_correct integral_iff) |
|
467 finally show ?case . |
|
468 next |
|
469 case 2 |
|
470 with FAdd show ?case |
|
471 by (simp add: split_beta split nonzero_union npemul_correct integral_iff) |
|
472 } |
|
473 next |
|
474 case (FSub e1 e2) |
|
475 note split = split_aux_correct' [where xs=xs and |
|
476 e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"] |
|
477 { |
|
478 case 1 |
|
479 let ?left = "peval xs (Left (Denom e1) (Denom e2))" |
|
480 let ?common = "peval xs (Common (Denom e1) (Denom e2))" |
|
481 let ?right = "peval xs (Right (Denom e1) (Denom e2))" |
|
482 from 1 FSub |
|
483 have "feval xs (FSub e1 e2) = |
|
484 (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<ominus> peval xs (Num e2) \<otimes> ?left)) \<oslash> |
|
485 (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))" |
|
486 by (simp add: split_beta split nonzero_union |
|
487 diff_frac_eq r_diff_distr m_ac) |
|
488 also from 1 FSub have "\<dots> = |
|
489 peval xs (Num (FSub e1 e2)) \<oslash> peval xs (Denom (FSub e1 e2))" |
|
490 by (simp add: split_beta split nonzero_union npesub_correct npemul_correct integral_iff) |
|
491 finally show ?case . |
|
492 next |
|
493 case 2 |
|
494 with FSub show ?case |
|
495 by (simp add: split_beta split nonzero_union npemul_correct integral_iff) |
|
496 } |
|
497 next |
|
498 case (FMul e1 e2) |
|
499 note split = |
|
500 split_aux_correct' [where xs=xs and |
|
501 e\<^sub>1="Num e1" and e\<^sub>2="Denom e2"] |
|
502 split_aux_correct' [where xs=xs and |
|
503 e\<^sub>1="Num e2" and e\<^sub>2="Denom e1"] |
|
504 { |
|
505 case 1 |
|
506 let ?left\<^sub>1 = "peval xs (Left (Num e1) (Denom e2))" |
|
507 let ?common\<^sub>1 = "peval xs (Common (Num e1) (Denom e2))" |
|
508 let ?right\<^sub>1 = "peval xs (Right (Num e1) (Denom e2))" |
|
509 let ?left\<^sub>2 = "peval xs (Left (Num e2) (Denom e1))" |
|
510 let ?common\<^sub>2 = "peval xs (Common (Num e2) (Denom e1))" |
|
511 let ?right\<^sub>2 = "peval xs (Right (Num e2) (Denom e1))" |
|
512 from 1 FMul |
|
513 have "feval xs (FMul e1 e2) = |
|
514 ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?left\<^sub>2)) \<oslash> |
|
515 ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?right\<^sub>2 \<otimes> ?right\<^sub>1))" |
|
516 by (simp add: split_beta split nonzero_union |
|
517 nonzero_divide_divide_eq_left m_ac) |
|
518 also from 1 FMul have "\<dots> = |
|
519 peval xs (Num (FMul e1 e2)) \<oslash> peval xs (Denom (FMul e1 e2))" |
|
520 by (simp add: split_beta split nonzero_union npemul_correct integral_iff) |
|
521 finally show ?case . |
|
522 next |
|
523 case 2 |
|
524 with FMul show ?case |
|
525 by (simp add: split_beta split nonzero_union npemul_correct integral_iff) |
|
526 } |
|
527 next |
|
528 case (FNeg e) |
|
529 { |
|
530 case 1 |
|
531 with FNeg show ?case |
|
532 by (simp add: split_beta npeneg_correct) |
|
533 next |
|
534 case 2 |
|
535 with FNeg show ?case |
|
536 by (simp add: split_beta) |
|
537 } |
|
538 next |
|
539 case (FDiv e1 e2) |
|
540 note split = |
|
541 split_aux_correct' [where xs=xs and |
|
542 e\<^sub>1="Num e1" and e\<^sub>2="Num e2"] |
|
543 split_aux_correct' [where xs=xs and |
|
544 e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"] |
|
545 { |
|
546 case 1 |
|
547 let ?left\<^sub>1 = "peval xs (Left (Num e1) (Num e2))" |
|
548 let ?common\<^sub>1 = "peval xs (Common (Num e1) (Num e2))" |
|
549 let ?right\<^sub>1 = "peval xs (Right (Num e1) (Num e2))" |
|
550 let ?left\<^sub>2 = "peval xs (Left (Denom e1) (Denom e2))" |
|
551 let ?common\<^sub>2 = "peval xs (Common (Denom e1) (Denom e2))" |
|
552 let ?right\<^sub>2 = "peval xs (Right (Denom e1) (Denom e2))" |
|
553 from 1 FDiv |
|
554 have "feval xs (FDiv e1 e2) = |
|
555 ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?right\<^sub>2)) \<oslash> |
|
556 ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>2 \<otimes> ?right\<^sub>1))" |
|
557 by (simp add: split_beta split nonzero_union nonzero_insert |
|
558 nonzero_divide_divide_eq m_ac) |
|
559 also from 1 FDiv have "\<dots> = |
|
560 peval xs (Num (FDiv e1 e2)) \<oslash> peval xs (Denom (FDiv e1 e2))" |
|
561 by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff) |
|
562 finally show ?case . |
|
563 next |
|
564 case 2 |
|
565 with FDiv show ?case |
|
566 by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff) |
|
567 } |
|
568 next |
|
569 case (FPow e n) |
|
570 { |
|
571 case 1 |
|
572 with FPow show ?case |
|
573 by (simp add: split_beta nonzero_power_divide npepow_correct) |
|
574 next |
|
575 case 2 |
|
576 with FPow show ?case |
|
577 by (simp add: split_beta npepow_correct) |
|
578 } |
|
579 qed |
|
580 |
|
581 lemma (in field) feval_eq0: |
|
582 assumes "in_carrier xs" |
|
583 and "fnorm e = (n, d, c)" |
|
584 and "nonzero xs c" |
|
585 and "peval xs n = \<zero>" |
|
586 shows "feval xs e = \<zero>" |
|
587 using assms fnorm_correct [of xs e] |
|
588 by simp |
|
589 |
|
590 lemma (in field) fexpr_in_carrier: |
|
591 assumes "in_carrier xs" |
|
592 and "nonzero xs (Cond e)" |
|
593 shows "feval xs e \<in> carrier R" |
|
594 using assms |
|
595 proof (induct e) |
|
596 case (FDiv e1 e2) |
|
597 then have "feval xs e1 \<in> carrier R" "feval xs e2 \<in> carrier R" |
|
598 "peval xs (Num e2) \<noteq> \<zero>" "nonzero xs (Cond e2)" |
|
599 by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm) |
|
600 from `in_carrier xs` `nonzero xs (Cond e2)` |
|
601 have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)" |
|
602 by (rule fnorm_correct) |
|
603 moreover from `in_carrier xs` `nonzero xs (Cond e2)` |
|
604 have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct) |
|
605 ultimately have "feval xs e2 \<noteq> \<zero>" using `peval xs (Num e2) \<noteq> \<zero>` `in_carrier xs` |
|
606 by (simp add: divide_eq_0_iff) |
|
607 with `feval xs e1 \<in> carrier R` `feval xs e2 \<in> carrier R` |
|
608 show ?case by simp |
|
609 qed (simp_all add: nonzero_union split: prod.split_asm) |
|
610 |
|
611 lemma (in field) feval_eq: |
|
612 assumes "in_carrier xs" |
|
613 and "fnorm (FSub e e') = (n, d, c)" |
|
614 and "nonzero xs c" |
|
615 shows "(feval xs e = feval xs e') = (peval xs n = \<zero>)" |
|
616 proof - |
|
617 from assms have "nonzero xs (Cond e)" "nonzero xs (Cond e')" |
|
618 by (auto simp add: nonzero_union split: prod.split_asm) |
|
619 with assms fnorm_correct [of xs "FSub e e'"] |
|
620 have "feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d" |
|
621 "peval xs d \<noteq> \<zero>" |
|
622 by simp_all |
|
623 show ?thesis |
|
624 proof |
|
625 assume "feval xs e = feval xs e'" |
|
626 with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d` |
|
627 `in_carrier xs` `nonzero xs (Cond e')` |
|
628 have "peval xs n \<oslash> peval xs d = \<zero>" |
|
629 by (simp add: fexpr_in_carrier minus_eq r_neg) |
|
630 with `peval xs d \<noteq> \<zero>` `in_carrier xs` |
|
631 show "peval xs n = \<zero>" |
|
632 by (simp add: divide_eq_0_iff) |
|
633 next |
|
634 assume "peval xs n = \<zero>" |
|
635 with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d` `peval xs d \<noteq> \<zero>` |
|
636 `nonzero xs (Cond e)` `nonzero xs (Cond e')` `in_carrier xs` |
|
637 show "feval xs e = feval xs e'" |
|
638 by (simp add: eq_diff0 fexpr_in_carrier) |
|
639 qed |
|
640 qed |
|
641 |
|
642 code_reflect Field_Code |
|
643 datatypes fexpr = FCnst | FVar | FAdd | FSub | FMul | FNeg | FDiv | FPow |
|
644 and pexpr = PExpr1 | PExpr2 |
|
645 and pexpr1 = PCnst | PVar | PAdd | PSub | PNeg |
|
646 and pexpr2 = PMul | PPow |
|
647 functions fnorm |
|
648 term_of_fexpr_inst.term_of_fexpr |
|
649 term_of_pexpr_inst.term_of_pexpr |
|
650 equal_pexpr_inst.equal_pexpr |
|
651 |
|
652 definition field_codegen_aux :: "(pexpr \<times> pexpr list) itself" where |
|
653 "field_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::(pexpr \<times> pexpr list) itself)" |
|
654 |
|
655 ML {* |
|
656 signature FIELD_TAC = |
|
657 sig |
|
658 structure Field_Simps: |
|
659 sig |
|
660 type T |
|
661 val get: Context.generic -> T |
|
662 val put: T -> Context.generic -> Context.generic |
|
663 val map: (T -> T) -> Context.generic -> Context.generic |
|
664 end |
|
665 val eq_field_simps: |
|
666 (term * (thm list * thm list * thm list * thm * thm)) * |
|
667 (term * (thm list * thm list * thm list * thm * thm)) -> bool |
|
668 val field_tac: bool -> Proof.context -> int -> tactic |
|
669 end |
|
670 |
|
671 structure Field_Tac : FIELD_TAC = |
|
672 struct |
|
673 |
|
674 open Ring_Tac; |
|
675 |
|
676 fun field_struct (Const (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R |
|
677 | field_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R |
|
678 | field_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R |
|
679 | field_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R |
|
680 | field_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R |
|
681 | field_struct (Const (@{const_name Algebra_Aux.m_div}, _) $ R $ _ $ _) = SOME R |
|
682 | field_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R |
|
683 | field_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R |
|
684 | field_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R |
|
685 | field_struct _ = NONE; |
|
686 |
|
687 fun reif_fexpr vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) = |
|
688 @{const FAdd} $ reif_fexpr vs a $ reif_fexpr vs b |
|
689 | reif_fexpr vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) = |
|
690 @{const FSub} $ reif_fexpr vs a $ reif_fexpr vs b |
|
691 | reif_fexpr vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) = |
|
692 @{const FMul} $ reif_fexpr vs a $ reif_fexpr vs b |
|
693 | reif_fexpr vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) = |
|
694 @{const FNeg} $ reif_fexpr vs a |
|
695 | reif_fexpr vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) = |
|
696 @{const FPow} $ reif_fexpr vs a $ n |
|
697 | reif_fexpr vs (Const (@{const_name Algebra_Aux.m_div}, _) $ _ $ a $ b) = |
|
698 @{const FDiv} $ reif_fexpr vs a $ reif_fexpr vs b |
|
699 | reif_fexpr vs (Free x) = |
|
700 @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs) |
|
701 | reif_fexpr vs (Const (@{const_name Ring.ring.zero}, _) $ _) = |
|
702 @{term "FCnst 0"} |
|
703 | reif_fexpr vs (Const (@{const_name Group.monoid.one}, _) $ _) = |
|
704 @{term "FCnst 1"} |
|
705 | reif_fexpr vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) = |
|
706 @{const FCnst} $ n |
|
707 | reif_fexpr _ _ = error "reif_fexpr: bad expression"; |
|
708 |
|
709 fun reif_fexpr' vs (Const (@{const_name Groups.plus}, _) $ a $ b) = |
|
710 @{const FAdd} $ reif_fexpr' vs a $ reif_fexpr' vs b |
|
711 | reif_fexpr' vs (Const (@{const_name Groups.minus}, _) $ a $ b) = |
|
712 @{const FSub} $ reif_fexpr' vs a $ reif_fexpr' vs b |
|
713 | reif_fexpr' vs (Const (@{const_name Groups.times}, _) $ a $ b) = |
|
714 @{const FMul} $ reif_fexpr' vs a $ reif_fexpr' vs b |
|
715 | reif_fexpr' vs (Const (@{const_name Groups.uminus}, _) $ a) = |
|
716 @{const FNeg} $ reif_fexpr' vs a |
|
717 | reif_fexpr' vs (Const (@{const_name Power.power}, _) $ a $ n) = |
|
718 @{const FPow} $ reif_fexpr' vs a $ n |
|
719 | reif_fexpr' vs (Const (@{const_name divide}, _) $ a $ b) = |
|
720 @{const FDiv} $ reif_fexpr' vs a $ reif_fexpr' vs b |
|
721 | reif_fexpr' vs (Free x) = |
|
722 @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs) |
|
723 | reif_fexpr' vs (Const (@{const_name zero_class.zero}, _)) = |
|
724 @{term "FCnst 0"} |
|
725 | reif_fexpr' vs (Const (@{const_name one_class.one}, _)) = |
|
726 @{term "FCnst 1"} |
|
727 | reif_fexpr' vs (Const (@{const_name numeral}, _) $ b) = |
|
728 @{const FCnst} $ (@{const numeral (int)} $ b) |
|
729 | reif_fexpr' _ _ = error "reif_fexpr: bad expression"; |
|
730 |
|
731 fun eq_field_simps |
|
732 ((t, (ths1, ths2, ths3, th4, th)), |
|
733 (t', (ths1', ths2', ths3', th4', th'))) = |
|
734 t aconv t' andalso |
|
735 eq_list Thm.eq_thm (ths1, ths1') andalso |
|
736 eq_list Thm.eq_thm (ths2, ths2') andalso |
|
737 eq_list Thm.eq_thm (ths3, ths3') andalso |
|
738 Thm.eq_thm (th4, th4') andalso |
|
739 Thm.eq_thm (th, th'); |
|
740 |
|
741 structure Field_Simps = Generic_Data |
|
742 (struct |
|
743 type T = (term * (thm list * thm list * thm list * thm * thm)) Net.net |
|
744 val empty = Net.empty |
|
745 val extend = I |
|
746 val merge = Net.merge eq_field_simps |
|
747 end); |
|
748 |
|
749 fun get_field_simps ctxt optcT t = |
|
750 (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of |
|
751 SOME (ths1, ths2, ths3, th4, th) => |
|
752 let val tr = |
|
753 Thm.transfer (Proof_Context.theory_of ctxt) #> |
|
754 (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) |
|
755 in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end |
|
756 | NONE => error "get_field_simps: lookup failed"); |
|
757 |
|
758 fun nth_el_conv (_, _, _, nth_el_Cons, _) = |
|
759 let |
|
760 val a = type_of_eqn nth_el_Cons; |
|
761 val If_conv_a = If_conv a; |
|
762 |
|
763 fun conv ys n = (case strip_app ys of |
|
764 (@{const_name Cons}, [x, xs]) => |
|
765 transitive' |
|
766 (inst [] [x, xs, n] nth_el_Cons) |
|
767 (If_conv_a (args2 nat_eq_conv) |
|
768 Thm.reflexive |
|
769 (cong2' conv Thm.reflexive (args2 nat_minus_conv)))) |
|
770 in conv end; |
|
771 |
|
772 fun feval_conv (rls as |
|
773 ([feval_simps_1, feval_simps_2, feval_simps_3, |
|
774 feval_simps_4, feval_simps_5, feval_simps_6, |
|
775 feval_simps_7, feval_simps_8, feval_simps_9, |
|
776 feval_simps_10, feval_simps_11], |
|
777 _, _, _, _)) = |
|
778 let |
|
779 val nth_el_conv' = nth_el_conv rls; |
|
780 |
|
781 fun conv xs x = (case strip_app x of |
|
782 (@{const_name FCnst}, [c]) => (case strip_app c of |
|
783 (@{const_name zero_class.zero}, _) => inst [] [xs] feval_simps_9 |
|
784 | (@{const_name one_class.one}, _) => inst [] [xs] feval_simps_10 |
|
785 | (@{const_name numeral}, [n]) => inst [] [xs, n] feval_simps_11 |
|
786 | _ => inst [] [xs, c] feval_simps_1) |
|
787 | (@{const_name FVar}, [n]) => |
|
788 transitive' (inst [] [xs, n] feval_simps_2) (args2 nth_el_conv') |
|
789 | (@{const_name FAdd}, [a, b]) => |
|
790 transitive' (inst [] [xs, a, b] feval_simps_3) |
|
791 (cong2 (args2 conv) (args2 conv)) |
|
792 | (@{const_name FSub}, [a, b]) => |
|
793 transitive' (inst [] [xs, a, b] feval_simps_4) |
|
794 (cong2 (args2 conv) (args2 conv)) |
|
795 | (@{const_name FMul}, [a, b]) => |
|
796 transitive' (inst [] [xs, a, b] feval_simps_5) |
|
797 (cong2 (args2 conv) (args2 conv)) |
|
798 | (@{const_name FNeg}, [a]) => |
|
799 transitive' (inst [] [xs, a] feval_simps_6) |
|
800 (cong1 (args2 conv)) |
|
801 | (@{const_name FDiv}, [a, b]) => |
|
802 transitive' (inst [] [xs, a, b] feval_simps_7) |
|
803 (cong2 (args2 conv) (args2 conv)) |
|
804 | (@{const_name FPow}, [a, n]) => |
|
805 transitive' (inst [] [xs, a, n] feval_simps_8) |
|
806 (cong2 (args2 conv) Thm.reflexive)) |
|
807 in conv end; |
|
808 |
|
809 fun peval_conv (rls as |
|
810 (_, |
|
811 [peval_simps_1, peval_simps_2, peval_simps_3, |
|
812 peval_simps_4, peval_simps_5, peval_simps_6, |
|
813 peval_simps_7, peval_simps_8, peval_simps_9, |
|
814 peval_simps_10, peval_simps_11], |
|
815 _, _, _)) = |
|
816 let |
|
817 val nth_el_conv' = nth_el_conv rls; |
|
818 |
|
819 fun conv xs x = (case strip_app x of |
|
820 (@{const_name PExpr1}, [e]) => (case strip_app e of |
|
821 (@{const_name PCnst}, [c]) => (case strip_numeral c of |
|
822 (@{const_name zero_class.zero}, _) => inst [] [xs] peval_simps_8 |
|
823 | (@{const_name one_class.one}, _) => inst [] [xs] peval_simps_9 |
|
824 | (@{const_name numeral}, [n]) => inst [] [xs, n] peval_simps_10 |
|
825 | (@{const_name uminus}, [n]) => inst [] [xs, n] peval_simps_11 |
|
826 | _ => inst [] [xs, c] peval_simps_1) |
|
827 | (@{const_name PVar}, [n]) => |
|
828 transitive' (inst [] [xs, n] peval_simps_2) (args2 nth_el_conv') |
|
829 | (@{const_name PAdd}, [a, b]) => |
|
830 transitive' (inst [] [xs, a, b] peval_simps_3) |
|
831 (cong2 (args2 conv) (args2 conv)) |
|
832 | (@{const_name PSub}, [a, b]) => |
|
833 transitive' (inst [] [xs, a, b] peval_simps_4) |
|
834 (cong2 (args2 conv) (args2 conv)) |
|
835 | (@{const_name PNeg}, [a]) => |
|
836 transitive' (inst [] [xs, a] peval_simps_5) |
|
837 (cong1 (args2 conv))) |
|
838 | (@{const_name PExpr2}, [e]) => (case strip_app e of |
|
839 (@{const_name PMul}, [a, b]) => |
|
840 transitive' (inst [] [xs, a, b] peval_simps_6) |
|
841 (cong2 (args2 conv) (args2 conv)) |
|
842 | (@{const_name PPow}, [a, n]) => |
|
843 transitive' (inst [] [xs, a, n] peval_simps_7) |
|
844 (cong2 (args2 conv) Thm.reflexive))) |
|
845 in conv end; |
|
846 |
|
847 fun nonzero_conv (rls as |
|
848 (_, _, |
|
849 [nonzero_Nil, nonzero_Cons, nonzero_singleton], |
|
850 _, _)) = |
|
851 let |
|
852 val peval_conv' = peval_conv rls; |
|
853 |
|
854 fun conv xs qs = (case strip_app qs of |
|
855 (@{const_name Nil}, []) => inst [] [xs] nonzero_Nil |
|
856 | (@{const_name Cons}, [p, ps]) => (case Thm.term_of ps of |
|
857 Const (@{const_name Nil}, _) => |
|
858 transitive' (inst [] [xs, p] nonzero_singleton) |
|
859 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) |
|
860 | _ => transitive' (inst [] [xs, p, ps] nonzero_Cons) |
|
861 (cong2 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) (args2 conv)))) |
|
862 in conv end; |
|
863 |
|
864 val cv = Code_Evaluation.static_conv |
|
865 {ctxt = @{context}, |
|
866 consts = |
|
867 [@{const_name nat_of_integer}, |
|
868 @{const_name fnorm}, @{const_name field_codegen_aux}]}; |
|
869 |
|
870 fun field_tac in_prem ctxt = |
|
871 SUBGOAL (fn (g, i) => |
|
872 let |
|
873 val (prems, concl) = Logic.strip_horn g; |
|
874 fun find_eq s = (case s of |
|
875 (_ $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t $ u)) => |
|
876 (case (field_struct t, field_struct u) of |
|
877 (SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr) |
|
878 | (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr) |
|
879 | _ => |
|
880 if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort field}) |
|
881 then SOME ((t, u), mk_ring T, T, SOME T, K @{thm in_carrier_trivial}, reif_fexpr') |
|
882 else NONE) |
|
883 | _ => NONE); |
|
884 val ((t, u), R, T, optT, mkic, reif) = |
|
885 (case get_first find_eq |
|
886 (if in_prem then prems else [concl]) of |
|
887 SOME q => q |
|
888 | NONE => error "cannot determine field"); |
|
889 val rls as (_, _, _, _, feval_eq) = |
|
890 get_field_simps ctxt (Option.map (Thm.ctyp_of ctxt) optT) R; |
|
891 val xs = [] |> Term.add_frees t |> Term.add_frees u |> filter (equal T o snd); |
|
892 val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs)); |
|
893 val ce = Thm.cterm_of ctxt (reif xs t); |
|
894 val ce' = Thm.cterm_of ctxt (reif xs u); |
|
895 val fnorm = cv ctxt |
|
896 (Thm.apply @{cterm fnorm} (Thm.apply (Thm.apply @{cterm FSub} ce) ce')); |
|
897 val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm); |
|
898 val (_, [_, c]) = strip_app dc; |
|
899 val th = |
|
900 Conv.fconv_rule (Conv.concl_conv 1 (Conv.arg_conv |
|
901 (binop_conv |
|
902 (binop_conv |
|
903 (K (feval_conv rls cxs ce)) (K (feval_conv rls cxs ce'))) |
|
904 (Conv.arg1_conv (K (peval_conv rls cxs n)))))) |
|
905 ([mkic xs, |
|
906 mk_obj_eq fnorm, |
|
907 mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS |
|
908 feval_eq); |
|
909 val th' = Drule.rotate_prems 1 |
|
910 (th RS (if in_prem then @{thm iffD1} else @{thm iffD2})); |
|
911 in |
|
912 if in_prem then |
|
913 dresolve_tac ctxt [th'] 1 THEN defer_tac 1 |
|
914 else |
|
915 resolve_tac ctxt [th'] 1 |
|
916 end); |
|
917 |
|
918 end |
|
919 *} |
|
920 |
|
921 context field begin |
|
922 |
|
923 local_setup {* |
|
924 Local_Theory.declaration {syntax = false, pervasive = false} |
|
925 (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps |
|
926 (Morphism.term phi @{term R}, |
|
927 (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]}, |
|
928 Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]}, |
|
929 Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]}, |
|
930 singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]}, |
|
931 singleton (Morphism.fact phi) @{thm feval_eq})))) |
|
932 *} |
|
933 |
|
934 end |
|
935 |
|
936 method_setup field = {* |
|
937 Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt => |
|
938 SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt)) |
|
939 *} "reduce equations over fields to equations over rings" |
|
940 |
|
941 end |