src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
 author nipkow Tue Feb 23 16:25:08 2016 +0100 (2016-02-23) changeset 62390 842917225d56 parent 61586 5197a2ecb658 child 64962 bf41e1109db3 permissions -rw-r--r--
more canonical names
```     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 section \<open>Proof of the relative completeness of method comm-ring\<close>
```
```     9
```
```    10 theory Commutative_Ring_Complete
```
```    11 imports Commutative_Ring
```
```    12 begin
```
```    13
```
```    14 text \<open>Formalization of normal form\<close>
```
```    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   subgoal for \<dots> pol2 by (cases pol2) auto
```
```    43   done
```
```    44
```
```    45 lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
```
```    46   apply (cases i)
```
```    47   apply auto
```
```    48   apply (cases P)
```
```    49   apply auto
```
```    50   subgoal for \<dots> pol2 by (cases pol2) auto
```
```    51   done
```
```    52
```
```    53 lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
```
```    54   apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
```
```    55   apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
```
```    56   apply (rename_tac pol a, case_tac pol, auto)
```
```    57   apply (case_tac y, auto)
```
```    58   done
```
```    59
```
```    60 lemma norm_PXtrans:
```
```    61   assumes A: "isnorm (PX P x Q)"
```
```    62     and "isnorm Q2"
```
```    63   shows "isnorm (PX P x Q2)"
```
```    64 proof (cases P)
```
```    65   case (PX p1 y p2)
```
```    66   with assms show ?thesis
```
```    67     apply (cases x)
```
```    68     apply auto
```
```    69     apply (cases p2)
```
```    70     apply auto
```
```    71     done
```
```    72 next
```
```    73   case Pc
```
```    74   with assms show ?thesis
```
```    75     by (cases x) auto
```
```    76 next
```
```    77   case Pinj
```
```    78   with assms show ?thesis
```
```    79     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 \<open>mkPX conserves normalizedness (\<open>_cn\<close>)\<close>
```
```   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     apply (cases x)
```
```   126     apply (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _])
```
```   127     apply (cases P2)
```
```   128     apply auto
```
```   129     done
```
```   130 qed
```
```   131
```
```   132 text \<open>add conserves normalizedness\<close>
```
```   133 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
```
```   134 proof (induct P Q rule: add.induct)
```
```   135   case 1
```
```   136   then show ?case by simp
```
```   137 next
```
```   138   case (2 c i P2)
```
```   139   then show ?case
```
```   140     apply (cases P2)
```
```   141     apply simp_all
```
```   142     apply (cases i)
```
```   143     apply simp_all
```
```   144     done
```
```   145 next
```
```   146   case (3 i P2 c)
```
```   147   then show ?case
```
```   148     apply (cases P2)
```
```   149     apply simp_all
```
```   150     apply (cases i)
```
```   151     apply simp_all
```
```   152     done
```
```   153 next
```
```   154   case (4 c P2 i Q2)
```
```   155   then have "isnorm P2" "isnorm Q2"
```
```   156     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   157   with 4 show ?case
```
```   158     apply (cases i)
```
```   159     apply simp
```
```   160     apply (cases P2)
```
```   161     apply auto
```
```   162     subgoal for \<dots> pol2 by (cases pol2) auto
```
```   163     done
```
```   164 next
```
```   165   case (5 P2 i Q2 c)
```
```   166   then have "isnorm P2" "isnorm Q2"
```
```   167     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   168   with 5 show ?case
```
```   169     apply (cases i)
```
```   170     apply simp
```
```   171     apply (cases P2)
```
```   172     apply auto
```
```   173     subgoal for \<dots> pol2 by (cases pol2) auto
```
```   174     done
```
```   175 next
```
```   176   case (6 x P2 y Q2)
```
```   177   then have Y0: "y > 0"
```
```   178     by (cases y) (auto simp add: norm_Pinj_0_False)
```
```   179   with 6 have X0: "x > 0"
```
```   180     by (cases x) (auto simp add: norm_Pinj_0_False)
```
```   181   consider "x < y" | "x = y" | "x > y" by arith
```
```   182   then show ?case
```
```   183   proof cases
```
```   184     case xy: 1
```
```   185     then obtain d where y: "y = d + x"
```
```   186       by atomize_elim arith
```
```   187     from 6 have *: "isnorm P2" "isnorm Q2"
```
```   188       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   189     from 6 xy y have "isnorm (Pinj d Q2)"
```
```   190       by (cases d, simp, cases Q2, auto)
```
```   191     with 6 X0 y * show ?thesis
```
```   192       by (simp add: mkPinj_cn)
```
```   193   next
```
```   194     case xy: 2
```
```   195     from 6 have "isnorm P2" "isnorm Q2"
```
```   196       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   197     with xy 6 Y0 show ?thesis
```
```   198       by (simp add: mkPinj_cn)
```
```   199   next
```
```   200     case xy: 3
```
```   201     then obtain d where x: "x = d + y"
```
```   202       by atomize_elim arith
```
```   203     from 6 have *: "isnorm P2" "isnorm Q2"
```
```   204       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   205     from 6 xy x have "isnorm (Pinj d P2)"
```
```   206       by (cases d) (simp, cases P2, auto)
```
```   207     with xy 6 Y0 * x show ?thesis by (simp add: mkPinj_cn)
```
```   208   qed
```
```   209 next
```
```   210   case (7 x P2 Q2 y R)
```
```   211   consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
```
```   212     by atomize_elim arith
```
```   213   then show ?case
```
```   214   proof cases
```
```   215     case 1
```
```   216     with 7 show ?thesis
```
```   217       by (auto simp add: norm_Pinj_0_False)
```
```   218   next
```
```   219     case x: 2
```
```   220     from 7 have "isnorm R" "isnorm P2"
```
```   221       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   222     with 7 x have "isnorm (R \<oplus> P2)"
```
```   223       by simp
```
```   224     with 7 x show ?thesis
```
```   225       by (simp add: norm_PXtrans[of Q2 y _])
```
```   226   next
```
```   227     case x: 3
```
```   228     with 7 have NR: "isnorm R" "isnorm P2"
```
```   229       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   230     with 7 x have "isnorm (Pinj (x - 1) P2)"
```
```   231       by (cases P2) auto
```
```   232     with 7 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
```
```   233       by simp
```
```   234     with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
```
```   235       by (simp add: norm_PXtrans[of Q2 y _])
```
```   236   qed
```
```   237 next
```
```   238   case (8 Q2 y R x P2)
```
```   239   consider "x = 0" | "x = 1" | "x > 1"
```
```   240     by arith
```
```   241   then show ?case
```
```   242   proof cases
```
```   243     case 1
```
```   244     with 8 show ?thesis
```
```   245       by (auto simp add: norm_Pinj_0_False)
```
```   246   next
```
```   247     case x: 2
```
```   248     with 8 have "isnorm R" "isnorm P2"
```
```   249       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   250     with 8 x have "isnorm (R \<oplus> P2)"
```
```   251       by simp
```
```   252     with 8 x show ?thesis
```
```   253       by (simp add: norm_PXtrans[of Q2 y _])
```
```   254   next
```
```   255     case x: 3
```
```   256     then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith
```
```   257     with 8 have NR: "isnorm R" "isnorm P2"
```
```   258       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   259     with 8 x have "isnorm (Pinj (x - 1) P2)"
```
```   260       by (cases P2) auto
```
```   261     with 8 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
```
```   262       by simp
```
```   263     with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
```
```   264       by (simp add: norm_PXtrans[of Q2 y _])
```
```   265   qed
```
```   266 next
```
```   267   case (9 P1 x P2 Q1 y Q2)
```
```   268   then have Y0: "y > 0" by (cases y) auto
```
```   269   with 9 have X0: "x > 0" by (cases x) auto
```
```   270   with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
```
```   271     by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
```
```   272   with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
```
```   273     by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
```
```   274   consider "y < x" | "x = y" | "x < y" by arith
```
```   275   then show ?case
```
```   276   proof cases
```
```   277     case xy: 1
```
```   278     then obtain d where x: "x = d + y"
```
```   279       by atomize_elim arith
```
```   280     have "isnorm (PX P1 d (Pc 0))"
```
```   281     proof (cases P1)
```
```   282       case (PX p1 y p2)
```
```   283       with 9 xy x show ?thesis
```
```   284         by (cases d) (simp, cases p2, auto)
```
```   285     next
```
```   286       case Pc
```
```   287       with 9 xy x show ?thesis
```
```   288         by (cases d) auto
```
```   289     next
```
```   290       case Pinj
```
```   291       with 9 xy x show ?thesis
```
```   292         by (cases d) auto
```
```   293     qed
```
```   294     with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
```
```   295       by auto
```
```   296     with Y0 xy x show ?thesis
```
```   297       by (simp add: mkPX_cn)
```
```   298   next
```
```   299     case xy: 2
```
```   300     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
```
```   301       by auto
```
```   302     with xy Y0 show ?thesis
```
```   303       by (simp add: mkPX_cn)
```
```   304   next
```
```   305     case xy: 3
```
```   306     then obtain d where y: "y = d + x"
```
```   307       by atomize_elim arith
```
```   308     have "isnorm (PX Q1 d (Pc 0))"
```
```   309     proof (cases Q1)
```
```   310       case (PX p1 y p2)
```
```   311       with 9 xy y show ?thesis
```
```   312         by (cases d) (simp, cases p2, auto)
```
```   313     next
```
```   314       case Pc
```
```   315       with 9 xy y show ?thesis
```
```   316         by (cases d) auto
```
```   317     next
```
```   318       case Pinj
```
```   319       with 9 xy y show ?thesis
```
```   320         by (cases d) auto
```
```   321     qed
```
```   322     with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
```
```   323       by auto
```
```   324     with X0 xy y show ?thesis
```
```   325       by (simp add: mkPX_cn)
```
```   326   qed
```
```   327 qed
```
```   328
```
```   329 text \<open>mul concerves normalizedness\<close>
```
```   330 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
```
```   331 proof (induct P Q rule: mul.induct)
```
```   332   case 1
```
```   333   then show ?case by simp
```
```   334 next
```
```   335   case (2 c i P2)
```
```   336   then show ?case
```
```   337     apply (cases P2)
```
```   338     apply simp_all
```
```   339     apply (cases i)
```
```   340     apply (simp_all add: mkPinj_cn)
```
```   341     done
```
```   342 next
```
```   343   case (3 i P2 c)
```
```   344   then show ?case
```
```   345     apply (cases P2)
```
```   346     apply simp_all
```
```   347     apply (cases i)
```
```   348     apply (simp_all add: mkPinj_cn)
```
```   349     done
```
```   350 next
```
```   351   case (4 c P2 i Q2)
```
```   352   then have "isnorm P2" "isnorm Q2"
```
```   353     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   354   with 4 show ?case
```
```   355     apply (cases "c = 0")
```
```   356     apply simp_all
```
```   357     apply (cases "i = 0")
```
```   358     apply (simp_all add: mkPX_cn)
```
```   359     done
```
```   360 next
```
```   361   case (5 P2 i Q2 c)
```
```   362   then have "isnorm P2" "isnorm Q2"
```
```   363     by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
```
```   364   with 5 show ?case
```
```   365     apply (cases "c = 0")
```
```   366     apply simp_all
```
```   367     apply (cases "i = 0")
```
```   368     apply (simp_all add: mkPX_cn)
```
```   369     done
```
```   370 next
```
```   371   case (6 x P2 y Q2)
```
```   372   consider "x < y" | "x = y" | "x > y" by arith
```
```   373   then show ?case
```
```   374   proof cases
```
```   375     case xy: 1
```
```   376     then obtain d where y: "y = d + x"
```
```   377       by atomize_elim arith
```
```   378     from 6 have *: "x > 0"
```
```   379       by (cases x) (auto simp add: norm_Pinj_0_False)
```
```   380     from 6 have **: "isnorm P2" "isnorm Q2"
```
```   381       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   382     from 6 xy y have "isnorm (Pinj d Q2)"
```
```   383       apply (cases d)
```
```   384       apply simp
```
```   385       apply (cases Q2)
```
```   386       apply auto
```
```   387       done
```
```   388     with 6 * ** y show ?thesis
```
```   389       by (simp add: mkPinj_cn)
```
```   390   next
```
```   391     case xy: 2
```
```   392     from 6 have *: "isnorm P2" "isnorm Q2"
```
```   393       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   394     from 6 have **: "y > 0"
```
```   395       by (cases y) (auto simp add: norm_Pinj_0_False)
```
```   396     with 6 xy * ** show ?thesis
```
```   397       by (simp add: mkPinj_cn)
```
```   398   next
```
```   399     case xy: 3
```
```   400     then obtain d where x: "x = d + y"
```
```   401       by atomize_elim arith
```
```   402     from 6 have *: "y > 0"
```
```   403       by (cases y) (auto simp add: norm_Pinj_0_False)
```
```   404     from 6 have **: "isnorm P2" "isnorm Q2"
```
```   405       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
```
```   406     from 6 xy x have "isnorm (Pinj d P2)"
```
```   407       apply (cases d)
```
```   408       apply simp
```
```   409       apply (cases P2)
```
```   410       apply auto
```
```   411       done
```
```   412     with 6 xy * ** x show ?thesis
```
```   413       by (simp add: mkPinj_cn)
```
```   414   qed
```
```   415 next
```
```   416   case (7 x P2 Q2 y R)
```
```   417   then have Y0: "y > 0" by (cases y) auto
```
```   418   consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
```
```   419     by atomize_elim arith
```
```   420   then show ?case
```
```   421   proof cases
```
```   422     case 1
```
```   423     with 7 show ?thesis
```
```   424       by (auto simp add: norm_Pinj_0_False)
```
```   425   next
```
```   426     case x: 2
```
```   427     from 7 have "isnorm R" "isnorm P2"
```
```   428       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   429     with 7 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
```
```   430       by (auto simp add: norm_PX1[of Q2 y R])
```
```   431     with 7 x Y0 show ?thesis
```
```   432       by (simp add: mkPX_cn)
```
```   433   next
```
```   434     case x: 3
```
```   435     from 7 have *: "isnorm R" "isnorm Q2"
```
```   436       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
```
```   437     from 7 x have "isnorm (Pinj (x - 1) P2)"
```
```   438       by (cases P2) auto
```
```   439     with 7 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
```
```   440       by auto
```
```   441     with Y0 x show ?thesis
```
```   442       by (simp add: mkPX_cn)
```
```   443   qed
```
```   444 next
```
```   445   case (8 Q2 y R x P2)
```
```   446   then have Y0: "y > 0"
```
```   447     by (cases y) auto
```
```   448   consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
```
```   449     by atomize_elim arith
```
```   450   then show ?case
```
```   451   proof cases
```
```   452     case 1
```
```   453     with 8 show ?thesis
```
```   454       by (auto simp add: norm_Pinj_0_False)
```
```   455   next
```
```   456     case x: 2
```
```   457     from 8 have "isnorm R" "isnorm P2"
```
```   458       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
```
```   459     with 8 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
```
```   460       by (auto simp add: norm_PX1[of Q2 y R])
```
```   461     with 8 x Y0 show ?thesis
```
```   462       by (simp add: mkPX_cn)
```
```   463   next
```
```   464     case x: 3
```
```   465     from 8 have *: "isnorm R" "isnorm Q2"
```
```   466       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
```
```   467     from 8 x have "isnorm (Pinj (x - 1) P2)"
```
```   468       by (cases P2) auto
```
```   469     with 8 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
```
```   470       by auto
```
```   471     with Y0 x show ?thesis
```
```   472       by (simp add: mkPX_cn)
```
```   473   qed
```
```   474 next
```
```   475   case (9 P1 x P2 Q1 y Q2)
```
```   476   from 9 have X0: "x > 0" by (cases x) auto
```
```   477   from 9 have Y0: "y > 0" by (cases y) auto
```
```   478   from 9 have *: "isnorm P1" "isnorm P2"
```
```   479     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
```
```   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   with 9 * 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
```
```   491     by (simp add: add_cn)
```
```   492 qed
```
```   493
```
```   494 text \<open>neg conserves normalizedness\<close>
```
```   495 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
```
```   496 proof (induct P)
```
```   497   case Pc
```
```   498   then show ?case by simp
```
```   499 next
```
```   500   case (Pinj i P2)
```
```   501   then have "isnorm P2"
```
```   502     by (simp add: norm_Pinj[of i P2])
```
```   503   with Pinj show ?case
```
```   504     by (cases P2) (auto, cases i, auto)
```
```   505 next
```
```   506   case (PX P1 x P2) note PX1 = this
```
```   507   from PX have "isnorm P2" "isnorm P1"
```
```   508     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
```
```   509   with PX show ?case
```
```   510   proof (cases P1)
```
```   511     case (PX p1 y p2)
```
```   512     with PX1 show ?thesis
```
```   513       by (cases x) (auto, cases p2, auto)
```
```   514   next
```
```   515     case Pinj
```
```   516     with PX1 show ?thesis
```
```   517       by (cases x) auto
```
```   518   qed (cases x, auto)
```
```   519 qed
```
```   520
```
```   521 text \<open>sub conserves normalizedness\<close>
```
```   522 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
```
```   523   by (simp add: sub_def add_cn neg_cn)
```
```   524
```
```   525 text \<open>sqr conserves normalizizedness\<close>
```
```   526 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
```
```   527 proof (induct P)
```
```   528   case Pc
```
```   529   then show ?case by simp
```
```   530 next
```
```   531   case (Pinj i Q)
```
```   532   then show ?case
```
```   533     apply (cases Q)
```
```   534     apply (auto simp add: mkPX_cn mkPinj_cn)
```
```   535     apply (cases i)
```
```   536     apply (auto simp add: mkPX_cn mkPinj_cn)
```
```   537     done
```
```   538 next
```
```   539   case (PX P1 x P2)
```
```   540   then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
```
```   541     apply (cases x)
```
```   542     using PX
```
```   543     apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
```
```   544     done
```
```   545   with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
```
```   546     and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
```
```   547     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
```
```   548   then show ?case
```
```   549     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
```
```   550 qed
```
```   551
```
```   552 text \<open>pow conserves normalizedness\<close>
```
```   553 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
```
```   554 proof (induct n arbitrary: P rule: less_induct)
```
```   555   case (less k)
```
```   556   show ?case
```
```   557   proof (cases "k = 0")
```
```   558     case True
```
```   559     then show ?thesis by simp
```
```   560   next
```
```   561     case False
```
```   562     then have K2: "k div 2 < k"
```
```   563       by (cases k) auto
```
```   564     from less have "isnorm (sqr P)"
```
```   565       by (simp add: sqr_cn)
```
```   566     with less False K2 show ?thesis
```
```   567       by (cases "even k") (auto simp add: mul_cn elim: evenE oddE)
```
```   568   qed
```
```   569 qed
```
```   570
```
```   571 end
```