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--
```     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
```