src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
 author wenzelm Wed Sep 07 16:37:50 2011 +0200 (2011-09-07) changeset 44779 98d597c4193d parent 41807 ab5d2d81f9fb child 53374 a14d2a854c02 permissions -rw-r--r--
tuned proofs;
```     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
```