# HG changeset patch
# User wenzelm
# Date 1434814191 -7200
# Node ID 25a3c522cc8f65805a129feec90ef4b1932f9d60
# Parent  b2add2b08412b50f9a1d98622ef30a784db8fcf2
tuned proofs;

diff -r b2add2b08412 -r 25a3c522cc8f src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- 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