src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 58259 52c35a59bbf5 child 58710 7216a10d69ba permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Author:     Bernhard Haeupler
3 This theory is about of the relative completeness of method comm-ring
4 method.  As long as the reified atomic polynomials of type 'a pol are
5 in normal form, the cring method is complete.
6 *)
8 header {* Proof of the relative completeness of method comm-ring *}
10 theory Commutative_Ring_Complete
11 imports Commutative_Ring
12 begin
14 text {* Formalization of normal form *}
15 fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
16 where
17   "isnorm (Pc c) \<longleftrightarrow> True"
18 | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
19 | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"
20 | "isnorm (Pinj 0 P) \<longleftrightarrow> False"
21 | "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"
22 | "isnorm (PX P 0 Q) \<longleftrightarrow> False"
23 | "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"
24 | "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"
25 | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
27 (* Some helpful lemmas *)
28 lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
29   by (cases P) auto
31 lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
32   by (cases i) auto
34 lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
35   by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)
37 lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
38   apply (cases i)
39   apply auto
40   apply (cases P)
41   apply auto
42   apply (rename_tac pol2, case_tac pol2)
43   apply auto
44   done
46 lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
47   apply (cases i)
48   apply auto
49   apply (cases P)
50   apply auto
51   apply (rename_tac pol2, case_tac pol2)
52   apply auto
53   done
55 lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
56   apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
57   apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
58   apply (rename_tac pol a, case_tac pol, auto)
59   apply (case_tac y, auto)
60   done
62 lemma norm_PXtrans:
63   assumes A: "isnorm (PX P x Q)"
64     and "isnorm Q2"
65   shows "isnorm (PX P x Q2)"
66 proof (cases P)
67   case (PX p1 y p2)
68   with assms show ?thesis
69     apply (cases x)
70     apply auto
71     apply (cases p2)
72     apply auto
73     done
74 next
75   case Pc
76   with assms show ?thesis by (cases x) auto
77 next
78   case Pinj
79   with assms show ?thesis by (cases x) auto
80 qed
82 lemma norm_PXtrans2:
83   assumes "isnorm (PX P x Q)"
84     and "isnorm Q2"
85   shows "isnorm (PX P (Suc (n + x)) Q2)"
86 proof (cases P)
87   case (PX p1 y p2)
88   with assms show ?thesis
89     apply (cases x)
90     apply auto
91     apply (cases p2)
92     apply auto
93     done
94 next
95   case Pc
96   with assms show ?thesis
97     by (cases x) auto
98 next
99   case Pinj
100   with assms show ?thesis
101     by (cases x) auto
102 qed
104 text {* mkPX conserves normalizedness (@{text "_cn"}) *}
105 lemma mkPX_cn:
106   assumes "x \<noteq> 0"
107     and "isnorm P"
108     and "isnorm Q"
109   shows "isnorm (mkPX P x Q)"
110 proof (cases P)
111   case (Pc c)
112   with assms show ?thesis
113     by (cases x) (auto simp add: mkPinj_cn mkPX_def)
114 next
115   case (Pinj i Q)
116   with assms show ?thesis
117     by (cases x) (auto simp add: mkPinj_cn mkPX_def)
118 next
119   case (PX P1 y P2)
120   with assms have Y0: "y > 0"
121     by (cases y) auto
122   from assms PX have "isnorm P1" "isnorm P2"
123     by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
124   from assms PX Y0 show ?thesis
125     by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
126 qed
128 text {* add conserves normalizedness *}
129 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
130 proof (induct P Q rule: add.induct)
131   case (2 c i P2)
132   then show ?case
133     by (cases P2) (simp_all, cases i, simp_all)
134 next
135   case (3 i P2 c)
136   then show ?case
137     by (cases P2) (simp_all, cases i, simp_all)
138 next
139   case (4 c P2 i Q2)
140   then have "isnorm P2" "isnorm Q2"
141     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
142   with 4 show ?case
143     by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
144 next
145   case (5 P2 i Q2 c)
146   then have "isnorm P2" "isnorm Q2"
147     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
148   with 5 show ?case
149     by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
150 next
151   case (6 x P2 y Q2)
152   then have Y0: "y > 0"
153     by (cases y) (auto simp add: norm_Pinj_0_False)
154   with 6 have X0: "x > 0"
155     by (cases x) (auto simp add: norm_Pinj_0_False)
156   have "x < y \<or> x = y \<or> x > y" by arith
157   moreover {
158     assume "x < y"
159     then have "\<exists>d. y = d + x" by arith
160     then obtain d where y: "y = d + x" ..
161     moreover
162     note 6 X0
163     moreover
164     from 6 have "isnorm P2" "isnorm Q2"
165       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
166     moreover
167     from 6 `x < y` y have "isnorm (Pinj d Q2)"
168       by (cases d, simp, cases Q2, auto)
169     ultimately have ?case by (simp add: mkPinj_cn)
170   }
171   moreover {
172     assume "x = y"
173     moreover
174     from 6 have "isnorm P2" "isnorm Q2"
175       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
176     moreover
177     note 6 Y0
178     ultimately have ?case by (simp add: mkPinj_cn)
179   }
180   moreover {
181     assume "x > y"
182     then have "\<exists>d. x = d + y"
183       by arith
184     then obtain d where x: "x = d + y" ..
185     moreover
186     note 6 Y0
187     moreover
188     from 6 have "isnorm P2" "isnorm Q2"
189       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
190     moreover
191     from 6 `x > y` x have "isnorm (Pinj d P2)"
192       by (cases d) (simp, cases P2, auto)
193     ultimately have ?case by (simp add: mkPinj_cn)
194   }
195   ultimately show ?case by blast
196 next
197   case (7 x P2 Q2 y R)
198   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
199   moreover {
200     assume "x = 0"
201     with 7 have ?case by (auto simp add: norm_Pinj_0_False)
202   }
203   moreover {
204     assume "x = 1"
205     from 7 have "isnorm R" "isnorm P2"
206       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
207     with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
208     with 7 `x = 1` have ?case
209       by (simp add: norm_PXtrans[of Q2 y _])
210   }
211   moreover {
212     assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
213     then obtain d where X: "x=Suc (Suc d)" ..
214     with 7 have NR: "isnorm R" "isnorm P2"
215       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
216     with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
217     with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
218     with `isnorm (PX Q2 y R)` X have ?case
219       by (simp add: norm_PXtrans[of Q2 y _])
220   }
221   ultimately show ?case by blast
222 next
223   case (8 Q2 y R x P2)
224   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
225   moreover {
226     assume "x = 0"
227     with 8 have ?case
228       by (auto simp add: norm_Pinj_0_False)
229   }
230   moreover {
231     assume "x = 1"
232     with 8 have "isnorm R" "isnorm P2"
233       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
234     with 8 `x = 1` have "isnorm (R \<oplus> P2)"
235       by simp
236     with 8 `x = 1` have ?case
237       by (simp add: norm_PXtrans[of Q2 y _])
238   }
239   moreover {
240     assume "x > 1"
241     then have "\<exists>d. x = Suc (Suc d)" by arith
242     then obtain d where X: "x = Suc (Suc d)" ..
243     with 8 have NR: "isnorm R" "isnorm P2"
244       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
245     with 8 X have "isnorm (Pinj (x - 1) P2)"
246       by (cases P2) auto
247     with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
248       by simp
249     with `isnorm (PX Q2 y R)` X have ?case
250       by (simp add: norm_PXtrans[of Q2 y _])
251   }
252   ultimately show ?case by blast
253 next
254   case (9 P1 x P2 Q1 y Q2)
255   then have Y0: "y > 0" by (cases y) auto
256   with 9 have X0: "x > 0" by (cases x) auto
257   with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
258     by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
259   with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
260     by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
261   have "y < x \<or> x = y \<or> x < y" by arith
262   moreover {
263     assume sm1: "y < x"
264     then have "\<exists>d. x = d + y" by arith
265     then obtain d where sm2: "x = d + y" ..
266     note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
267     moreover
268     have "isnorm (PX P1 d (Pc 0))"
269     proof (cases P1)
270       case (PX p1 y p2)
271       with 9 sm1 sm2 show ?thesis
272         by (cases d) (simp, cases p2, auto)
273     next
274       case Pc
275       with 9 sm1 sm2 show ?thesis
276         by (cases d) auto
277     next
278       case Pinj
279       with 9 sm1 sm2 show ?thesis
280         by (cases d) auto
281     qed
282     ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
283       by auto
284     with Y0 sm1 sm2 have ?case
285       by (simp add: mkPX_cn)
286   }
287   moreover {
288     assume "x = y"
289     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
290       by auto
291     with `x = y` Y0 have ?case
292       by (simp add: mkPX_cn)
293   }
294   moreover {
295     assume sm1: "x < y"
296     then have "\<exists>d. y = d + x" by arith
297     then obtain d where sm2: "y = d + x" ..
298     note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
299     moreover
300     have "isnorm (PX Q1 d (Pc 0))"
301     proof (cases Q1)
302       case (PX p1 y p2)
303       with 9 sm1 sm2 show ?thesis
304         by (cases d) (simp, cases p2, auto)
305     next
306       case Pc
307       with 9 sm1 sm2 show ?thesis
308         by (cases d) auto
309     next
310       case Pinj
311       with 9 sm1 sm2 show ?thesis
312         by (cases d) auto
313     qed
314     ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
315       by auto
316     with X0 sm1 sm2 have ?case
317       by (simp add: mkPX_cn)
318   }
319   ultimately show ?case by blast
320 qed simp
322 text {* mul concerves normalizedness *}
323 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
324 proof (induct P Q rule: mul.induct)
325   case (2 c i P2)
326   then show ?case
327     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
328 next
329   case (3 i P2 c)
330   then show ?case
331     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
332 next
333   case (4 c P2 i Q2)
334   then have "isnorm P2" "isnorm Q2"
335     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
336   with 4 show ?case
337     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
338 next
339   case (5 P2 i Q2 c)
340   then have "isnorm P2" "isnorm Q2"
341     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
342   with 5 show ?case
343     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
344 next
345   case (6 x P2 y Q2)
346   have "x < y \<or> x = y \<or> x > y" by arith
347   moreover {
348     assume "x < y"
349     then have "\<exists>d. y = d + x" by arith
350     then obtain d where y: "y = d + x" ..
351     moreover
352     note 6
353     moreover
354     from 6 have "x > 0"
355       by (cases x) (auto simp add: norm_Pinj_0_False)
356     moreover
357     from 6 have "isnorm P2" "isnorm Q2"
358       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
359     moreover
360     from 6 `x < y` y have "isnorm (Pinj d Q2)"
361       by (cases d) (simp, cases Q2, auto)
362     ultimately have ?case by (simp add: mkPinj_cn)
363   }
364   moreover {
365     assume "x = y"
366     moreover
367     from 6 have "isnorm P2" "isnorm Q2"
368       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
369     moreover
370     from 6 have "y>0"
371       by (cases y) (auto simp add: norm_Pinj_0_False)
372     moreover
373     note 6
374     ultimately have ?case by (simp add: mkPinj_cn)
375   }
376   moreover {
377     assume "x > y"
378     then have "\<exists>d. x = d + y" by arith
379     then obtain d where x: "x = d + y" ..
380     moreover
381     note 6
382     moreover
383     from 6 have "y > 0"
384       by (cases y) (auto simp add: norm_Pinj_0_False)
385     moreover
386     from 6 have "isnorm P2" "isnorm Q2"
387       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
388     moreover
389     from 6 `x > y` x have "isnorm (Pinj d P2)"
390       by (cases d) (simp, cases P2, auto)
391     ultimately have ?case by (simp add: mkPinj_cn)
392   }
393   ultimately show ?case by blast
394 next
395   case (7 x P2 Q2 y R)
396   then have Y0: "y > 0" by (cases y) auto
397   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
398   moreover {
399     assume "x = 0"
400     with 7 have ?case
401       by (auto simp add: norm_Pinj_0_False)
402   }
403   moreover {
404     assume "x = 1"
405     from 7 have "isnorm R" "isnorm P2"
406       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
407     with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
408       by (auto simp add: norm_PX1[of Q2 y R])
409     with 7 `x = 1` Y0 have ?case
410       by (simp add: mkPX_cn)
411   }
412   moreover {
413     assume "x > 1"
414     then have "\<exists>d. x = Suc (Suc d)"
415       by arith
416     then obtain d where X: "x = Suc (Suc d)" ..
417     from 7 have NR: "isnorm R" "isnorm Q2"
418       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
419     moreover
420     from 7 X have "isnorm (Pinj (x - 1) P2)"
421       by (cases P2) auto
422     moreover
423     from 7 have "isnorm (Pinj x P2)"
424       by (cases P2) auto
425     moreover
426     note 7 X
427     ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
428       by auto
429     with Y0 X have ?case
430       by (simp add: mkPX_cn)
431   }
432   ultimately show ?case by blast
433 next
434   case (8 Q2 y R x P2)
435   then have Y0: "y > 0"
436     by (cases y) auto
437   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
438   moreover {
439     assume "x = 0"
440     with 8 have ?case
441       by (auto simp add: norm_Pinj_0_False)
442   }
443   moreover {
444     assume "x = 1"
445     from 8 have "isnorm R" "isnorm P2"
446       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
447     with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
448       by (auto simp add: norm_PX1[of Q2 y R])
449     with 8 `x = 1` Y0 have ?case
450       by (simp add: mkPX_cn)
451   }
452   moreover {
453     assume "x > 1"
454     then have "\<exists>d. x = Suc (Suc d)" by arith
455     then obtain d where X: "x = Suc (Suc d)" ..
456     from 8 have NR: "isnorm R" "isnorm Q2"
457       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
458     moreover
459     from 8 X have "isnorm (Pinj (x - 1) P2)"
460       by (cases P2) auto
461     moreover
462     from 8 X have "isnorm (Pinj x P2)"
463       by (cases P2) auto
464     moreover
465     note 8 X
466     ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
467       by auto
468     with Y0 X have ?case by (simp add: mkPX_cn)
469   }
470   ultimately show ?case by blast
471 next
472   case (9 P1 x P2 Q1 y Q2)
473   from 9 have X0: "x > 0" by (cases x) auto
474   from 9 have Y0: "y > 0" by (cases y) auto
475   note 9
476   moreover
477   from 9 have "isnorm P1" "isnorm P2"
478     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
479   moreover
480   from 9 have "isnorm Q1" "isnorm Q2"
481     by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
482   ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
483     "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
484     by (auto simp add: mkPinj_cn)
485   with 9 X0 Y0 have
486     "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
487     "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
488     "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
489     by (auto simp add: mkPX_cn)
490   then show ?case by (simp add: add_cn)
491 qed simp
493 text {* neg conserves normalizedness *}
494 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
495 proof (induct P)
496   case (Pinj i P2)
497   then have "isnorm P2"
498     by (simp add: norm_Pinj[of i P2])
499   with Pinj show ?case
500     by (cases P2) (auto, cases i, auto)
501 next
502   case (PX P1 x P2) note PX1 = this
503   from PX have "isnorm P2" "isnorm P1"
504     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
505   with PX show ?case
506   proof (cases P1)
507     case (PX p1 y p2)
508     with PX1 show ?thesis
509       by (cases x) (auto, cases p2, auto)
510   next
511     case Pinj
512     with PX1 show ?thesis
513       by (cases x) auto
514   qed (cases x, auto)
515 qed simp
517 text {* sub conserves normalizedness *}
518 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
519   by (simp add: sub_def add_cn neg_cn)
521 text {* sqr conserves normalizizedness *}
522 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
523 proof (induct P)
524   case Pc
525   then show ?case by simp
526 next
527   case (Pinj i Q)
528   then show ?case
529     by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
530 next
531   case (PX P1 x P2)
532   then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
533     by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
534   with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
535       and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
536     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
537   then show ?case
538     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
539 qed
541 text {* pow conserves normalizedness *}
542 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
543 proof (induct n arbitrary: P rule: less_induct)
544   case (less k)
545   show ?case
546   proof (cases "k = 0")
547     case True
548     then show ?thesis by simp
549   next
550     case False
551     then have K2: "k div 2 < k" by (cases k) auto
552     from less have "isnorm (sqr P)" by (simp add: sqr_cn)
553     with less False K2 show ?thesis
554       by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
555   qed
556 qed
558 end