--- 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
text \<open>add conserves normalizedness\<close>
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
+ by (simp add: mkPinj_cn)
+ 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
+ by (simp add: mkPinj_cn)
+ 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
by (auto simp add: norm_Pinj_0_False)
- }
- 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
by (simp add: mkPX_cn)
- }
- 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
by (simp add: mkPX_cn)
- }
- 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
by (simp add: mkPX_cn)
- }
- 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)
+ apply (simp_all add: mkPinj_cn)
+ 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)
+ apply (simp_all add: mkPinj_cn)
+ 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")
+ apply (simp_all add: mkPX_cn)
+ 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")
+ apply (simp_all add: mkPX_cn)
+ 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
+ by (simp add: mkPinj_cn)
+ 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
+ by (simp add: mkPinj_cn)
+ 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
+ by (simp add: mkPinj_cn)
+ 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
by (auto simp add: norm_Pinj_0_False)
- }
- 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
by (simp add: mkPX_cn)
- }
- 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
by (simp add: mkPX_cn)
- }
- 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
by (auto simp add: norm_Pinj_0_False)
- }
- 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
by (simp add: mkPX_cn)
- }
- 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
+ by (simp add: mkPX_cn)
+ 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)"
by (auto simp add: mkPinj_cn)
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))"
by (auto simp add: mkPX_cn)
- then show ?case by (simp add: add_cn)
-qed simp
+ then show ?case
+ by (simp add: add_cn)
+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))"
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
then show ?case
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
@@ -548,8 +563,10 @@
then show ?thesis by simp
next
case False
- then have K2: "k div 2 < k" by (cases k) auto
- from less have "isnorm (sqr P)" by (simp add: sqr_cn)
+ then have K2: "k div 2 < k"
+ by (cases k) auto
+ from less have "isnorm (sqr P)"
+ by (simp add: sqr_cn)
with less False K2 show ?thesis
by (cases "even k") (auto simp add: mul_cn elim: evenE oddE)
qed