src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
 author wenzelm Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) changeset 55990 41c6b99c5fb7 parent 55793 52c8f934ea6f child 58259 52c35a59bbf5 permissions -rw-r--r--
more antiquotations;
```     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   apply (cases i)
```
```    39   apply auto
```
```    40   apply (cases P)
```
```    41   apply auto
```
```    42   apply (case_tac pol2)
```
```    43   apply auto
```
```    44   done
```
```    45
```
```    46 lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
```
```    47   apply (cases i)
```
```    48   apply auto
```
```    49   apply (cases P)
```
```    50   apply auto
```
```    51   apply (case_tac pol2)
```
```    52   apply auto
```
```    53   done
```
```    54
```
```    55 lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
```
```    56   apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
```
```    57   apply (case_tac nat, auto simp add: norm_Pinj_0_False)
```
```    58   apply (case_tac pol, auto)
```
```    59   apply (case_tac y, auto)
```
```    60   done
```
```    61
```
```    62 lemma norm_PXtrans:
```
```    63   assumes A: "isnorm (PX P x Q)"
```
```    64     and "isnorm Q2"
```
```    65   shows "isnorm (PX P x Q2)"
```
```    66 proof (cases P)
```
```    67   case (PX p1 y p2)
```
```    68   with assms show ?thesis
```
```    69     apply (cases x)
```
```    70     apply auto
```
```    71     apply (cases p2)
```
```    72     apply auto
```
```    73     done
```
```    74 next
```
```    75   case Pc
```
```    76   with assms show ?thesis by (cases x) auto
```
```    77 next
```
```    78   case Pinj
```
```    79   with assms show ?thesis by (cases x) auto
```
```    80 qed
```
```    81
```
```    82 lemma norm_PXtrans2:
```
```    83   assumes "isnorm (PX P x Q)"
```
```    84     and "isnorm Q2"
```
```    85   shows "isnorm (PX P (Suc (n + x)) Q2)"
```
```    86 proof (cases P)
```
```    87   case (PX p1 y p2)
```
```    88   with assms show ?thesis
```
```    89     apply (cases x)
```
```    90     apply auto
```
```    91     apply (cases p2)
```
```    92     apply auto
```
```    93     done
```
```    94 next
```
```    95   case Pc
```
```    96   with assms show ?thesis
```
```    97     by (cases x) auto
```
```    98 next
```
```    99   case Pinj
```
```   100   with assms show ?thesis
```
```   101     by (cases x) auto
```
```   102 qed
```
```   103
```
```   104 text {* mkPX conserves normalizedness (@{text "_cn"}) *}
```
```   105 lemma mkPX_cn:
```
```   106   assumes "x \<noteq> 0"
```
```   107     and "isnorm P"
```
```   108     and "isnorm Q"
```
```   109   shows "isnorm (mkPX P x Q)"
```
```   110 proof (cases P)
```
```   111   case (Pc c)
```
```   112   with assms show ?thesis
```
```   113     by (cases x) (auto simp add: mkPinj_cn mkPX_def)
```
```   114 next
```
```   115   case (Pinj i Q)
```
```   116   with assms show ?thesis
```
```   117     by (cases x) (auto simp add: mkPinj_cn mkPX_def)
```
```   118 next
```
```   119   case (PX P1 y P2)
```
```   120   with assms have Y0: "y > 0"
```
```   121     by (cases y) auto
```
```   122   from assms PX have "isnorm P1" "isnorm P2"
```
```   123     by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
```
```   124   from assms PX Y0 show ?thesis
```
```   125     by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
```
```   126 qed
```
```   127
```
```   128 text {* add conserves normalizedness *}
```
```   129 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
```
```   130 proof (induct P Q rule: add.induct)
```
```   131   case (2 c i P2)
```
```   132   then show ?case
```
```   133     by (cases P2) (simp_all, cases i, simp_all)
```
```   134 next
```
```   135   case (3 i P2 c)
```
```   136   then show ?case
```
```   137     by (cases P2) (simp_all, cases i, simp_all)
```
```   138 next
```
```   139   case (4 c P2 i Q2)
```
```   140   then have "isnorm P2" "isnorm Q2"
```
```   141     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   142   with 4 show ?case
```
```   143     by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
```
```   144 next
```
```   145   case (5 P2 i Q2 c)
```
```   146   then have "isnorm P2" "isnorm Q2"
```
```   147     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   148   with 5 show ?case
```
```   149     by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
```
```   150 next
```
```   151   case (6 x P2 y Q2)
```
```   152   then have Y0: "y > 0"
```
```   153     by (cases y) (auto simp add: norm_Pinj_0_False)
```
```   154   with 6 have X0: "x > 0"
```
```   155     by (cases x) (auto simp add: norm_Pinj_0_False)
```
```   156   have "x < y \<or> x = y \<or> x > y" by arith
```
```   157   moreover {
```
```   158     assume "x < y"
```
```   159     then have "\<exists>d. y = d + x" by arith
```
```   160     then obtain d where y: "y = d + x" ..
```
```   161     moreover
```
```   162     note 6 X0
```
```   163     moreover
```
```   164     from 6 have "isnorm P2" "isnorm Q2"
```
```   165       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   166     moreover
```
```   167     from 6 `x < y` y have "isnorm (Pinj d Q2)"
```
```   168       by (cases d, simp, cases Q2, auto)
```
```   169     ultimately have ?case by (simp add: mkPinj_cn)
```
```   170   }
```
```   171   moreover {
```
```   172     assume "x = y"
```
```   173     moreover
```
```   174     from 6 have "isnorm P2" "isnorm Q2"
```
```   175       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   176     moreover
```
```   177     note 6 Y0
```
```   178     ultimately have ?case by (simp add: mkPinj_cn)
```
```   179   }
```
```   180   moreover {
```
```   181     assume "x > y"
```
```   182     then have "\<exists>d. x = d + y"
```
```   183       by arith
```
```   184     then obtain d where x: "x = d + y" ..
```
```   185     moreover
```
```   186     note 6 Y0
```
```   187     moreover
```
```   188     from 6 have "isnorm P2" "isnorm Q2"
```
```   189       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   190     moreover
```
```   191     from 6 `x > y` x have "isnorm (Pinj d P2)"
```
```   192       by (cases d) (simp, cases P2, auto)
```
```   193     ultimately have ?case by (simp add: mkPinj_cn)
```
```   194   }
```
```   195   ultimately show ?case by blast
```
```   196 next
```
```   197   case (7 x P2 Q2 y R)
```
```   198   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
```
```   199   moreover {
```
```   200     assume "x = 0"
```
```   201     with 7 have ?case by (auto simp add: norm_Pinj_0_False)
```
```   202   }
```
```   203   moreover {
```
```   204     assume "x = 1"
```
```   205     from 7 have "isnorm R" "isnorm P2"
```
```   206       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   207     with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
```
```   208     with 7 `x = 1` have ?case
```
```   209       by (simp add: norm_PXtrans[of Q2 y _])
```
```   210   }
```
```   211   moreover {
```
```   212     assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
```
```   213     then obtain d where X: "x=Suc (Suc d)" ..
```
```   214     with 7 have NR: "isnorm R" "isnorm P2"
```
```   215       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   216     with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
```
```   217     with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
```
```   218     with `isnorm (PX Q2 y R)` X have ?case
```
```   219       by (simp add: norm_PXtrans[of Q2 y _])
```
```   220   }
```
```   221   ultimately show ?case by blast
```
```   222 next
```
```   223   case (8 Q2 y R x P2)
```
```   224   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
```
```   225   moreover {
```
```   226     assume "x = 0"
```
```   227     with 8 have ?case
```
```   228       by (auto simp add: norm_Pinj_0_False)
```
```   229   }
```
```   230   moreover {
```
```   231     assume "x = 1"
```
```   232     with 8 have "isnorm R" "isnorm P2"
```
```   233       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   234     with 8 `x = 1` have "isnorm (R \<oplus> P2)"
```
```   235       by simp
```
```   236     with 8 `x = 1` have ?case
```
```   237       by (simp add: norm_PXtrans[of Q2 y _])
```
```   238   }
```
```   239   moreover {
```
```   240     assume "x > 1"
```
```   241     then have "\<exists>d. x = Suc (Suc d)" by arith
```
```   242     then obtain d where X: "x = Suc (Suc d)" ..
```
```   243     with 8 have NR: "isnorm R" "isnorm P2"
```
```   244       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   245     with 8 X have "isnorm (Pinj (x - 1) P2)"
```
```   246       by (cases P2) auto
```
```   247     with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
```
```   248       by simp
```
```   249     with `isnorm (PX Q2 y R)` X have ?case
```
```   250       by (simp add: norm_PXtrans[of Q2 y _])
```
```   251   }
```
```   252   ultimately show ?case by blast
```
```   253 next
```
```   254   case (9 P1 x P2 Q1 y Q2)
```
```   255   then have Y0: "y > 0" by (cases y) auto
```
```   256   with 9 have X0: "x > 0" by (cases x) auto
```
```   257   with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
```
```   258     by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
```
```   259   with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
```
```   260     by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
```
```   261   have "y < x \<or> x = y \<or> x < y" by arith
```
```   262   moreover {
```
```   263     assume sm1: "y < x"
```
```   264     then have "\<exists>d. x = d + y" by arith
```
```   265     then obtain d where sm2: "x = d + y" ..
```
```   266     note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
```
```   267     moreover
```
```   268     have "isnorm (PX P1 d (Pc 0))"
```
```   269     proof (cases P1)
```
```   270       case (PX p1 y p2)
```
```   271       with 9 sm1 sm2 show ?thesis
```
```   272         by (cases d) (simp, cases p2, auto)
```
```   273     next
```
```   274       case Pc
```
```   275       with 9 sm1 sm2 show ?thesis
```
```   276         by (cases d) auto
```
```   277     next
```
```   278       case Pinj
```
```   279       with 9 sm1 sm2 show ?thesis
```
```   280         by (cases d) auto
```
```   281     qed
```
```   282     ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
```
```   283       by auto
```
```   284     with Y0 sm1 sm2 have ?case
```
```   285       by (simp add: mkPX_cn)
```
```   286   }
```
```   287   moreover {
```
```   288     assume "x = y"
```
```   289     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
```
```   290       by auto
```
```   291     with `x = y` Y0 have ?case
```
```   292       by (simp add: mkPX_cn)
```
```   293   }
```
```   294   moreover {
```
```   295     assume sm1: "x < y"
```
```   296     then have "\<exists>d. y = d + x" by arith
```
```   297     then obtain d where sm2: "y = d + x" ..
```
```   298     note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
```
```   299     moreover
```
```   300     have "isnorm (PX Q1 d (Pc 0))"
```
```   301     proof (cases Q1)
```
```   302       case (PX p1 y p2)
```
```   303       with 9 sm1 sm2 show ?thesis
```
```   304         by (cases d) (simp, cases p2, auto)
```
```   305     next
```
```   306       case Pc
```
```   307       with 9 sm1 sm2 show ?thesis
```
```   308         by (cases d) auto
```
```   309     next
```
```   310       case Pinj
```
```   311       with 9 sm1 sm2 show ?thesis
```
```   312         by (cases d) auto
```
```   313     qed
```
```   314     ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
```
```   315       by auto
```
```   316     with X0 sm1 sm2 have ?case
```
```   317       by (simp add: mkPX_cn)
```
```   318   }
```
```   319   ultimately show ?case by blast
```
```   320 qed simp
```
```   321
```
```   322 text {* mul concerves normalizedness *}
```
```   323 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
```
```   324 proof (induct P Q rule: mul.induct)
```
```   325   case (2 c i P2)
```
```   326   then show ?case
```
```   327     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
```
```   328 next
```
```   329   case (3 i P2 c)
```
```   330   then show ?case
```
```   331     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
```
```   332 next
```
```   333   case (4 c P2 i Q2)
```
```   334   then have "isnorm P2" "isnorm Q2"
```
```   335     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   336   with 4 show ?case
```
```   337     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
```
```   338 next
```
```   339   case (5 P2 i Q2 c)
```
```   340   then have "isnorm P2" "isnorm Q2"
```
```   341     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   342   with 5 show ?case
```
```   343     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
```
```   344 next
```
```   345   case (6 x P2 y Q2)
```
```   346   have "x < y \<or> x = y \<or> x > y" by arith
```
```   347   moreover {
```
```   348     assume "x < y"
```
```   349     then have "\<exists>d. y = d + x" by arith
```
```   350     then obtain d where y: "y = d + x" ..
```
```   351     moreover
```
```   352     note 6
```
```   353     moreover
```
```   354     from 6 have "x > 0"
```
```   355       by (cases x) (auto simp add: norm_Pinj_0_False)
```
```   356     moreover
```
```   357     from 6 have "isnorm P2" "isnorm Q2"
```
```   358       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   359     moreover
```
```   360     from 6 `x < y` y have "isnorm (Pinj d Q2)"
```
```   361       by (cases d) (simp, cases Q2, auto)
```
```   362     ultimately have ?case by (simp add: mkPinj_cn)
```
```   363   }
```
```   364   moreover {
```
```   365     assume "x = y"
```
```   366     moreover
```
```   367     from 6 have "isnorm P2" "isnorm Q2"
```
```   368       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   369     moreover
```
```   370     from 6 have "y>0"
```
```   371       by (cases y) (auto simp add: norm_Pinj_0_False)
```
```   372     moreover
```
```   373     note 6
```
```   374     ultimately have ?case by (simp add: mkPinj_cn)
```
```   375   }
```
```   376   moreover {
```
```   377     assume "x > y"
```
```   378     then have "\<exists>d. x = d + y" by arith
```
```   379     then obtain d where x: "x = d + y" ..
```
```   380     moreover
```
```   381     note 6
```
```   382     moreover
```
```   383     from 6 have "y > 0"
```
```   384       by (cases y) (auto simp add: norm_Pinj_0_False)
```
```   385     moreover
```
```   386     from 6 have "isnorm P2" "isnorm Q2"
```
```   387       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   388     moreover
```
```   389     from 6 `x > y` x have "isnorm (Pinj d P2)"
```
```   390       by (cases d) (simp, cases P2, auto)
```
```   391     ultimately have ?case by (simp add: mkPinj_cn)
```
```   392   }
```
```   393   ultimately show ?case by blast
```
```   394 next
```
```   395   case (7 x P2 Q2 y R)
```
```   396   then have Y0: "y > 0" by (cases y) auto
```
```   397   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
```
```   398   moreover {
```
```   399     assume "x = 0"
```
```   400     with 7 have ?case
```
```   401       by (auto simp add: norm_Pinj_0_False)
```
```   402   }
```
```   403   moreover {
```
```   404     assume "x = 1"
```
```   405     from 7 have "isnorm R" "isnorm P2"
```
```   406       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   407     with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
```
```   408       by (auto simp add: norm_PX1[of Q2 y R])
```
```   409     with 7 `x = 1` Y0 have ?case
```
```   410       by (simp add: mkPX_cn)
```
```   411   }
```
```   412   moreover {
```
```   413     assume "x > 1"
```
```   414     then have "\<exists>d. x = Suc (Suc d)"
```
```   415       by arith
```
```   416     then obtain d where X: "x = Suc (Suc d)" ..
```
```   417     from 7 have NR: "isnorm R" "isnorm Q2"
```
```   418       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
```
```   419     moreover
```
```   420     from 7 X have "isnorm (Pinj (x - 1) P2)"
```
```   421       by (cases P2) auto
```
```   422     moreover
```
```   423     from 7 have "isnorm (Pinj x P2)"
```
```   424       by (cases P2) auto
```
```   425     moreover
```
```   426     note 7 X
```
```   427     ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
```
```   428       by auto
```
```   429     with Y0 X have ?case
```
```   430       by (simp add: mkPX_cn)
```
```   431   }
```
```   432   ultimately show ?case by blast
```
```   433 next
```
```   434   case (8 Q2 y R x P2)
```
```   435   then have Y0: "y > 0"
```
```   436     by (cases y) auto
```
```   437   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
```
```   438   moreover {
```
```   439     assume "x = 0"
```
```   440     with 8 have ?case
```
```   441       by (auto simp add: norm_Pinj_0_False)
```
```   442   }
```
```   443   moreover {
```
```   444     assume "x = 1"
```
```   445     from 8 have "isnorm R" "isnorm P2"
```
```   446       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   447     with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
```
```   448       by (auto simp add: norm_PX1[of Q2 y R])
```
```   449     with 8 `x = 1` Y0 have ?case
```
```   450       by (simp add: mkPX_cn)
```
```   451   }
```
```   452   moreover {
```
```   453     assume "x > 1"
```
```   454     then have "\<exists>d. x = Suc (Suc d)" by arith
```
```   455     then obtain d where X: "x = Suc (Suc d)" ..
```
```   456     from 8 have NR: "isnorm R" "isnorm Q2"
```
```   457       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
```
```   458     moreover
```
```   459     from 8 X have "isnorm (Pinj (x - 1) P2)"
```
```   460       by (cases P2) auto
```
```   461     moreover
```
```   462     from 8 X have "isnorm (Pinj x P2)"
```
```   463       by (cases P2) auto
```
```   464     moreover
```
```   465     note 8 X
```
```   466     ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
```
```   467       by auto
```
```   468     with Y0 X have ?case by (simp add: mkPX_cn)
```
```   469   }
```
```   470   ultimately show ?case by blast
```
```   471 next
```
```   472   case (9 P1 x P2 Q1 y Q2)
```
```   473   from 9 have X0: "x > 0" by (cases x) auto
```
```   474   from 9 have Y0: "y > 0" by (cases y) auto
```
```   475   note 9
```
```   476   moreover
```
```   477   from 9 have "isnorm P1" "isnorm P2"
```
```   478     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
```
```   479   moreover
```
```   480   from 9 have "isnorm Q1" "isnorm Q2"
```
```   481     by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
```
```   482   ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
```
```   483     "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
```
```   484     by (auto simp add: mkPinj_cn)
```
```   485   with 9 X0 Y0 have
```
```   486     "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
```
```   487     "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
```
```   488     "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
```
```   489     by (auto simp add: mkPX_cn)
```
```   490   then show ?case by (simp add: add_cn)
```
```   491 qed simp
```
```   492
```
```   493 text {* neg conserves normalizedness *}
```
```   494 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
```
```   495 proof (induct P)
```
```   496   case (Pinj i P2)
```
```   497   then have "isnorm P2"
```
```   498     by (simp add: norm_Pinj[of i P2])
```
```   499   with Pinj show ?case
```
```   500     by (cases P2) (auto, cases i, auto)
```
```   501 next
```
```   502   case (PX P1 x P2) note PX1 = this
```
```   503   from PX have "isnorm P2" "isnorm P1"
```
```   504     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
```
```   505   with PX show ?case
```
```   506   proof (cases P1)
```
```   507     case (PX p1 y p2)
```
```   508     with PX1 show ?thesis
```
```   509       by (cases x) (auto, cases p2, auto)
```
```   510   next
```
```   511     case Pinj
```
```   512     with PX1 show ?thesis
```
```   513       by (cases x) auto
```
```   514   qed (cases x, auto)
```
```   515 qed simp
```
```   516
```
```   517 text {* sub conserves normalizedness *}
```
```   518 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
```
```   519   by (simp add: sub_def add_cn neg_cn)
```
```   520
```
```   521 text {* sqr conserves normalizizedness *}
```
```   522 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
```
```   523 proof (induct P)
```
```   524   case Pc
```
```   525   then show ?case by simp
```
```   526 next
```
```   527   case (Pinj i Q)
```
```   528   then show ?case
```
```   529     by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
```
```   530 next
```
```   531   case (PX P1 x P2)
```
```   532   then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
```
```   533     by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
```
```   534   with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
```
```   535       and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
```
```   536     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
```
```   537   then show ?case
```
```   538     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
```
```   539 qed
```
```   540
```
```   541 text {* pow conserves normalizedness *}
```
```   542 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
```
```   543 proof (induct n arbitrary: P rule: less_induct)
```
```   544   case (less k)
```
```   545   show ?case
```
```   546   proof (cases "k = 0")
```
```   547     case True
```
```   548     then show ?thesis by simp
```
```   549   next
```
```   550     case False
```
```   551     then have K2: "k div 2 < k" by (cases k) auto
```
```   552     from less have "isnorm (sqr P)" by (simp add: sqr_cn)
```
```   553     with less False K2 show ?thesis
```
```   554       by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
```
```   555   qed
```
```   556 qed
```
```   557
```
```   558 end
```