ported Decision_Procs to new datatypes
authorblanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 5825952c35a59bbf5
parent 58258 b66034025548
child 58260 c96e511bfb79
ported Decision_Procs to new datatypes
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -60,6 +60,9 @@
     1.4  
     1.5  text {* Defining the basic ring operations on normalized polynomials *}
     1.6  
     1.7 +lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
     1.8 +  by (cases p) simp_all
     1.9 +
    1.10  function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<oplus>" 65)
    1.11  where
    1.12    "Pc a \<oplus> Pc b = Pc (a + b)"
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Tue Sep 09 20:51:36 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Tue Sep 09 20:51:36 2014 +0200
     2.3 @@ -39,7 +39,7 @@
     2.4    apply auto
     2.5    apply (cases P)
     2.6    apply auto
     2.7 -  apply (case_tac pol2)
     2.8 +  apply (rename_tac pol2, case_tac pol2)
     2.9    apply auto
    2.10    done
    2.11  
    2.12 @@ -48,14 +48,14 @@
    2.13    apply auto
    2.14    apply (cases P)
    2.15    apply auto
    2.16 -  apply (case_tac pol2)
    2.17 +  apply (rename_tac pol2, case_tac pol2)
    2.18    apply auto
    2.19    done
    2.20  
    2.21  lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
    2.22    apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
    2.23 -  apply (case_tac nat, auto simp add: norm_Pinj_0_False)
    2.24 -  apply (case_tac pol, auto)
    2.25 +  apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
    2.26 +  apply (rename_tac pol a, case_tac pol, auto)
    2.27    apply (case_tac y, auto)
    2.28    done
    2.29  
    2.30 @@ -140,13 +140,13 @@
    2.31    then have "isnorm P2" "isnorm Q2"
    2.32      by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
    2.33    with 4 show ?case
    2.34 -    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
    2.35 +    by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
    2.36  next
    2.37    case (5 P2 i Q2 c)
    2.38    then have "isnorm P2" "isnorm Q2"
    2.39      by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
    2.40    with 5 show ?case
    2.41 -    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
    2.42 +    by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)
    2.43  next
    2.44    case (6 x P2 y Q2)
    2.45    then have Y0: "y > 0"
     3.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Tue Sep 09 20:51:36 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Sep 09 20:51:36 2014 +0200
     3.3 @@ -276,7 +276,7 @@
     3.4    using assms
     3.5    apply (induct a)
     3.6    apply simp_all
     3.7 -  apply (case_tac nat)
     3.8 +  apply (rename_tac nat a b, case_tac nat)
     3.9    apply simp_all
    3.10    done
    3.11  
    3.12 @@ -1126,7 +1126,7 @@
    3.13      apply (auto simp add: Let_def split_def algebra_simps)
    3.14      apply (cases "?r")
    3.15      apply auto
    3.16 -    apply (case_tac nat)
    3.17 +    apply (rename_tac nat a b, case_tac nat)
    3.18      apply auto
    3.19      done
    3.20  next
    3.21 @@ -1143,7 +1143,7 @@
    3.22      apply (auto simp add: Let_def split_def algebra_simps)
    3.23      apply (cases "?r")
    3.24      apply auto
    3.25 -    apply (case_tac nat)
    3.26 +    apply (rename_tac nat a b, case_tac nat)
    3.27      apply auto
    3.28      done
    3.29  next
    3.30 @@ -1160,7 +1160,7 @@
    3.31      apply (auto simp add: Let_def split_def algebra_simps)
    3.32      apply (cases "?r")
    3.33      apply auto
    3.34 -    apply (case_tac nat)
    3.35 +    apply (rename_tac nat a b, case_tac nat)
    3.36      apply auto
    3.37      done
    3.38  next
    3.39 @@ -1177,7 +1177,7 @@
    3.40      apply (auto simp add: Let_def split_def algebra_simps)
    3.41      apply (cases "?r")
    3.42      apply auto
    3.43 -    apply (case_tac nat)
    3.44 +    apply (rename_tac nat a b, case_tac nat)
    3.45      apply auto
    3.46      done
    3.47  next
    3.48 @@ -1194,7 +1194,7 @@
    3.49      apply (auto simp add: Let_def split_def algebra_simps)
    3.50      apply (cases "?r")
    3.51      apply auto
    3.52 -    apply (case_tac nat)
    3.53 +    apply (rename_tac nat a b, case_tac nat)
    3.54      apply auto
    3.55      done
    3.56  next
    3.57 @@ -1211,7 +1211,7 @@
    3.58      apply (auto simp add: Let_def split_def algebra_simps)
    3.59      apply (cases "?r")
    3.60      apply auto
    3.61 -    apply (case_tac nat)
    3.62 +    apply (rename_tac nat a b, case_tac nat)
    3.63      apply auto
    3.64      done
    3.65  next
    3.66 @@ -1242,7 +1242,7 @@
    3.67      apply (auto simp add: Let_def split_def algebra_simps)
    3.68      apply (cases "?r")
    3.69      apply auto
    3.70 -    apply (case_tac nat)
    3.71 +    apply (rename_tac nat a b, case_tac nat)
    3.72      apply auto
    3.73      done
    3.74    }
    3.75 @@ -1292,7 +1292,7 @@
    3.76      apply (auto simp add: Let_def split_def algebra_simps)
    3.77      apply (cases "?r")
    3.78      apply auto
    3.79 -    apply (case_tac nat)
    3.80 +    apply (rename_tac nat a b, case_tac nat)
    3.81      apply auto
    3.82      done
    3.83    }
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
     4.3 @@ -978,27 +978,27 @@
     4.4  
     4.5  lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"
     4.6  using rsplit0[where bs = "bs" and t="t"]
     4.7 -by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
     4.8 +by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
     4.9  
    4.10  lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) = Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"
    4.11  using rsplit0[where bs = "bs" and t="t"]
    4.12 -by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
    4.13 +by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
    4.14  
    4.15  lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) = Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"
    4.16  using rsplit0[where bs = "bs" and t="t"]
    4.17 -by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
    4.18 +by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
    4.19  
    4.20  lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) = Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"
    4.21  using rsplit0[where bs = "bs" and t="t"]
    4.22 -by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
    4.23 +by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
    4.24  
    4.25  lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) = Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"
    4.26  using rsplit0[where bs = "bs" and t="t"]
    4.27 -by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
    4.28 +by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
    4.29  
    4.30  lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) = Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"
    4.31  using rsplit0[where bs = "bs" and t="t"]
    4.32 -by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
    4.33 +by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
    4.34  
    4.35  lemma conj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
    4.36  by (auto simp add: conj_def)
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Sep 09 20:51:36 2014 +0200
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Sep 09 20:51:36 2014 +0200
     5.3 @@ -1722,7 +1722,7 @@
     5.4    have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
     5.5    moreover
     5.6    {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
     5.7 -      by (cases "?r", simp_all add: Let_def split_def,case_tac "nat", simp_all)}
     5.8 +      by (cases "?r", simp_all add: Let_def split_def,rename_tac nat a b,case_tac "nat", simp_all)}
     5.9    moreover
    5.10    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
    5.11        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.12 @@ -1747,7 +1747,7 @@
    5.13    have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
    5.14    moreover
    5.15    {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
    5.16 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat",simp_all)}
    5.17 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat",simp_all)}
    5.18    moreover
    5.19    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
    5.20        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.21 @@ -1772,7 +1772,7 @@
    5.22    have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
    5.23    moreover
    5.24    {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
    5.25 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
    5.26 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
    5.27    moreover
    5.28    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
    5.29        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.30 @@ -1797,7 +1797,7 @@
    5.31    have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
    5.32    moreover
    5.33    {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
    5.34 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
    5.35 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
    5.36    moreover
    5.37    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
    5.38        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.39 @@ -1822,7 +1822,7 @@
    5.40    have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
    5.41    moreover
    5.42    {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
    5.43 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
    5.44 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
    5.45    moreover
    5.46    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Eq a))" 
    5.47        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.48 @@ -1847,7 +1847,7 @@
    5.49    have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith
    5.50    moreover
    5.51    {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 
    5.52 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
    5.53 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
    5.54    moreover
    5.55    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (NEq a))" 
    5.56        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.57 @@ -1876,7 +1876,7 @@
    5.58    moreover
    5.59    {assume "?c=0" and "j\<noteq>0" hence ?case 
    5.60        using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
    5.61 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
    5.62 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
    5.63    moreover
    5.64    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    5.65        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.66 @@ -1922,7 +1922,7 @@
    5.67    moreover
    5.68    {assume "?c=0" and "j\<noteq>0" hence ?case 
    5.69        using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]
    5.70 -      by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}
    5.71 +      by (cases "?r", simp_all add: Let_def split_def, rename_tac nat a b, case_tac "nat", simp_all)}
    5.72    moreover
    5.73    {assume cp: "?c > 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))" 
    5.74        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    5.75 @@ -3714,7 +3714,7 @@
    5.76  
    5.77  lemma lt_l: "isrlfm (rsplit lt a)"
    5.78    by (rule rsplit_l[where f="lt" and a="a"], auto simp add: lt_def,
    5.79 -    case_tac s, simp_all, case_tac "nat", simp_all)
    5.80 +    case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
    5.81  
    5.82  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)")
    5.83  proof(clarify)
    5.84 @@ -3726,7 +3726,7 @@
    5.85  
    5.86  lemma le_l: "isrlfm (rsplit le a)"
    5.87    by (rule rsplit_l[where f="le" and a="a"], auto simp add: le_def) 
    5.88 -(case_tac s, simp_all, case_tac "nat",simp_all)
    5.89 +(case_tac s, simp_all, rename_tac nat a b, case_tac "nat",simp_all)
    5.90  
    5.91  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)")
    5.92  proof(clarify)
    5.93 @@ -3737,7 +3737,7 @@
    5.94  qed
    5.95  lemma gt_l: "isrlfm (rsplit gt a)"
    5.96    by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def) 
    5.97 -(case_tac s, simp_all, case_tac "nat", simp_all)
    5.98 +(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
    5.99  
   5.100  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)")
   5.101  proof(clarify)
   5.102 @@ -3748,7 +3748,7 @@
   5.103  qed
   5.104  lemma ge_l: "isrlfm (rsplit ge a)"
   5.105    by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def) 
   5.106 -(case_tac s, simp_all, case_tac "nat", simp_all)
   5.107 +(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.108  
   5.109  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)")
   5.110  proof(clarify)
   5.111 @@ -3758,7 +3758,7 @@
   5.112  qed
   5.113  lemma eq_l: "isrlfm (rsplit eq a)"
   5.114    by (rule rsplit_l[where f="eq" and a="a"], auto simp add: eq_def) 
   5.115 -(case_tac s, simp_all, case_tac"nat", simp_all)
   5.116 +(case_tac s, simp_all, rename_tac nat a b, case_tac"nat", simp_all)
   5.117  
   5.118  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)")
   5.119  proof(clarify)
   5.120 @@ -3769,7 +3769,7 @@
   5.121  
   5.122  lemma neq_l: "isrlfm (rsplit neq a)"
   5.123    by (rule rsplit_l[where f="neq" and a="a"], auto simp add: neq_def) 
   5.124 -(case_tac s, simp_all, case_tac"nat", simp_all)
   5.125 +(case_tac s, simp_all, rename_tac nat a b, case_tac"nat", simp_all)
   5.126  
   5.127  lemma small_le: 
   5.128    assumes u0:"0 \<le> u" and u1: "u < 1"
   5.129 @@ -3928,11 +3928,11 @@
   5.130  
   5.131  lemma DVD_l: "isrlfm (rsplit (DVD i) a)"
   5.132    by (rule rsplit_l[where f="DVD i" and a="a"], auto simp add: DVD_def eq_def DVDJ_l) 
   5.133 -(case_tac s, simp_all, case_tac "nat", simp_all)
   5.134 +(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.135  
   5.136  lemma NDVD_l: "isrlfm (rsplit (NDVD i) a)"
   5.137    by (rule rsplit_l[where f="NDVD i" and a="a"], auto simp add: NDVD_def neq_def NDVDJ_l) 
   5.138 -(case_tac s, simp_all, case_tac "nat", simp_all)
   5.139 +(case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.140  
   5.141  consts rlfm :: "fm \<Rightarrow> fm"
   5.142  recdef rlfm "measure fmsize"
   5.143 @@ -3972,7 +3972,7 @@
   5.144  proof (induct p)
   5.145    case (Lt a) 
   5.146    hence "bound0 (Lt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
   5.147 -    by (cases a,simp_all, case_tac "nat", simp_all)
   5.148 +    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.149    moreover
   5.150    {assume "bound0 (Lt a)" hence bn:"bound0 (simpfm (Lt a))"  
   5.151        using simpfm_bound0 by blast
   5.152 @@ -3996,7 +3996,7 @@
   5.153  next
   5.154    case (Le a)   
   5.155    hence "bound0 (Le a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
   5.156 -    by (cases a,simp_all, case_tac "nat", simp_all)
   5.157 +    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.158    moreover
   5.159    { assume "bound0 (Le a)" hence bn:"bound0 (simpfm (Le a))"  
   5.160        using simpfm_bound0 by blast
   5.161 @@ -4020,7 +4020,7 @@
   5.162  next
   5.163    case (Gt a)   
   5.164    hence "bound0 (Gt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
   5.165 -    by (cases a,simp_all, case_tac "nat", simp_all)
   5.166 +    by (cases a, simp_all, rename_tac nat a b,case_tac "nat", simp_all)
   5.167    moreover
   5.168    {assume "bound0 (Gt a)" hence bn:"bound0 (simpfm (Gt a))"  
   5.169        using simpfm_bound0 by blast
   5.170 @@ -4044,7 +4044,7 @@
   5.171  next
   5.172    case (Ge a)   
   5.173    hence "bound0 (Ge a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
   5.174 -    by (cases a,simp_all, case_tac "nat", simp_all)
   5.175 +    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.176    moreover
   5.177    { assume "bound0 (Ge a)" hence bn:"bound0 (simpfm (Ge a))"  
   5.178        using simpfm_bound0 by blast
   5.179 @@ -4068,7 +4068,7 @@
   5.180  next
   5.181    case (Eq a)   
   5.182    hence "bound0 (Eq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
   5.183 -    by (cases a,simp_all, case_tac "nat", simp_all)
   5.184 +    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.185    moreover
   5.186    { assume "bound0 (Eq a)" hence bn:"bound0 (simpfm (Eq a))"  
   5.187        using simpfm_bound0 by blast
   5.188 @@ -4092,7 +4092,7 @@
   5.189  next
   5.190    case (NEq a)  
   5.191    hence "bound0 (NEq a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
   5.192 -    by (cases a,simp_all, case_tac "nat", simp_all)
   5.193 +    by (cases a,simp_all, rename_tac nat a b, case_tac "nat", simp_all)
   5.194    moreover
   5.195    {assume "bound0 (NEq a)" hence bn:"bound0 (simpfm (NEq a))"  
   5.196        using simpfm_bound0 by blast
     6.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 09 20:51:36 2014 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 09 20:51:36 2014 +0200
     6.3 @@ -1066,7 +1066,7 @@
     6.4      and "islin (Le p)"
     6.5      and "islin (Eq p)"
     6.6      and "islin (NEq p)"
     6.7 -  using nb by (cases p, auto, case_tac nat, auto)+
     6.8 +  using nb by (cases p, auto, rename_tac nat a b, case_tac nat, auto)+
     6.9  
    6.10  definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
    6.11  definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
    6.12 @@ -1077,7 +1077,7 @@
    6.13    apply (simp add: lt_def)
    6.14    apply (cases p)
    6.15    apply simp_all
    6.16 -  apply (case_tac poly)
    6.17 +  apply (rename_tac poly, case_tac poly)
    6.18    apply (simp_all add: isnpoly_def)
    6.19    done
    6.20  
    6.21 @@ -1085,7 +1085,7 @@
    6.22    apply (simp add: le_def)
    6.23    apply (cases p)
    6.24    apply simp_all
    6.25 -  apply (case_tac poly)
    6.26 +  apply (rename_tac poly, case_tac poly)
    6.27    apply (simp_all add: isnpoly_def)
    6.28    done
    6.29  
    6.30 @@ -1093,7 +1093,7 @@
    6.31    apply (simp add: eq_def)
    6.32    apply (cases p)
    6.33    apply simp_all
    6.34 -  apply (case_tac poly)
    6.35 +  apply (rename_tac poly, case_tac poly)
    6.36    apply (simp_all add: isnpoly_def)
    6.37    done
    6.38  
    6.39 @@ -1104,9 +1104,9 @@
    6.40    apply (simp add: lt_def)
    6.41    apply (cases p)
    6.42    apply simp_all
    6.43 -  apply (case_tac poly)
    6.44 +  apply (rename_tac poly, case_tac poly)
    6.45    apply simp_all
    6.46 -  apply (case_tac nat)
    6.47 +  apply (rename_tac nat a b, case_tac nat)
    6.48    apply simp_all
    6.49    done
    6.50  
    6.51 @@ -1114,9 +1114,9 @@
    6.52    apply (simp add: le_def)
    6.53    apply (cases p)
    6.54    apply simp_all
    6.55 -  apply (case_tac poly)
    6.56 +  apply (rename_tac poly, case_tac poly)
    6.57    apply simp_all
    6.58 -  apply (case_tac nat)
    6.59 +  apply (rename_tac nat a b, case_tac nat)
    6.60    apply simp_all
    6.61    done
    6.62  
    6.63 @@ -1124,9 +1124,9 @@
    6.64    apply (simp add: eq_def)
    6.65    apply (cases p)
    6.66    apply simp_all
    6.67 -  apply (case_tac poly)
    6.68 +  apply (rename_tac poly, case_tac poly)
    6.69    apply simp_all
    6.70 -  apply (case_tac nat)
    6.71 +  apply (rename_tac nat a b, case_tac nat)
    6.72    apply simp_all
    6.73    done
    6.74  
    6.75 @@ -1134,9 +1134,9 @@
    6.76    apply (simp add: neq_def eq_def)
    6.77    apply (cases p)
    6.78    apply simp_all
    6.79 -  apply (case_tac poly)
    6.80 +  apply (rename_tac poly, case_tac poly)
    6.81    apply simp_all
    6.82 -  apply (case_tac nat)
    6.83 +  apply (rename_tac nat a b, case_tac nat)
    6.84    apply simp_all
    6.85    done
    6.86  
    6.87 @@ -1276,7 +1276,7 @@
    6.88    apply (simp add: lt_def)
    6.89    apply (cases t)
    6.90    apply auto
    6.91 -  apply (case_tac poly)
    6.92 +  apply (rename_tac poly, case_tac poly)
    6.93    apply auto
    6.94    done
    6.95  
    6.96 @@ -1284,7 +1284,7 @@
    6.97    apply (simp add: le_def)
    6.98    apply (cases t)
    6.99    apply auto
   6.100 -  apply (case_tac poly)
   6.101 +  apply (rename_tac poly, case_tac poly)
   6.102    apply auto
   6.103    done
   6.104  
   6.105 @@ -1292,7 +1292,7 @@
   6.106    apply (simp add: eq_def)
   6.107    apply (cases t)
   6.108    apply auto
   6.109 -  apply (case_tac poly)
   6.110 +  apply (rename_tac poly, case_tac poly)
   6.111    apply auto
   6.112    done
   6.113  
   6.114 @@ -1300,7 +1300,7 @@
   6.115    apply (simp add: neq_def eq_def)
   6.116    apply (cases t)
   6.117    apply auto
   6.118 -  apply (case_tac poly)
   6.119 +  apply (rename_tac poly, case_tac poly)
   6.120    apply auto
   6.121    done
   6.122  
   6.123 @@ -1533,21 +1533,21 @@
   6.124  lemma lt_qf[simp]: "qfree (lt t)"
   6.125    apply (cases t)
   6.126    apply (auto simp add: lt_def)
   6.127 -  apply (case_tac poly)
   6.128 +  apply (rename_tac poly, case_tac poly)
   6.129    apply auto
   6.130    done
   6.131  
   6.132  lemma le_qf[simp]: "qfree (le t)"
   6.133    apply (cases t)
   6.134    apply (auto simp add: le_def)
   6.135 -  apply (case_tac poly)
   6.136 +  apply (rename_tac poly, case_tac poly)
   6.137    apply auto
   6.138    done
   6.139  
   6.140  lemma eq_qf[simp]: "qfree (eq t)"
   6.141    apply (cases t)
   6.142    apply (auto simp add: eq_def)
   6.143 -  apply (case_tac poly)
   6.144 +  apply (rename_tac poly, case_tac poly)
   6.145    apply auto
   6.146    done
   6.147  
     7.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
     7.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
     7.3 @@ -930,7 +930,7 @@
     7.4    apply (induct p arbitrary: n0)
     7.5    apply auto
     7.6    apply atomize
     7.7 -  apply (erule_tac x = "Suc nat" in allE)
     7.8 +  apply (rename_tac nat a b, erule_tac x = "Suc nat" in allE)
     7.9    apply auto
    7.10    done
    7.11  
    7.12 @@ -1056,7 +1056,7 @@
    7.13  lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
    7.14    apply (cases p)
    7.15    apply auto
    7.16 -  apply (case_tac "nat")
    7.17 +  apply (rename_tac nat a, case_tac "nat")
    7.18    apply simp_all
    7.19    done
    7.20  
    7.21 @@ -1144,7 +1144,7 @@
    7.22    unfolding polypoly_def
    7.23    apply (cases p)
    7.24    apply auto
    7.25 -  apply (case_tac nat)
    7.26 +  apply (rename_tac nat a, case_tac nat)
    7.27    apply auto
    7.28    done
    7.29  
    7.30 @@ -2009,7 +2009,7 @@
    7.31    unfolding isnonconstant_def
    7.32    apply (cases p)
    7.33    apply simp_all
    7.34 -  apply (case_tac nat)
    7.35 +  apply (rename_tac nat a, case_tac nat)
    7.36    apply auto
    7.37    done
    7.38