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