64962
|
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)
|
64998
|
600 |
from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
|
64962
|
601 |
have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
|
|
602 |
by (rule fnorm_correct)
|
64998
|
603 |
moreover from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
|
64962
|
604 |
have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
|
64998
|
605 |
ultimately have "feval xs e2 \<noteq> \<zero>" using \<open>peval xs (Num e2) \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
|
64962
|
606 |
by (simp add: divide_eq_0_iff)
|
64998
|
607 |
with \<open>feval xs e1 \<in> carrier R\<close> \<open>feval xs e2 \<in> carrier R\<close>
|
64962
|
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'"
|
64998
|
626 |
with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close>
|
|
627 |
\<open>in_carrier xs\<close> \<open>nonzero xs (Cond e')\<close>
|
64962
|
628 |
have "peval xs n \<oslash> peval xs d = \<zero>"
|
|
629 |
by (simp add: fexpr_in_carrier minus_eq r_neg)
|
64998
|
630 |
with \<open>peval xs d \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
|
64962
|
631 |
show "peval xs n = \<zero>"
|
|
632 |
by (simp add: divide_eq_0_iff)
|
|
633 |
next
|
|
634 |
assume "peval xs n = \<zero>"
|
64998
|
635 |
with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close> \<open>peval xs d \<noteq> \<zero>\<close>
|
|
636 |
\<open>nonzero xs (Cond e)\<close> \<open>nonzero xs (Cond e')\<close> \<open>in_carrier xs\<close>
|
64962
|
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 |
|
64998
|
655 |
ML \<open>
|
64962
|
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
|
64998
|
919 |
\<close>
|
64962
|
920 |
|
|
921 |
context field begin
|
|
922 |
|
64998
|
923 |
local_setup \<open>
|
64962
|
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}))))
|
64998
|
932 |
\<close>
|
64962
|
933 |
|
|
934 |
end
|
|
935 |
|
64998
|
936 |
method_setup field = \<open>
|
64962
|
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))
|
64998
|
939 |
\<close> "reduce equations over fields to equations over rings"
|
64962
|
940 |
|
|
941 |
end
|