proper case_names for int_cases, int_of_nat_induct;
authorwenzelm
Wed May 04 15:37:39 2011 +0200 (2011-05-04)
changeset 426768724f20bf69c
parent 42675 223153bb68a1
child 42703 6ab174bfefe2
proper case_names for int_cases, int_of_nat_induct;
tuned some proofs, eliminating (cases, auto) anti-pattern;
src/HOL/Int.thy
src/HOL/Library/Float.thy
src/HOL/Matrix/ComputeFloat.thy
     1.1 --- a/src/HOL/Int.thy	Wed May 04 11:49:46 2011 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed May 04 15:37:39 2011 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4  qed
     1.5  
     1.6  lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
     1.7 -by (induct m, simp_all add: Zero_int_def One_int_def add)
     1.8 +by (induct m) (simp_all add: Zero_int_def One_int_def add)
     1.9  
    1.10  
    1.11  subsection {* The @{text "\<le>"} Ordering *}
    1.12 @@ -219,7 +219,8 @@
    1.13  text{*strict, in 1st argument; proof is by induction on k>0*}
    1.14  lemma zmult_zless_mono2_lemma:
    1.15       "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
    1.16 -apply (induct "k", simp)
    1.17 +apply (induct k)
    1.18 +apply simp
    1.19  apply (simp add: left_distrib)
    1.20  apply (case_tac "k=0")
    1.21  apply (simp_all add: add_strict_mono)
    1.22 @@ -299,10 +300,10 @@
    1.23  by (simp add: of_int One_int_def)
    1.24  
    1.25  lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
    1.26 -by (cases w, cases z, simp add: algebra_simps of_int add)
    1.27 +by (cases w, cases z) (simp add: algebra_simps of_int add)
    1.28  
    1.29  lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
    1.30 -by (cases z, simp add: algebra_simps of_int minus)
    1.31 +by (cases z) (simp add: algebra_simps of_int minus)
    1.32  
    1.33  lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
    1.34  by (simp add: diff_minus Groups.diff_minus)
    1.35 @@ -329,7 +330,8 @@
    1.36  
    1.37  lemma of_int_eq_iff [simp]:
    1.38     "of_int w = of_int z \<longleftrightarrow> w = z"
    1.39 -apply (cases w, cases z, simp add: of_int)
    1.40 +apply (cases w, cases z)
    1.41 +apply (simp add: of_int)
    1.42  apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
    1.43  apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
    1.44  done
    1.45 @@ -353,7 +355,8 @@
    1.46  
    1.47  lemma of_int_le_iff [simp]:
    1.48    "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
    1.49 -  by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
    1.50 +  by (cases w, cases z)
    1.51 +    (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
    1.52  
    1.53  lemma of_int_less_iff [simp]:
    1.54    "of_int w < of_int z \<longleftrightarrow> w < z"
    1.55 @@ -405,13 +408,13 @@
    1.56  by (simp add: Zero_int_def nat)
    1.57  
    1.58  lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
    1.59 -by (cases z, simp add: nat le int_def Zero_int_def)
    1.60 +by (cases z) (simp add: nat le int_def Zero_int_def)
    1.61  
    1.62  corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
    1.63  by simp
    1.64  
    1.65  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
    1.66 -by (cases z, simp add: nat le Zero_int_def)
    1.67 +by (cases z) (simp add: nat le Zero_int_def)
    1.68  
    1.69  lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
    1.70  apply (cases w, cases z) 
    1.71 @@ -437,7 +440,7 @@
    1.72    using assms by (blast dest: nat_0_le sym)
    1.73  
    1.74  lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
    1.75 -by (cases w, simp add: nat le int_def Zero_int_def, arith)
    1.76 +by (cases w) (simp add: nat le int_def Zero_int_def, arith)
    1.77  
    1.78  corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
    1.79  by (simp only: eq_commute [of m] nat_eq_iff)
    1.80 @@ -458,18 +461,18 @@
    1.81  
    1.82  lemma nat_add_distrib:
    1.83       "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
    1.84 -by (cases z, cases z', simp add: nat add le Zero_int_def)
    1.85 +by (cases z, cases z') (simp add: nat add le Zero_int_def)
    1.86  
    1.87  lemma nat_diff_distrib:
    1.88       "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
    1.89 -by (cases z, cases z', 
    1.90 -    simp add: nat add minus diff_minus le Zero_int_def)
    1.91 +by (cases z, cases z')
    1.92 +  (simp add: nat add minus diff_minus le Zero_int_def)
    1.93  
    1.94  lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
    1.95  by (simp add: int_def minus nat Zero_int_def) 
    1.96  
    1.97  lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
    1.98 -by (cases z, simp add: nat less int_def, arith)
    1.99 +by (cases z) (simp add: nat less int_def, arith)
   1.100  
   1.101  context ring_1
   1.102  begin
   1.103 @@ -547,17 +550,18 @@
   1.104  text{*Now we replace the case analysis rule by a more conventional one:
   1.105  whether an integer is negative or not.*}
   1.106  
   1.107 -theorem int_cases [cases type: int, case_names nonneg neg]:
   1.108 +theorem int_cases [case_names nonneg neg, cases type: int]:
   1.109    "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
   1.110 -apply (cases "z < 0", blast dest!: negD)
   1.111 +apply (cases "z < 0")
   1.112 +apply (blast dest!: negD)
   1.113  apply (simp add: linorder_not_less del: of_nat_Suc)
   1.114  apply auto
   1.115  apply (blast dest: nat_0_le [THEN sym])
   1.116  done
   1.117  
   1.118 -theorem int_of_nat_induct [induct type: int, case_names nonneg neg]:
   1.119 +theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
   1.120       "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
   1.121 -  by (cases z rule: int_cases) auto
   1.122 +  by (cases z) auto
   1.123  
   1.124  text{*Contributed by Brian Huffman*}
   1.125  theorem int_diff_cases:
   1.126 @@ -822,7 +826,7 @@
   1.127  
   1.128  lemma odd_less_0_iff:
   1.129    "(1 + z + z < 0) = (z < (0::int))"
   1.130 -proof (cases z rule: int_cases)
   1.131 +proof (cases z)
   1.132    case (nonneg n)
   1.133    thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   1.134                               le_imp_0_less [THEN order_less_imp_le])  
   1.135 @@ -1089,7 +1093,7 @@
   1.136  
   1.137  lemma odd_nonzero:
   1.138    "1 + z + z \<noteq> (0::int)"
   1.139 -proof (cases z rule: int_cases)
   1.140 +proof (cases z)
   1.141    case (nonneg n)
   1.142    have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   1.143    thus ?thesis using  le_imp_0_less [OF le]
   1.144 @@ -1159,14 +1163,16 @@
   1.145  
   1.146  lemma odd_less_0:
   1.147    "(1 + z + z < 0) = (z < (0::int))"
   1.148 -proof (cases z rule: int_cases)
   1.149 +proof (cases z)
   1.150    case (nonneg n)
   1.151 -  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   1.152 -                             le_imp_0_less [THEN order_less_imp_le])  
   1.153 +  then show ?thesis
   1.154 +    by (simp add: linorder_not_less add_assoc add_increasing
   1.155 +      le_imp_0_less [THEN order_less_imp_le])
   1.156  next
   1.157    case (neg n)
   1.158 -  thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
   1.159 -    add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
   1.160 +  then show ?thesis
   1.161 +    by (simp del: of_nat_Suc of_nat_add of_nat_1
   1.162 +      add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
   1.163  qed
   1.164  
   1.165  text {* Less-Than or Equals *}
   1.166 @@ -1709,7 +1715,8 @@
   1.167      step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   1.168    shows "P i"
   1.169  proof -
   1.170 -  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
   1.171 +  { fix n
   1.172 +    have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
   1.173      proof (induct n)
   1.174        case 0
   1.175        hence "i = k" by arith
   1.176 @@ -1720,8 +1727,8 @@
   1.177        moreover
   1.178        have ki1: "k \<le> i - 1" using Suc.prems by arith
   1.179        ultimately
   1.180 -      have "P(i - 1)" by(rule Suc.hyps)
   1.181 -      from step[OF ki1 this] show ?case by simp
   1.182 +      have "P (i - 1)" by (rule Suc.hyps)
   1.183 +      from step [OF ki1 this] show ?case by simp
   1.184      qed
   1.185    }
   1.186    with ge show ?thesis by fast
   1.187 @@ -1739,31 +1746,32 @@
   1.188  apply (rule step, simp+)
   1.189  done
   1.190  
   1.191 -theorem int_le_induct[consumes 1,case_names base step]:
   1.192 +theorem int_le_induct [consumes 1, case_names base step]:
   1.193    assumes le: "i \<le> (k::int)" and
   1.194          base: "P(k)" and
   1.195          step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   1.196    shows "P i"
   1.197  proof -
   1.198 -  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
   1.199 +  { fix n
   1.200 +    have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
   1.201      proof (induct n)
   1.202        case 0
   1.203        hence "i = k" by arith
   1.204        thus "P i" using base by simp
   1.205      next
   1.206        case (Suc n)
   1.207 -      hence "n = nat(k - (i+1))" by arith
   1.208 +      hence "n = nat (k - (i + 1))" by arith
   1.209        moreover
   1.210        have ki1: "i + 1 \<le> k" using Suc.prems by arith
   1.211        ultimately
   1.212 -      have "P(i+1)" by(rule Suc.hyps)
   1.213 +      have "P (i + 1)" by(rule Suc.hyps)
   1.214        from step[OF ki1 this] show ?case by simp
   1.215      qed
   1.216    }
   1.217    with le show ?thesis by fast
   1.218  qed
   1.219  
   1.220 -theorem int_less_induct [consumes 1,case_names base step]:
   1.221 +theorem int_less_induct [consumes 1, case_names base step]:
   1.222    assumes less: "(i::int) < k" and
   1.223          base: "P(k - 1)" and
   1.224          step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   1.225 @@ -1782,11 +1790,14 @@
   1.226    shows "P i"
   1.227  proof -
   1.228    have "i \<le> k \<or> i \<ge> k" by arith
   1.229 -  then show ?thesis proof
   1.230 -    assume "i \<ge> k" then show ?thesis using base
   1.231 +  then show ?thesis
   1.232 +  proof
   1.233 +    assume "i \<ge> k"
   1.234 +    then show ?thesis using base
   1.235        by (rule int_ge_induct) (fact step1)
   1.236    next
   1.237 -    assume "i \<le> k" then show ?thesis using base
   1.238 +    assume "i \<le> k"
   1.239 +    then show ?thesis using base
   1.240        by (rule int_le_induct) (fact step2)
   1.241    qed
   1.242  qed
   1.243 @@ -1797,7 +1808,8 @@
   1.244       "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
   1.245        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
   1.246  unfolding One_nat_def
   1.247 -apply (induct n, simp)
   1.248 +apply (induct n)
   1.249 +apply simp
   1.250  apply (intro strip)
   1.251  apply (erule impE, simp)
   1.252  apply (erule_tac x = n in allE, simp)
   1.253 @@ -2120,11 +2132,14 @@
   1.254    proof -
   1.255      fix k
   1.256      assume A: "int y = int x * k"
   1.257 -    then show "x dvd y" proof (cases k)
   1.258 -      case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
   1.259 +    then show "x dvd y"
   1.260 +    proof (cases k)
   1.261 +      case (nonneg n)
   1.262 +      with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
   1.263        then show ?thesis ..
   1.264      next
   1.265 -      case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
   1.266 +      case (neg n)
   1.267 +      with A have "int y = int x * (- int (Suc n))" by simp
   1.268        also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
   1.269        also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
   1.270        finally have "- int (x * Suc n) = int y" ..
   1.271 @@ -2134,12 +2149,12 @@
   1.272    then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
   1.273  qed
   1.274  
   1.275 -lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   1.276 +lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
   1.277  proof
   1.278    assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   1.279    hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   1.280    hence "nat \<bar>x\<bar> = 1"  by simp
   1.281 -  thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
   1.282 +  thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
   1.283  next
   1.284    assume "\<bar>x\<bar>=1"
   1.285    then have "x = 1 \<or> x = -1" by auto
   1.286 @@ -2150,7 +2165,7 @@
   1.287    assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   1.288  proof
   1.289    assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   1.290 -    by (cases "n >0", auto simp add: minus_equation_iff)
   1.291 +    by (cases "n >0") (auto simp add: minus_equation_iff)
   1.292  next
   1.293    assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   1.294    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
   1.295 @@ -2174,9 +2189,9 @@
   1.296    by (induct n) (simp_all add: nat_mult_distrib)
   1.297  
   1.298  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   1.299 -  apply (rule_tac z=n in int_cases)
   1.300 +  apply (cases n)
   1.301    apply (auto simp add: dvd_int_iff)
   1.302 -  apply (rule_tac z=z in int_cases)
   1.303 +  apply (cases z)
   1.304    apply (auto simp add: dvd_imp_le)
   1.305    done
   1.306  
   1.307 @@ -2186,7 +2201,8 @@
   1.308    shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
   1.309  proof -
   1.310    from assms obtain k where "d = a * k" by (rule dvdE)
   1.311 -  show ?thesis proof
   1.312 +  show ?thesis
   1.313 +  proof
   1.314      assume "a dvd (x + t)"
   1.315      then obtain l where "x + t = a * l" by (rule dvdE)
   1.316      then have "x = a * l - t" by simp
     2.1 --- a/src/HOL/Library/Float.thy	Wed May 04 11:49:46 2011 +0200
     2.2 +++ b/src/HOL/Library/Float.thy	Wed May 04 15:37:39 2011 +0200
     2.3 @@ -85,10 +85,10 @@
     2.4      by (auto simp add: h)
     2.5    show ?thesis
     2.6    proof (induct a)
     2.7 -    case (1 n)
     2.8 +    case (nonneg n)
     2.9      from pos show ?case by (simp add: algebra_simps)
    2.10    next
    2.11 -    case (2 n)
    2.12 +    case (neg n)
    2.13      show ?case
    2.14        apply (auto)
    2.15        apply (subst pow2_neg[of "- int n"])
    2.16 @@ -100,7 +100,7 @@
    2.17  
    2.18  lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
    2.19  proof (induct b)
    2.20 -  case (1 n)
    2.21 +  case (nonneg n)
    2.22    show ?case
    2.23    proof (induct n)
    2.24      case 0
    2.25 @@ -110,7 +110,7 @@
    2.26      then show ?case by (auto simp add: algebra_simps pow2_add1)
    2.27    qed
    2.28  next
    2.29 -  case (2 n)
    2.30 +  case (neg n)
    2.31    show ?case
    2.32    proof (induct n)
    2.33      case 0
     3.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Wed May 04 11:49:46 2011 +0200
     3.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Wed May 04 15:37:39 2011 +0200
     3.3 @@ -35,10 +35,10 @@
     3.4      by (auto simp add: h)
     3.5    show ?thesis
     3.6    proof (induct a)
     3.7 -    case (1 n)
     3.8 +    case (nonneg n)
     3.9      from pos show ?case by (simp add: algebra_simps)
    3.10    next
    3.11 -    case (2 n)
    3.12 +    case (neg n)
    3.13      show ?case
    3.14        apply (auto)
    3.15        apply (subst pow2_neg[of "- int n"])
    3.16 @@ -50,17 +50,17 @@
    3.17  
    3.18  lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
    3.19  proof (induct b)
    3.20 -  case (1 n)
    3.21 +  case (nonneg n)
    3.22    show ?case
    3.23    proof (induct n)
    3.24      case 0
    3.25      show ?case by simp
    3.26    next
    3.27      case (Suc m)
    3.28 -    show ?case by (auto simp add: algebra_simps pow2_add1 1 Suc)
    3.29 +    show ?case by (auto simp add: algebra_simps pow2_add1 nonneg Suc)
    3.30    qed
    3.31  next
    3.32 -  case (2 n)
    3.33 +  case (neg n)
    3.34    show ?case
    3.35    proof (induct n)
    3.36      case 0