src/HOL/ex/Commutative_Ring_Complete.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17508 c84af7f39a6b
child 22742 06165e40e7bd
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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   (* Fromalization of normal form *)
    16 consts isnorm :: "('a::{comm_ring,recpower}) pol \<Rightarrow> bool"
    17 recdef isnorm "measure size"
    18   "isnorm (Pc c) = True"
    19   "isnorm (Pinj i (Pc c)) = False"
    20   "isnorm (Pinj i (Pinj j Q)) = False"
    21   "isnorm (Pinj 0 P) = False"
    22   "isnorm (Pinj i (PX Q1 j Q2)) = isnorm (PX Q1 j Q2)"
    23   "isnorm (PX P 0 Q) = False"
    24   "isnorm (PX (Pc c) i Q) = (c \<noteq> 0 & isnorm Q)"
    25   "isnorm (PX (PX P1 j (Pc c)) i Q) = (c\<noteq>0 \<and> isnorm(PX P1 j (Pc c))\<and>isnorm Q)"
    26   "isnorm (PX P i Q) = (isnorm P \<and> isnorm Q)"
    27 
    28 (* Some helpful lemmas *)
    29 lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
    30 by(cases P, auto)
    31 
    32 lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
    33 by(cases i, auto)
    34 
    35 lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
    36 by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
    37 
    38 lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
    39 by(cases i, auto, cases P, auto, case_tac pol2, auto)
    40 
    41 lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
    42 by(cases i, auto, cases P, auto, case_tac pol2, auto)
    43 
    44 lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)" 
    45 apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
    46 apply(case_tac nat, auto simp add: norm_Pinj_0_False)
    47 by(case_tac pol, auto) (case_tac y, auto)
    48 
    49 lemma norm_PXtrans: 
    50   assumes A:"isnorm (PX P x Q)" and "isnorm Q2" 
    51   shows "isnorm (PX P x Q2)"
    52 proof(cases P)
    53   case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
    54 next
    55   case Pc from prems show ?thesis by(cases x, auto)
    56 next
    57   case Pinj from prems show ?thesis by(cases x, auto)
    58 qed
    59  
    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     (* mkPX conserves normalizedness (_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     (* add conserves normalizedness *)
    91 lemma add_cn:"\<lbrakk>isnorm P; (isnorm Q)\<rbrakk> \<Longrightarrow> isnorm (add (P, 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 (add (R, 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( add (R, Pinj (x - 1) P2))" "isnorm(PX Q2 y R)" by simp
   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 (add (R, 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( add (R, Pinj (x - 1) P2))" "isnorm(PX Q2 y R)" by simp
   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 (add (P2, Q2))" "isnorm (add (PX P1 (x - y) (Pc 0), 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 (add (P2, Q2))" "isnorm (add (P1, 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 (add (P2, Q2))" "isnorm (add (PX Q1 (y - x) (Pc 0), 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     (* mul concerves normalizedness *)
   217 lemma mul_cn :"\<lbrakk>isnorm P; (isnorm Q)\<rbrakk> \<Longrightarrow> isnorm (mul (P, 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 (mul (R, 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 (mul (R, Pinj (x - 1) P2))" "isnorm (mul (Pinj x P2, 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 (mul (R, 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 (mul (R, Pinj (x - 1) P2))" "isnorm (mul (Pinj x P2, 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 (mul (P1, Q1))" "isnorm (mul (P2, Q2))" "isnorm (mul (P1, mkPinj 1 Q2))" "isnorm (mul (Q1, mkPinj 1 P2))" 
   330     by (auto simp add: mkPinj_cn)
   331   with prems X0 Y0 have "isnorm (mkPX (mul (P1, Q1)) (x + y) (mul (P2, Q2)))" "isnorm (mkPX (mul (P1, mkPinj (Suc 0) Q2)) x (Pc 0))"  
   332     "isnorm (mkPX (mul (Q1, mkPinj (Suc 0) P2)) y (Pc 0))" 
   333     by (auto simp add: mkPX_cn)
   334   thus ?case by (simp add: add_cn)
   335 qed(simp)
   336 
   337     (* neg conserves normalizedness *)
   338 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
   339 proof(induct P rule: neg.induct)
   340   case (Pinj i P2)
   341   from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
   342   with prems show ?case by(cases P2, auto, cases i, auto)
   343 next
   344   case (PX P1 x P2)
   345   from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   346   with prems show ?case
   347   proof(cases P1)
   348     case (PX p1 y p2)
   349     with prems show ?thesis by(cases x, auto, cases p2, auto)
   350   next
   351     case Pinj
   352     with prems show ?thesis by(cases x, auto)
   353   qed(cases x, auto)
   354 qed(simp)
   355 
   356     (* sub conserves normalizedness *)
   357 lemma sub_cn:"\<lbrakk>isnorm p; isnorm q\<rbrakk> \<Longrightarrow> isnorm (sub p q)"
   358 by (simp add: sub_def add_cn neg_cn)
   359 
   360   (* sqr conserves normalizizedness *)
   361 lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
   362 proof(induct P)
   363   case (Pinj i Q)
   364   from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
   365 next 
   366   case (PX P1 x P2)
   367   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])
   368   with prems have "isnorm (mkPX (mul (mul (Pc ((1\<Colon>'a) + (1\<Colon>'a)), P1), mkPinj (Suc 0) P2)) x (Pc (0\<Colon>'a)))"
   369               and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" by( auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   370   thus ?case by( auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   371 qed(simp)
   372 
   373 
   374     (* pow conserves normalizedness  *)
   375 lemma pow_cn:"!! P. \<lbrakk>isnorm P\<rbrakk> \<Longrightarrow> isnorm (pow (P, n))"
   376 proof(induct n rule: nat_less_induct)
   377   case (1 k)
   378   show ?case 
   379   proof(cases "k=0")
   380     case False
   381     hence K2:"k div 2 < k" by (cases k, auto)
   382     from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
   383     with prems K2 show ?thesis by(simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
   384   qed(simp)
   385 qed
   386 
   387 end