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