author blanchet Tue, 09 Sep 2014 20:51:36 +0200 changeset 58259 52c35a59bbf5 parent 58258 b66034025548 child 58260 c96e511bfb79
ported Decision_Procs to new datatypes
```--- 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)"```
```--- 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"```
```--- 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
}```
```--- 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)"
```--- 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```
```--- 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 (cases p)
apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
done

@@ -1085,7 +1085,7 @@
apply (cases p)
apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
done

@@ -1093,7 +1093,7 @@
apply (cases p)
apply simp_all
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
done

@@ -1104,9 +1104,9 @@
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 (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 (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 (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 (cases t)
apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
apply auto
done

@@ -1284,7 +1284,7 @@
apply (cases t)
apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
apply auto
done

@@ -1292,7 +1292,7 @@
apply (cases t)
apply auto
-  apply (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
apply auto
done

@@ -1300,7 +1300,7 @@
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 (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
apply auto
done

lemma le_qf[simp]: "qfree (le t)"
apply (cases t)
-  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 (case_tac poly)
+  apply (rename_tac poly, case_tac poly)
apply auto
done
```
```--- 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
```