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