src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 44779 98d597c4193d
child 53374 a14d2a854c02
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
     1 (*  Author:     Bernhard Haeupler
     2 
     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 *)
     7 
     8 header {* Proof of the relative completeness of method comm-ring *}
     9 
    10 theory Commutative_Ring_Complete
    11 imports Commutative_Ring
    12 begin
    13 
    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"
    26 
    27 (* Some helpful lemmas *)
    28 lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
    29   by (cases P) auto
    30 
    31 lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
    32   by (cases i) auto
    33 
    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)
    36 
    37 lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
    38   by (cases i) (auto, cases P, auto, case_tac pol2, auto)
    39 
    40 lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
    41   by (cases i) (auto, cases P, auto, case_tac pol2, auto)
    42 
    43 lemma mkPinj_cn: "y ~= 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
    44   apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
    45   apply (case_tac nat, auto simp add: norm_Pinj_0_False)
    46   apply (case_tac pol, auto)
    47   apply (case_tac y, auto)
    48   done
    49 
    50 lemma norm_PXtrans: 
    51   assumes A: "isnorm (PX P x Q)" and "isnorm Q2" 
    52   shows "isnorm (PX P x Q2)"
    53 proof (cases P)
    54   case (PX p1 y p2)
    55   with assms show ?thesis by (cases x) (auto, cases p2, auto)
    56 next
    57   case Pc
    58   with assms show ?thesis by (cases x) auto
    59 next
    60   case Pinj
    61   with assms show ?thesis by (cases x) auto
    62 qed
    63  
    64 lemma norm_PXtrans2:
    65   assumes "isnorm (PX P x Q)" and "isnorm Q2"
    66   shows "isnorm (PX P (Suc (n+x)) Q2)"
    67 proof (cases P)
    68   case (PX p1 y p2)
    69   with assms show ?thesis by (cases x) (auto, cases p2, auto)
    70 next
    71   case Pc
    72   with assms show ?thesis by (cases x) auto
    73 next
    74   case Pinj
    75   with assms show ?thesis by (cases x) auto
    76 qed
    77 
    78 text {* mkPX conserves normalizedness (@{text "_cn"}) *}
    79 lemma mkPX_cn: 
    80   assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q" 
    81   shows "isnorm (mkPX P x Q)"
    82 proof(cases P)
    83   case (Pc c)
    84   with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    85 next
    86   case (Pinj i Q)
    87   with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    88 next
    89   case (PX P1 y P2)
    90   with assms have Y0: "y > 0" by (cases y) auto
    91   from assms PX have "isnorm P1" "isnorm P2"
    92     by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
    93   from assms PX Y0 show ?thesis
    94     by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
    95 qed
    96 
    97 text {* add conserves normalizedness *}
    98 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
    99 proof (induct P Q rule: add.induct)
   100   case (2 c i P2)
   101   thus ?case by (cases P2) (simp_all, cases i, simp_all)
   102 next
   103   case (3 i P2 c)
   104   thus ?case by (cases P2) (simp_all, cases i, simp_all)
   105 next
   106   case (4 c P2 i Q2)
   107   then have "isnorm P2" "isnorm Q2"
   108     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   109   with 4 show ?case
   110     by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
   111 next
   112   case (5 P2 i Q2 c)
   113   then have "isnorm P2" "isnorm Q2"
   114     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   115   with 5 show ?case
   116     by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
   117 next
   118   case (6 x P2 y Q2)
   119   then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
   120   with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)
   121   have "x < y \<or> x = y \<or> x > y" by arith
   122   moreover
   123   { assume "x<y" hence "EX d. y =d + x" by arith
   124     then obtain d where y: "y = d + x" ..
   125     moreover
   126     note 6 X0
   127     moreover
   128     from 6 have "isnorm P2" "isnorm Q2"
   129       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   130     moreover
   131     from 6 `x < y` y have "isnorm (Pinj d Q2)"
   132       by (cases d, simp, cases Q2, auto)
   133     ultimately have ?case by (simp add: mkPinj_cn) }
   134   moreover
   135   { assume "x=y"
   136     moreover
   137     from 6 have "isnorm P2" "isnorm Q2"
   138       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   139     moreover
   140     note 6 Y0
   141     moreover
   142     ultimately have ?case by (simp add: mkPinj_cn) }
   143   moreover
   144   { assume "x>y" hence "EX d. x = d + y" by arith
   145     then obtain d where x: "x = d + y"..
   146     moreover
   147     note 6 Y0
   148     moreover
   149     from 6 have "isnorm P2" "isnorm Q2"
   150       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   151     moreover
   152     from 6 `x > y` x have "isnorm (Pinj d P2)"
   153       by (cases d) (simp, cases P2, auto)
   154     ultimately have ?case by (simp add: mkPinj_cn) }
   155   ultimately show ?case by blast
   156 next
   157   case (7 x P2 Q2 y R)
   158   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   159   moreover
   160   { assume "x = 0"
   161     with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
   162   moreover
   163   { assume "x = 1"
   164     from 7 have "isnorm R" "isnorm P2"
   165       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   166     with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
   167     with 7 `x = 1` have ?case
   168       by (simp add: norm_PXtrans[of Q2 y _]) }
   169   moreover
   170   { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
   171     then obtain d where X: "x=Suc (Suc d)" ..
   172     with 7 have NR: "isnorm R" "isnorm P2"
   173       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   174     with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   175     with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
   176     with `isnorm (PX Q2 y R)` X have ?case
   177       by (simp add: norm_PXtrans[of Q2 y _]) }
   178   ultimately show ?case by blast
   179 next
   180   case (8 Q2 y R x P2)
   181   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   182   moreover
   183   { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
   184   moreover
   185   { assume "x = 1"
   186     with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   187     with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
   188     with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   189   moreover
   190   { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
   191     then obtain d where X: "x = Suc (Suc d)" ..
   192     with 8 have NR: "isnorm R" "isnorm P2"
   193       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   194     with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   195     with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
   196     with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   197   ultimately show ?case by blast
   198 next
   199   case (9 P1 x P2 Q1 y Q2)
   200   then have Y0: "y>0" by (cases y) auto
   201   with 9 have X0: "x>0" by (cases x) auto
   202   with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
   203     by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
   204   with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
   205     by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
   206   have "y < x \<or> x = y \<or> x < y" by arith
   207   moreover
   208   { assume sm1: "y < x" hence "EX d. x = d + y" by arith
   209     then obtain d where sm2: "x = d + y" ..
   210     note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
   211     moreover
   212     have "isnorm (PX P1 d (Pc 0))" 
   213     proof (cases P1)
   214       case (PX p1 y p2)
   215       with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
   216     next
   217       case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
   218     next
   219       case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
   220     qed
   221     ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
   222     with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
   223   moreover
   224   { assume "x = y"
   225     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
   226     with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
   227   moreover
   228   { assume sm1: "x < y" hence "EX d. y = d + x" by arith
   229     then obtain d where sm2: "y = d + x" ..
   230     note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
   231     moreover
   232     have "isnorm (PX Q1 d (Pc 0))" 
   233     proof (cases Q1)
   234       case (PX p1 y p2)
   235       with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
   236     next
   237       case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
   238     next
   239       case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
   240     qed
   241     ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
   242     with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
   243   ultimately show ?case by blast
   244 qed simp
   245 
   246 text {* mul concerves normalizedness *}
   247 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
   248 proof (induct P Q rule: mul.induct)
   249   case (2 c i P2) thus ?case 
   250     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
   251 next
   252   case (3 i P2 c) thus ?case 
   253     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
   254 next
   255   case (4 c P2 i Q2)
   256   then have "isnorm P2" "isnorm Q2"
   257     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   258   with 4 show ?case 
   259     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
   260 next
   261   case (5 P2 i Q2 c)
   262   then have "isnorm P2" "isnorm Q2"
   263     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
   264   with 5 show ?case
   265     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
   266 next
   267   case (6 x P2 y Q2)
   268   have "x < y \<or> x = y \<or> x > y" by arith
   269   moreover
   270   { assume "x < y" hence "EX d. y = d + x" by arith
   271     then obtain d where y: "y = d + x" ..
   272     moreover
   273     note 6
   274     moreover
   275     from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)
   276     moreover
   277     from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   278     moreover
   279     from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto) 
   280     ultimately have ?case by (simp add: mkPinj_cn) }
   281   moreover
   282   { assume "x = y"
   283     moreover
   284     from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   285     moreover
   286     from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
   287     moreover
   288     note 6
   289     moreover
   290     ultimately have ?case by (simp add: mkPinj_cn) }
   291   moreover
   292   { assume "x > y" hence "EX d. x = d + y" by arith
   293     then obtain d where x: "x = d + y" ..
   294     moreover
   295     note 6
   296     moreover
   297     from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
   298     moreover
   299     from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
   300     moreover
   301     from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
   302     ultimately have ?case by (simp add: mkPinj_cn) }
   303   ultimately show ?case by blast
   304 next
   305   case (7 x P2 Q2 y R)
   306   then have Y0: "y > 0" by (cases y) auto
   307   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   308   moreover
   309   { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
   310   moreover
   311   { assume "x = 1"
   312     from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   313     with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
   314     with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
   315   moreover
   316   { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
   317     then obtain d where X: "x = Suc (Suc d)" ..
   318     from 7 have NR: "isnorm R" "isnorm Q2"
   319       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
   320     moreover
   321     from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   322     moreover
   323     from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
   324     moreover
   325     note 7 X
   326     ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
   327     with Y0 X have ?case by (simp add: mkPX_cn) }
   328   ultimately show ?case by blast
   329 next
   330   case (8 Q2 y R x P2)
   331   then have Y0: "y>0" by (cases y) auto
   332   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   333   moreover
   334   { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
   335   moreover
   336   { assume "x = 1"
   337     from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
   338     with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
   339     with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
   340   moreover
   341   { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
   342     then obtain d where X: "x = Suc (Suc d)" ..
   343     from 8 have NR: "isnorm R" "isnorm Q2"
   344       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
   345     moreover
   346     from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
   347     moreover
   348     from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
   349     moreover
   350     note 8 X
   351     ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
   352     with Y0 X have ?case by (simp add: mkPX_cn) }
   353   ultimately show ?case by blast
   354 next
   355   case (9 P1 x P2 Q1 y Q2)
   356   from 9 have X0: "x > 0" by (cases x) auto
   357   from 9 have Y0: "y > 0" by (cases y) auto
   358   note 9
   359   moreover
   360   from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   361   moreover 
   362   from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
   363   ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
   364     "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" 
   365     by (auto simp add: mkPinj_cn)
   366   with 9 X0 Y0 have
   367     "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
   368     "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"  
   369     "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" 
   370     by (auto simp add: mkPX_cn)
   371   thus ?case by (simp add: add_cn)
   372 qed simp
   373 
   374 text {* neg conserves normalizedness *}
   375 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
   376 proof (induct P)
   377   case (Pinj i P2)
   378   then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
   379   with Pinj show ?case by (cases P2) (auto, cases i, auto)
   380 next
   381   case (PX P1 x P2) note PX1 = this
   382   from PX have "isnorm P2" "isnorm P1"
   383     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   384   with PX show ?case
   385   proof (cases P1)
   386     case (PX p1 y p2)
   387     with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
   388   next
   389     case Pinj
   390     with PX1 show ?thesis by (cases x) auto
   391   qed (cases x, auto)
   392 qed simp
   393 
   394 text {* sub conserves normalizedness *}
   395 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
   396   by (simp add: sub_def add_cn neg_cn)
   397 
   398 text {* sqr conserves normalizizedness *}
   399 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
   400 proof (induct P)
   401   case Pc
   402   then show ?case by simp
   403 next
   404   case (Pinj i Q)
   405   then show ?case
   406     by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
   407 next 
   408   case (PX P1 x P2)
   409   then have "x + x ~= 0" "isnorm P2" "isnorm P1"
   410     by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   411   with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
   412       and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
   413     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   414   then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   415 qed
   416 
   417 text {* pow conserves normalizedness *}
   418 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
   419 proof (induct n arbitrary: P rule: less_induct)
   420   case (less k)
   421   show ?case 
   422   proof (cases "k = 0")
   423     case True
   424     then show ?thesis by simp
   425   next
   426     case False
   427     then have K2: "k div 2 < k" by (cases k) auto
   428     from less have "isnorm (sqr P)" by (simp add: sqr_cn)
   429     with less False K2 show ?thesis
   430       by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
   431   qed
   432 qed
   433 
   434 end