# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 52c35a59bbf53d67e80ca34cf8451dfb6f34f768
# Parent  b6603402554862ba8315137ba5a6b9996eaf9b63
ported Decision_Procs to new datatypes

diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -60,6 +60,9 @@
 
 text {* Defining the basic ring operations on normalized polynomials *}
 
+lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
+  by (cases p) simp_all
+
 function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<oplus>" 65)
 where
   "Pc a \<oplus> Pc b = Pc (a + b)"
diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -39,7 +39,7 @@
   apply auto
   apply (cases P)
   apply auto
-  apply (case_tac pol2)
+  apply (rename_tac pol2, case_tac pol2)
   apply auto
   done
 
@@ -48,14 +48,14 @@
   apply auto
   apply (cases P)
   apply auto
-  apply (case_tac pol2)
+  apply (rename_tac pol2, case_tac pol2)
   apply auto
   done
 
 lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
   apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
-  apply (case_tac nat, auto simp add: norm_Pinj_0_False)
-  apply (case_tac pol, auto)
+  apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
+  apply (rename_tac pol a, case_tac pol, auto)
   apply (case_tac y, auto)
   done
 
@@ -140,13 +140,13 @@
   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, case_tac pol2, auto)
+    by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
 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, case_tac pol2, auto)
+    by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
 next
   case (6 x P2 y Q2)
   then have Y0: "y > 0"
diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -276,7 +276,7 @@
   using assms
   apply (induct a)
   apply simp_all
-  apply (case_tac nat)
+  apply (rename_tac nat a b, case_tac nat)
   apply simp_all
   done
 
@@ -1126,7 +1126,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
 next
@@ -1143,7 +1143,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
 next
@@ -1160,7 +1160,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
 next
@@ -1177,7 +1177,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
 next
@@ -1194,7 +1194,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
 next
@@ -1211,7 +1211,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
 next
@@ -1242,7 +1242,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
   }
@@ -1292,7 +1292,7 @@
     apply (auto simp add: Let_def split_def algebra_simps)
     apply (cases "?r")
     apply auto
-    apply (case_tac nat)
+    apply (rename_tac nat a b, case_tac nat)
     apply auto
     done
   }
diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -978,27 +978,27 @@
 
 lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) = Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) = Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) = Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) = Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) = Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma conj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
 by (auto simp add: conj_def)
diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -1722,7 +1722,7 @@
   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
   moreover
   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
-      by (cases "?r", simp_all add: Let_def split_def,case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def,rename_tac nat a b,case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1747,7 +1747,7 @@
   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
   moreover
   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat",simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat",simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1772,7 +1772,7 @@
   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
   moreover
   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1797,7 +1797,7 @@
   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
   moreover
   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1822,7 +1822,7 @@
   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
   moreover
   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Eq a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1847,7 +1847,7 @@
   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
   moreover
   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (NEq a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1876,7 +1876,7 @@
   moreover
   {assume "?c=0" and "j\<noteq>0" hence ?case 
       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -1922,7 +1922,7 @@
   moreover
   {assume "?c=0" and "j\<noteq>0" hence ?case 
       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
-      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
+      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
   moreover
   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
@@ -3714,7 +3714,7 @@
 
 lemma lt_l: "isrlfm (rsplit lt a)"
   by (rule rsplit_l[where f="lt" and a="a"], auto simp add: lt_def,
-    case_tac s, simp_all, case_tac "nat", simp_all)
+    case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
 
 lemma le_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (le n s) = Ifm (x#bs) (Le a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (le n s) = ?I (Le a)")
 proof(clarify)
@@ -3726,7 +3726,7 @@
 
 lemma le_l: "isrlfm (rsplit le a)"
   by (rule rsplit_l[where f="le" and a="a"], auto simp add: le_def) 
-(case_tac s, simp_all, case_tac "nat",simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac "nat",simp_all)
 
 lemma gt_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (gt n s) = Ifm (x#bs) (Gt a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (gt n s) = ?I (Gt a)")
 proof(clarify)
@@ -3737,7 +3737,7 @@
 qed
 lemma gt_l: "isrlfm (rsplit gt a)"
   by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def) 
-(case_tac s, simp_all, case_tac "nat", simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
 
 lemma ge_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (ge n s) = Ifm (x#bs) (Ge a)" (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (ge n s) = ?I (Ge a)")
 proof(clarify)
@@ -3748,7 +3748,7 @@
 qed
 lemma ge_l: "isrlfm (rsplit ge a)"
   by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def) 
-(case_tac s, simp_all, case_tac "nat", simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
 
 lemma eq_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (eq n s) = Ifm (x#bs) (Eq a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (eq n s) = ?I (Eq a)")
 proof(clarify)
@@ -3758,7 +3758,7 @@
 qed
 lemma eq_l: "isrlfm (rsplit eq a)"
   by (rule rsplit_l[where f="eq" and a="a"], auto simp add: eq_def) 
-(case_tac s, simp_all, case_tac"nat", simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac"nat", simp_all)
 
 lemma neq_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (neq n s) = Ifm (x#bs) (NEq a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (neq n s) = ?I (NEq a)")
 proof(clarify)
@@ -3769,7 +3769,7 @@
 
 lemma neq_l: "isrlfm (rsplit neq a)"
   by (rule rsplit_l[where f="neq" and a="a"], auto simp add: neq_def) 
-(case_tac s, simp_all, case_tac"nat", simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac"nat", simp_all)
 
 lemma small_le: 
   assumes u0:"0 \<le> u" and u1: "u < 1"
@@ -3928,11 +3928,11 @@
 
 lemma DVD_l: "isrlfm (rsplit (DVD i) a)"
   by (rule rsplit_l[where f="DVD i" and a="a"], auto simp add: DVD_def eq_def DVDJ_l) 
-(case_tac s, simp_all, case_tac "nat", simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
 
 lemma NDVD_l: "isrlfm (rsplit (NDVD i) a)"
   by (rule rsplit_l[where f="NDVD i" and a="a"], auto simp add: NDVD_def neq_def NDVDJ_l) 
-(case_tac s, simp_all, case_tac "nat", simp_all)
+(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
 
 consts rlfm :: "fm \<Rightarrow> fm"
 recdef rlfm "measure fmsize"
@@ -3972,7 +3972,7 @@
 proof (induct p)
   case (Lt a) 
   hence "bound0 (Lt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
-    by (cases a,simp_all, case_tac "nat", simp_all)
+    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   moreover
   {assume "bound0 (Lt a)" hence bn:"bound0 (simpfm (Lt a))"  
       using simpfm_bound0 by blast
@@ -3996,7 +3996,7 @@
 next
   case (Le a)   
   hence "bound0 (Le a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
-    by (cases a,simp_all, case_tac "nat", simp_all)
+    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   moreover
   { assume "bound0 (Le a)" hence bn:"bound0 (simpfm (Le a))"  
       using simpfm_bound0 by blast
@@ -4020,7 +4020,7 @@
 next
   case (Gt a)   
   hence "bound0 (Gt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
-    by (cases a,simp_all, case_tac "nat", simp_all)
+    by (cases a, simp_all, rename_tac nat a b,case_tac "nat", simp_all)
   moreover
   {assume "bound0 (Gt a)" hence bn:"bound0 (simpfm (Gt a))"  
       using simpfm_bound0 by blast
@@ -4044,7 +4044,7 @@
 next
   case (Ge a)   
   hence "bound0 (Ge a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
-    by (cases a,simp_all, case_tac "nat", simp_all)
+    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   moreover
   { assume "bound0 (Ge a)" hence bn:"bound0 (simpfm (Ge a))"  
       using simpfm_bound0 by blast
@@ -4068,7 +4068,7 @@
 next
   case (Eq a)   
   hence "bound0 (Eq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
-    by (cases a,simp_all, case_tac "nat", simp_all)
+    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   moreover
   { assume "bound0 (Eq a)" hence bn:"bound0 (simpfm (Eq a))"  
       using simpfm_bound0 by blast
@@ -4092,7 +4092,7 @@
 next
   case (NEq a)  
   hence "bound0 (NEq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
-    by (cases a,simp_all, case_tac "nat", simp_all)
+    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   moreover
   {assume "bound0 (NEq a)" hence bn:"bound0 (simpfm (NEq a))"  
       using simpfm_bound0 by blast
diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -1066,7 +1066,7 @@
     and "islin (Le p)"
     and "islin (Eq p)"
     and "islin (NEq p)"
-  using nb by (cases p, auto, case_tac nat, auto)+
+  using nb by (cases p, auto, rename_tac nat a b, case_tac nat, auto)+
 
 definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
 definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
@@ -1077,7 +1077,7 @@
   apply (simp add: lt_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply (simp_all add: isnpoly_def)
   done
 
@@ -1085,7 +1085,7 @@
   apply (simp add: le_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply (simp_all add: isnpoly_def)
   done
 
@@ -1093,7 +1093,7 @@
   apply (simp add: eq_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply (simp_all add: isnpoly_def)
   done
 
@@ -1104,9 +1104,9 @@
   apply (simp add: lt_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply simp_all
-  apply (case_tac nat)
+  apply (rename_tac nat a b, case_tac nat)
   apply simp_all
   done
 
@@ -1114,9 +1114,9 @@
   apply (simp add: le_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply simp_all
-  apply (case_tac nat)
+  apply (rename_tac nat a b, case_tac nat)
   apply simp_all
   done
 
@@ -1124,9 +1124,9 @@
   apply (simp add: eq_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply simp_all
-  apply (case_tac nat)
+  apply (rename_tac nat a b, case_tac nat)
   apply simp_all
   done
 
@@ -1134,9 +1134,9 @@
   apply (simp add: neq_def eq_def)
   apply (cases p)
   apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply simp_all
-  apply (case_tac nat)
+  apply (rename_tac nat a b, case_tac nat)
   apply simp_all
   done
 
@@ -1276,7 +1276,7 @@
   apply (simp add: lt_def)
   apply (cases t)
   apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
@@ -1284,7 +1284,7 @@
   apply (simp add: le_def)
   apply (cases t)
   apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
@@ -1292,7 +1292,7 @@
   apply (simp add: eq_def)
   apply (cases t)
   apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
@@ -1300,7 +1300,7 @@
   apply (simp add: neq_def eq_def)
   apply (cases t)
   apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
@@ -1533,21 +1533,21 @@
 lemma lt_qf[simp]: "qfree (lt t)"
   apply (cases t)
   apply (auto simp add: lt_def)
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
 lemma le_qf[simp]: "qfree (le t)"
   apply (cases t)
   apply (auto simp add: le_def)
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
 lemma eq_qf[simp]: "qfree (eq t)"
   apply (cases t)
   apply (auto simp add: eq_def)
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -930,7 +930,7 @@
   apply (induct p arbitrary: n0)
   apply auto
   apply atomize
-  apply (erule_tac x = "Suc nat" in allE)
+  apply (rename_tac nat a b, erule_tac x = "Suc nat" in allE)
   apply auto
   done
 
@@ -1056,7 +1056,7 @@
 lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
   apply (cases p)
   apply auto
-  apply (case_tac "nat")
+  apply (rename_tac nat a, case_tac "nat")
   apply simp_all
   done
 
@@ -1144,7 +1144,7 @@
   unfolding polypoly_def
   apply (cases p)
   apply auto
-  apply (case_tac nat)
+  apply (rename_tac nat a, case_tac nat)
   apply auto
   done
 
@@ -2009,7 +2009,7 @@
   unfolding isnonconstant_def
   apply (cases p)
   apply simp_all
-  apply (case_tac nat)
+  apply (rename_tac nat a, case_tac nat)
   apply auto
   done