author wenzelm Sat, 20 Jun 2015 17:29:51 +0200 changeset 60535 25a3c522cc8f parent 60534 b2add2b08412 child 60536 00db0d934a7d
tuned proofs;
```--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sat Jun 20 16:42:15 2015 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sat Jun 20 17:29:51 2015 +0200
@@ -73,10 +73,12 @@
done
next
case Pc
-  with assms show ?thesis by (cases x) auto
+  with assms show ?thesis
+    by (cases x) auto
next
case Pinj
-  with assms show ?thesis by (cases x) auto
+  with assms show ?thesis
+    by (cases x) auto
qed

lemma norm_PXtrans2:
@@ -122,134 +124,149 @@
from assms PX have "isnorm P1" "isnorm P2"
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
from assms PX Y0 show ?thesis
-    by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
+    apply (cases x)
+    apply (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _])
+    apply (cases P2)
+    apply auto
+    done
qed

lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
proof (induct P Q rule: add.induct)
+  case 1
+  then show ?case by simp
+next
case (2 c i P2)
then show ?case
-    by (cases P2) (simp_all, cases i, simp_all)
+    apply (cases P2)
+    apply simp_all
+    apply (cases i)
+    apply simp_all
+    done
next
case (3 i P2 c)
then show ?case
-    by (cases P2) (simp_all, cases i, simp_all)
+    apply (cases P2)
+    apply simp_all
+    apply (cases i)
+    apply simp_all
+    done
next
case (4 c P2 i Q2)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 4 show ?case
-    by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
+    apply (cases i)
+    apply simp
+    apply (cases P2)
+    apply auto
+    apply (rename_tac pol2, case_tac pol2)
+    apply auto
+    done
next
case (5 P2 i Q2 c)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 5 show ?case
-    by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
+    apply (cases i)
+    apply simp
+    apply (cases P2)
+    apply auto
+    apply (rename_tac pol2, case_tac pol2)
+    apply auto
+    done
next
case (6 x P2 y Q2)
then have Y0: "y > 0"
by (cases y) (auto simp add: norm_Pinj_0_False)
with 6 have X0: "x > 0"
by (cases x) (auto simp add: norm_Pinj_0_False)
-  have "x < y \<or> x = y \<or> x > y" by arith
-  moreover {
-    assume "x < y"
-    then have "\<exists>d. y = d + x" by arith
-    then obtain d where y: "y = d + x" ..
-    moreover
-    note 6 X0
-    moreover
-    from 6 have "isnorm P2" "isnorm Q2"
+  consider "x < y" | "x = y" | "x > y" by arith
+  then show ?case
+  proof cases
+    case 1
+    then obtain d where y: "y = d + x"
+      by atomize_elim arith
+    from 6 have *: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    moreover
-    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
+    from 6 1 y have "isnorm (Pinj d Q2)"
by (cases d, simp, cases Q2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn)
-  }
-  moreover {
-    assume "x = y"
-    moreover
+    with 6 X0 y * show ?thesis
+  next
+    case 2
from 6 have "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    moreover
-    note 6 Y0
-    ultimately have ?case by (simp add: mkPinj_cn)
-  }
-  moreover {
-    assume "x > y"
-    then have "\<exists>d. x = d + y"
-      by arith
-    then obtain d where x: "x = d + y" ..
-    moreover
-    note 6 Y0
-    moreover
-    from 6 have "isnorm P2" "isnorm Q2"
+    with 2 6 Y0 show ?thesis
+  next
+    case 3
+    then obtain d where x: "x = d + y"
+      by atomize_elim arith
+    from 6 have *: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    moreover
-    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
+    from 6 3 x have "isnorm (Pinj d P2)"
by (cases d) (simp, cases P2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn)
-  }
-  ultimately show ?case by blast
+    with 3 6 Y0 * x show ?thesis by (simp add: mkPinj_cn)
+  qed
next
case (7 x P2 Q2 y R)
-  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
-  moreover {
-    assume "x = 0"
-    with 7 have ?case by (auto simp add: norm_Pinj_0_False)
-  }
-  moreover {
-    assume "x = 1"
+  consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
+    by atomize_elim arith
+  then show ?case
+  proof cases
+    case 1
+    with 7 show ?thesis
+      by (auto simp add: norm_Pinj_0_False)
+  next
+    case 2
from 7 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)" by simp
-    with 7 \<open>x = 1\<close> have ?case
+    with 7 2 have "isnorm (R \<oplus> P2)"
+      by simp
+    with 7 2 show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
-  }
-  moreover {
-    assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
-    then obtain d where X: "x=Suc (Suc d)" ..
+  next
+    case 3
with 7 have NR: "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
-    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
-    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
+    with 7 3 have "isnorm (Pinj (x - 1) P2)"
+      by (cases P2) auto
+    with 7 3 NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+      by simp
+    with \<open>isnorm (PX Q2 y R)\<close> 3 show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
-  }
-  ultimately show ?case by blast
+  qed
next
case (8 Q2 y R x P2)
-  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
-  moreover {
-    assume "x = 0"
-    with 8 have ?case
+  consider "x = 0" | "x = 1" | "x > 1"
+    by arith
+  then show ?case
+  proof cases
+    case 1
+    with 8 show ?thesis
-  }
-  moreover {
-    assume "x = 1"
+  next
+    case 2
with 8 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)"
+    with 8 2 have "isnorm (R \<oplus> P2)"
by simp
-    with 8 \<open>x = 1\<close> have ?case
+    with 8 2 show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
-  }
-  moreover {
-    assume "x > 1"
-    then have "\<exists>d. x = Suc (Suc d)" by arith
-    then obtain d where X: "x = Suc (Suc d)" ..
+  next
+    case 3
+    then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith
with 8 have NR: "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 X have "isnorm (Pinj (x - 1) P2)"
+    with 8 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
-    with 8 \<open>x > 1\<close> NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 8 3 NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
by simp
-    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
+    with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
-  }
-  ultimately show ?case by blast
+  qed
next
case (9 P1 x P2 Q1 y Q2)
then have Y0: "y > 0" by (cases y) auto
@@ -258,228 +275,215 @@
by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
-  have "y < x \<or> x = y \<or> x < y" by arith
-  moreover {
-    assume sm1: "y < x"
-    then have "\<exists>d. x = d + y" by arith
-    then obtain d where sm2: "x = d + y" ..
-    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
-    moreover
+  consider "y < x" | "x = y" | "x < y" by arith
+  then show ?case
+  proof cases
+    case 1
+    then obtain d where x: "x = d + y"
+      by atomize_elim arith
have "isnorm (PX P1 d (Pc 0))"
proof (cases P1)
case (PX p1 y p2)
-      with 9 sm1 sm2 show ?thesis
+      with 9 1 x show ?thesis
by (cases d) (simp, cases p2, auto)
next
case Pc
-      with 9 sm1 sm2 show ?thesis
+      with 9 1 x show ?thesis
by (cases d) auto
next
case Pinj
-      with 9 sm1 sm2 show ?thesis
+      with 9 1 x show ?thesis
by (cases d) auto
qed
-    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
+    with 9 NQ1 NP1 NP2 NQ2 1 x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
by auto
-    with Y0 sm1 sm2 have ?case
+    with Y0 1 x show ?thesis
-  }
-  moreover {
-    assume "x = y"
+  next
+    case 2
with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
by auto
-    with \<open>x = y\<close> Y0 have ?case
+    with 2 Y0 show ?thesis
-  }
-  moreover {
-    assume sm1: "x < y"
-    then have "\<exists>d. y = d + x" by arith
-    then obtain d where sm2: "y = d + x" ..
-    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
-    moreover
+  next
+    case 3
+    then obtain d where y: "y = d + x"
+      by atomize_elim arith
have "isnorm (PX Q1 d (Pc 0))"
proof (cases Q1)
case (PX p1 y p2)
-      with 9 sm1 sm2 show ?thesis
+      with 9 3 y show ?thesis
by (cases d) (simp, cases p2, auto)
next
case Pc
-      with 9 sm1 sm2 show ?thesis
+      with 9 3 y show ?thesis
by (cases d) auto
next
case Pinj
-      with 9 sm1 sm2 show ?thesis
+      with 9 3 y show ?thesis
by (cases d) auto
qed
-    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
+    with 9 NQ1 NP1 NP2 NQ2 3 y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
by auto
-    with X0 sm1 sm2 have ?case
+    with X0 3 y show ?thesis
-  }
-  ultimately show ?case by blast
-qed simp
+  qed
+qed

text \<open>mul concerves normalizedness\<close>
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
proof (induct P Q rule: mul.induct)
+  case 1
+  then show ?case by simp
+next
case (2 c i P2)
then show ?case
-    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
+    apply (cases P2)
+    apply simp_all
+    apply (cases i)
+    done
next
case (3 i P2 c)
then show ?case
-    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
+    apply (cases P2)
+    apply simp_all
+    apply (cases i)
+    done
next
case (4 c P2 i Q2)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 4 show ?case
-    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
+    apply (cases "c = 0")
+    apply simp_all
+    apply (cases "i = 0")
+    done
next
case (5 P2 i Q2 c)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 5 show ?case
-    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
+    apply (cases "c = 0")
+    apply simp_all
+    apply (cases "i = 0")
+    done
next
case (6 x P2 y Q2)
-  have "x < y \<or> x = y \<or> x > y" by arith
-  moreover {
-    assume "x < y"
-    then have "\<exists>d. y = d + x" by arith
-    then obtain d where y: "y = d + x" ..
-    moreover
-    note 6
-    moreover
-    from 6 have "x > 0"
+  consider "x < y" | "x = y" | "x > y" by arith
+  then show ?case
+  proof cases
+    case 1
+    then obtain d where y: "y = d + x"
+      by atomize_elim arith
+    from 6 have *: "x > 0"
by (cases x) (auto simp add: norm_Pinj_0_False)
-    moreover
-    from 6 have "isnorm P2" "isnorm Q2"
+    from 6 have **: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    moreover
-    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
-      by (cases d) (simp, cases Q2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn)
-  }
-  moreover {
-    assume "x = y"
-    moreover
-    from 6 have "isnorm P2" "isnorm Q2"
+    from 6 1 y have "isnorm (Pinj d Q2)"
+      apply (cases d)
+      apply simp
+      apply (cases Q2)
+      apply auto
+      done
+    with 6 * ** y show ?thesis
+  next
+    case 2
+    from 6 have *: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    moreover
-    from 6 have "y>0"
+    from 6 have **: "y > 0"
+      by (cases y) (auto simp add: norm_Pinj_0_False)
+    with 6 2 * **show ?thesis
+  next
+    case 3
+    then obtain d where x: "x = d + y"
+      by atomize_elim arith
+    from 6 have *: "y > 0"
by (cases y) (auto simp add: norm_Pinj_0_False)
-    moreover
-    note 6
-    ultimately have ?case by (simp add: mkPinj_cn)
-  }
-  moreover {
-    assume "x > y"
-    then have "\<exists>d. x = d + y" by arith
-    then obtain d where x: "x = d + y" ..
-    moreover
-    note 6
-    moreover
-    from 6 have "y > 0"
-      by (cases y) (auto simp add: norm_Pinj_0_False)
-    moreover
-    from 6 have "isnorm P2" "isnorm Q2"
+    from 6 have **: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
-    moreover
-    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
-      by (cases d) (simp, cases P2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn)
-  }
-  ultimately show ?case by blast
+    from 6 3 x have "isnorm (Pinj d P2)"
+      apply (cases d)
+      apply simp
+      apply (cases P2)
+      apply auto
+      done
+    with 6 3 * ** x show ?thesis
+  qed
next
case (7 x P2 Q2 y R)
then have Y0: "y > 0" by (cases y) auto
-  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
-  moreover {
-    assume "x = 0"
-    with 7 have ?case
+  consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
+    by atomize_elim arith
+  then show ?case
+  proof cases
+    case 1
+    with 7 show ?thesis
-  }
-  moreover {
-    assume "x = 1"
+  next
+    case 2
from 7 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 7 2 have "isnorm (R \<otimes> P2)" "isnorm Q2"
by (auto simp add: norm_PX1[of Q2 y R])
-    with 7 \<open>x = 1\<close> Y0 have ?case
+    with 7 2 Y0 show ?thesis
-  }
-  moreover {
-    assume "x > 1"
-    then have "\<exists>d. x = Suc (Suc d)"
-      by arith
-    then obtain d where X: "x = Suc (Suc d)" ..
-    from 7 have NR: "isnorm R" "isnorm Q2"
+  next
+    case 3
+    from 7 have *: "isnorm R" "isnorm Q2"
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
-    moreover
-    from 7 X have "isnorm (Pinj (x - 1) P2)"
-      by (cases P2) auto
-    moreover
-    from 7 have "isnorm (Pinj x P2)"
+    from 7 3 have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
-    moreover
-    note 7 X
-    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+    with 7 3 * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
by auto
-    with Y0 X have ?case
+    with Y0 3 show ?thesis
-  }
-  ultimately show ?case by blast
+  qed
next
case (8 Q2 y R x P2)
then have Y0: "y > 0"
by (cases y) auto
-  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
-  moreover {
-    assume "x = 0"
-    with 8 have ?case
+  consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
+    by atomize_elim arith
+  then show ?case
+  proof cases
+    case 1
+    with 8 show ?thesis
-  }
-  moreover {
-    assume "x = 1"
+  next
+    case 2
from 8 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 8 2 have "isnorm (R \<otimes> P2)" "isnorm Q2"
by (auto simp add: norm_PX1[of Q2 y R])
-    with 8 \<open>x = 1\<close> Y0 have ?case
+    with 8 2 Y0 show ?thesis
-  }
-  moreover {
-    assume "x > 1"
-    then have "\<exists>d. x = Suc (Suc d)" by arith
-    then obtain d where X: "x = Suc (Suc d)" ..
-    from 8 have NR: "isnorm R" "isnorm Q2"
+  next
+    case 3
+    from 8 have *: "isnorm R" "isnorm Q2"
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
-    moreover
-    from 8 X have "isnorm (Pinj (x - 1) P2)"
-      by (cases P2) auto
-    moreover
-    from 8 X have "isnorm (Pinj x P2)"
+    from 8 3 have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
-    moreover
-    note 8 X
-    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+    with 8 3 * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
by auto
-    with Y0 X have ?case by (simp add: mkPX_cn)
-  }
-  ultimately show ?case by blast
+    with Y0 3 show ?thesis
+  qed
next
case (9 P1 x P2 Q1 y Q2)
from 9 have X0: "x > 0" by (cases x) auto
from 9 have Y0: "y > 0" by (cases y) auto
-  note 9
-  moreover
-  from 9 have "isnorm P1" "isnorm P2"
+  from 9 have *: "isnorm P1" "isnorm P2"
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
-  moreover
from 9 have "isnorm Q1" "isnorm Q2"
by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
-  ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
+  with 9 * have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
"isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
with 9 X0 Y0 have
@@ -487,12 +491,16 @@
"isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
"isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
-qed simp
+  then show ?case
+qed

text \<open>neg conserves normalizedness\<close>
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
proof (induct P)
+  case Pc
+  then show ?case by simp
+next
case (Pinj i P2)
then have "isnorm P2"
by (simp add: norm_Pinj[of i P2])
@@ -512,7 +520,7 @@
with PX1 show ?thesis
by (cases x) auto
qed (cases x, auto)
-qed simp
+qed

text \<open>sub conserves normalizedness\<close>
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
@@ -526,13 +534,20 @@
next
case (Pinj i Q)
then show ?case
-    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
+    apply (cases Q)
+    apply (auto simp add: mkPX_cn mkPinj_cn)
+    apply (cases i)
+    apply (auto simp add: mkPX_cn mkPinj_cn)
+    done
next
case (PX P1 x P2)
then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
-    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
+    apply (cases x)
+    using PX
+    apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
+    done
with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
-      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
+    and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
then show ?case