# HG changeset patch
# User wenzelm
# Date 1393533118 -3600
# Node ID 52c8f934ea6f31c6bcc56e9edfb07be8144e78ce
# Parent  687240115804c0cdc88d691ef3862986ff9768a0
tuned whitespace;
tuned proofs;

diff -r 687240115804 -r 52c8f934ea6f src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Feb 27 21:27:58 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Feb 27 21:31:58 2014 +0100
@@ -143,7 +143,7 @@
 | "pow n P =
     (if even n then pow (n div 2) (sqr P)
      else P \<otimes> pow (n div 2) (sqr P))"
-  
+
 lemma pow_if:
   "pow n P =
    (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
diff -r 687240115804 -r 52c8f934ea6f src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Thu Feb 27 21:27:58 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Thu Feb 27 21:31:58 2014 +0100
@@ -59,9 +59,9 @@
   apply (case_tac y, auto)
   done
 
-lemma norm_PXtrans: 
+lemma norm_PXtrans:
   assumes A: "isnorm (PX P x Q)"
-    and "isnorm Q2" 
+    and "isnorm Q2"
   shows "isnorm (PX P x Q2)"
 proof (cases P)
   case (PX p1 y p2)
@@ -78,31 +78,34 @@
   case Pinj
   with assms show ?thesis by (cases x) auto
 qed
- 
-lemma norm_PXtrans2:
-  assumes "isnorm (PX P x Q)" and "isnorm Q2"
-  shows "isnorm (PX P (Suc (n + x)) Q2)"
-proof (cases P)
-  case (PX p1 y p2)
-  with assms show ?thesis
-    apply (cases x)
-    apply auto
-    apply (cases p2)
-    apply auto
-    done
-next
-  case Pc
-  with assms show ?thesis by (cases x) auto
-next
-  case Pinj
-  with assms show ?thesis by (cases x) auto
-qed
 
+lemma norm_PXtrans2:
+  assumes "isnorm (PX P x Q)"
+    and "isnorm Q2"
+  shows "isnorm (PX P (Suc (n + x)) Q2)"
+proof (cases P)
+  case (PX p1 y p2)
+  with assms show ?thesis
+    apply (cases x)
+    apply auto
+    apply (cases p2)
+    apply auto
+    done
+next
+  case Pc
+  with assms show ?thesis
+    by (cases x) auto
+next
+  case Pinj
+  with assms show ?thesis
+    by (cases x) auto
+qed
+
 text {* mkPX conserves normalizedness (@{text "_cn"}) *}
-lemma mkPX_cn: 
+lemma mkPX_cn:
   assumes "x \<noteq> 0"
     and "isnorm P"
-    and "isnorm Q" 
+    and "isnorm Q"
   shows "isnorm (mkPX P x Q)"
 proof (cases P)
   case (Pc c)
@@ -114,7 +117,8 @@
     by (cases x) (auto simp add: mkPinj_cn mkPX_def)
 next
   case (PX P1 y P2)
-  with assms have Y0: "y > 0" by (cases y) auto
+  with assms have Y0: "y > 0"
+    by (cases y) auto
   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
@@ -125,10 +129,12 @@
 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
 proof (induct P Q rule: add.induct)
   case (2 c i P2)
-  then show ?case by (cases P2) (simp_all, cases i, simp_all)
+  then show ?case
+    by (cases P2) (simp_all, cases i, simp_all)
 next
   case (3 i P2 c)
-  then show ?case by (cases P2) (simp_all, cases i, simp_all)
+  then show ?case
+    by (cases P2) (simp_all, cases i, simp_all)
 next
   case (4 c P2 i Q2)
   then have "isnorm P2" "isnorm Q2"
@@ -143,11 +149,13 @@
     by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
 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)
+  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"
+  moreover {
+    assume "x < y"
     then have "\<exists>d. y = d + x" by arith
     then obtain d where y: "y = d + x" ..
     moreover
@@ -158,18 +166,22 @@
     moreover
     from 6 `x < y` 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"
+    ultimately have ?case by (simp add: mkPinj_cn)
+  }
+  moreover {
+    assume "x = y"
     moreover
     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"..
+    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
@@ -178,111 +190,150 @@
     moreover
     from 6 `x > y` x have "isnorm (Pinj d P2)"
       by (cases d) (simp, cases P2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn) }
+    ultimately have ?case by (simp add: mkPinj_cn)
+  }
   ultimately show ?case by blast
 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"
+  moreover {
+    assume "x = 0"
+    with 7 have ?case by (auto simp add: norm_Pinj_0_False)
+  }
+  moreover {
+    assume "x = 1"
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
     with 7 `x = 1` have ?case
-      by (simp add: norm_PXtrans[of Q2 y _]) }
-  moreover
-  { assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
+      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)" ..
     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 `isnorm (PX Q2 y R)` X have ?case
-      by (simp add: norm_PXtrans[of Q2 y _]) }
+      by (simp add: norm_PXtrans[of Q2 y _])
+  }
   ultimately show ?case by blast
 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 by (auto simp add: norm_Pinj_0_False) }
-  moreover
-  { assume "x = 1"
-    with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
-    with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
-  moreover
-  { assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
+  moreover {
+    assume "x = 0"
+    with 8 have ?case
+      by (auto simp add: norm_Pinj_0_False)
+  }
+  moreover {
+    assume "x = 1"
+    with 8 have "isnorm R" "isnorm P2"
+      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 8 `x = 1` have "isnorm (R \<oplus> P2)"
+      by simp
+    with 8 `x = 1` have ?case
+      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)" ..
     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)" by (cases P2) auto
-    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
-    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
+    with 8 X have "isnorm (Pinj (x - 1) P2)"
+      by (cases P2) auto
+    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+      by simp
+    with `isnorm (PX Q2 y R)` X have ?case
+      by (simp add: norm_PXtrans[of Q2 y _])
+  }
   ultimately show ?case by blast
 next
   case (9 P1 x P2 Q1 y Q2)
-  then have Y0: "y>0" by (cases y) auto
-  with 9 have X0: "x>0" by (cases x) auto
+  then have Y0: "y > 0" by (cases y) auto
+  with 9 have X0: "x > 0" by (cases x) auto
   with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
     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
+  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
-    have "isnorm (PX P1 d (Pc 0))" 
+    have "isnorm (PX P1 d (Pc 0))"
     proof (cases P1)
       case (PX p1 y p2)
-      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
+      with 9 sm1 sm2 show ?thesis
+        by (cases d) (simp, cases p2, auto)
     next
-      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
+      case Pc
+      with 9 sm1 sm2 show ?thesis
+        by (cases d) auto
     next
-      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
+      case Pinj
+      with 9 sm1 sm2 show ?thesis
+        by (cases d) auto
     qed
-    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
-    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
-  moreover
-  { assume "x = y"
-    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
-    with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
-  moreover
-  { assume sm1: "x < y" then have "\<exists>d. y = d + x" by arith
+    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
+      by auto
+    with Y0 sm1 sm2 have ?case
+      by (simp add: mkPX_cn)
+  }
+  moreover {
+    assume "x = y"
+    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
+      by auto
+    with `x = y` Y0 have ?case
+      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
-    have "isnorm (PX Q1 d (Pc 0))" 
+    have "isnorm (PX Q1 d (Pc 0))"
     proof (cases Q1)
       case (PX p1 y p2)
-      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
+      with 9 sm1 sm2 show ?thesis
+        by (cases d) (simp, cases p2, auto)
     next
-      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
+      case Pc
+      with 9 sm1 sm2 show ?thesis
+        by (cases d) auto
     next
-      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
+      case Pinj
+      with 9 sm1 sm2 show ?thesis
+        by (cases d) auto
     qed
-    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
-    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
+    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
+      by auto
+    with X0 sm1 sm2 have ?case
+      by (simp add: mkPX_cn)
+  }
   ultimately show ?case by blast
 qed simp
 
 text {* mul concerves normalizedness *}
 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
 proof (induct P Q rule: mul.induct)
-  case (2 c i P2) then show ?case 
+  case (2 c i P2)
+  then show ?case
     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
 next
-  case (3 i P2 c) then show ?case 
+  case (3 i P2 c)
+  then show ?case
     by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
 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 
+  with 4 show ?case
     by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
 next
   case (5 P2 i Q2 c)
@@ -293,89 +344,129 @@
 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
+  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" by (cases x) (auto simp add: norm_Pinj_0_False)
+    from 6 have "x > 0"
+      by (cases x) (auto simp add: norm_Pinj_0_False)
     moreover
-    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2"
+      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x < y` 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"
+    from 6 `x < y` 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" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    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" by (cases y) (auto simp add: norm_Pinj_0_False)
+    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
+    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)
+    from 6 have "y > 0"
+      by (cases y) (auto simp add: norm_Pinj_0_False)
     moreover
-    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
+    from 6 have "isnorm P2" "isnorm Q2"
+      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
-    ultimately have ?case by (simp add: mkPinj_cn) }
+    from 6 `x > y` 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
 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 by (auto simp add: norm_Pinj_0_False) }
-  moreover
-  { assume "x = 1"
-    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
-    with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
-  moreover
-  { assume "x > 1" then have "\<exists>d. x = Suc (Suc d)" by arith
+  moreover {
+    assume "x = 0"
+    with 7 have ?case
+      by (auto simp add: norm_Pinj_0_False)
+  }
+  moreover {
+    assume "x = 1"
+    from 7 have "isnorm R" "isnorm P2"
+      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
+      by (auto simp add: norm_PX1[of Q2 y R])
+    with 7 `x = 1` Y0 have ?case
+      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"
       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
+    from 7 X have "isnorm (Pinj (x - 1) P2)"
+      by (cases P2) auto
     moreover
-    from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
+    from 7 have "isnorm (Pinj x P2)"
+      by (cases P2) auto
     moreover
     note 7 X
-    ultimately 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 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
 next
   case (8 Q2 y R x P2)
-  then have Y0: "y > 0" by (cases y) auto
+  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 by (auto simp add: norm_Pinj_0_False) }
-  moreover
-  { assume "x = 1"
-    from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
-    with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
-  moreover
-  { assume "x > 1" then have "\<exists>d. x = Suc (Suc d)" by arith
+  moreover {
+    assume "x = 0"
+    with 8 have ?case
+      by (auto simp add: norm_Pinj_0_False)
+  }
+  moreover {
+    assume "x = 1"
+    from 8 have "isnorm R" "isnorm P2"
+      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
+    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
+      by (auto simp add: norm_PX1[of Q2 y R])
+    with 8 `x = 1` Y0 have ?case
+      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"
       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
+    from 8 X have "isnorm (Pinj (x - 1) P2)"
+      by (cases P2) auto
     moreover
-    from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
+    from 8 X have "isnorm (Pinj x P2)"
+      by (cases P2) auto
     moreover
     note 8 X
-    ultimately 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 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
 next
   case (9 P1 x P2 Q1 y Q2)
@@ -383,16 +474,18 @@
   from 9 have Y0: "y > 0" by (cases y) auto
   note 9
   moreover
-  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])
+  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)"
-    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" 
+    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
     by (auto simp add: mkPinj_cn)
   with 9 X0 Y0 have
     "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
-    "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"  
-    "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" 
+    "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
@@ -401,8 +494,10 @@
 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
 proof (induct P)
   case (Pinj i P2)
-  then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
-  with Pinj show ?case by (cases P2) (auto, cases i, auto)
+  then have "isnorm P2"
+    by (simp add: norm_Pinj[of i P2])
+  with Pinj show ?case
+    by (cases P2) (auto, cases i, auto)
 next
   case (PX P1 x P2) note PX1 = this
   from PX have "isnorm P2" "isnorm P1"
@@ -410,10 +505,12 @@
   with PX show ?case
   proof (cases P1)
     case (PX p1 y p2)
-    with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
+    with PX1 show ?thesis
+      by (cases x) (auto, cases p2, auto)
   next
     case Pinj
-    with PX1 show ?thesis by (cases x) auto
+    with PX1 show ?thesis
+      by (cases x) auto
   qed (cases x, auto)
 qed simp
 
@@ -430,21 +527,22 @@
   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)
-next 
+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])
   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))"
     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)
+  then show ?case
+    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
 qed
 
 text {* pow conserves normalizedness *}
 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
 proof (induct n arbitrary: P rule: less_induct)
   case (less k)
-  show ?case 
+  show ?case
   proof (cases "k = 0")
     case True
     then show ?thesis by simp
diff -r 687240115804 -r 52c8f934ea6f src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Feb 27 21:27:58 2014 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Feb 27 21:31:58 2014 +0100
@@ -22,31 +22,40 @@
 fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
 
 (* pol *)
-fun pol_Pc t = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
-fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
-fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
+fun pol_Pc t =
+  Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
+fun pol_Pinj t =
+  Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
+fun pol_PX t =
+  Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
 
 (* polex *)
-fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
-fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
-fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
-fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
-fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
-fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
+fun polex_add t =
+  Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
+fun polex_sub t =
+  Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
+fun polex_mul t =
+  Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
+fun polex_neg t =
+  Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
+fun polex_pol t =
+  Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
+fun polex_pow t =
+  Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
 
 (* reification of polynoms : primitive cring expressions *)
 fun reif_pol T vs (t as Free _) =
       let
         val one = @{term "1::nat"};
         val i = find_index (fn t' => t' = t) vs
-      in if i = 0
-        then pol_PX T $ (pol_Pc T $ cring_one T)
-          $ one $ (pol_Pc T $ cring_zero T)
-        else pol_Pinj T $ HOLogic.mk_nat i
-          $ (pol_PX T $ (pol_Pc T $ cring_one T)
-            $ one $ (pol_Pc T $ cring_zero T))
+      in
+        if i = 0 then
+          pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)
+        else
+          pol_Pinj T $ HOLogic.mk_nat i $
+            (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T))
         end
-  | reif_pol T vs t = pol_Pc T $ t;
+  | reif_pol T _ t = pol_Pc T $ t;
 
 (* reification of polynom expressions *)
 fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
@@ -62,34 +71,33 @@
   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
 
 (* reification of the equation *)
-val cr_sort = @{sort "comm_ring_1"};
+val cr_sort = @{sort comm_ring_1};
 
-fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
-      if Sign.of_sort thy (T, cr_sort) then
+fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
+      if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
         let
+          val thy = Proof_Context.theory_of ctxt;
           val fs = Misc_Legacy.term_frees eq;
           val cvs = cterm_of thy (HOLogic.mk_list T fs);
           val clhs = cterm_of thy (reif_polex T fs lhs);
           val crhs = cterm_of thy (reif_polex T fs rhs);
           val ca = ctyp_of thy T;
         in (ca, cvs, clhs, crhs) end
-      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
+      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
   | reif_eq _ _ = error "reif_eq: not an equation";
 
 (* The cring tactic *)
 (* Attention: You have to make sure that no t^0 is in the goal!! *)
 (* Use simply rewriting t^0 = 1 *)
 val cring_simps =
-  [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
-    @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
+  @{thms mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]};
 
 fun tac ctxt = SUBGOAL (fn (g, i) =>
   let
-    val thy = Proof_Context.theory_of ctxt;
     val cring_ctxt = ctxt addsimps cring_simps;  (*FIXME really the full simpset!?*)
-    val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
+    val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
     val norm_eq_th =
-      simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
+      simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
   in
     cut_tac norm_eq_th i
     THEN (simp_tac cring_ctxt i)