src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58259 52c35a59bbf5
child 58710 7216a10d69ba
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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 (rename_tac pol2, 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 (rename_tac pol2, 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 (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
    58   apply (rename_tac pol a, 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, rename_tac pol2, 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, rename_tac pol2, 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