tuned proofs;
authorwenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988e4b69e10b990
parent 47987 4e9df6ffcc6e
child 47989 1e790c27162d
tuned proofs;
src/HOL/Hilbert_Choice.thy
src/HOL/Nat.thy
src/HOL/Nitpick.thy
src/HOL/Product_Type.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu May 24 17:05:30 2012 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu May 24 17:25:53 2012 +0200
     1.3 @@ -443,7 +443,7 @@
     1.4    have "h ` A = B"
     1.5    proof safe
     1.6      fix a assume "a \<in> A"
     1.7 -    thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto)
     1.8 +    thus "h a \<in> B" using SUB1 2 3 by (cases "a \<in> A'") auto
     1.9    next
    1.10      fix b assume *: "b \<in> B"
    1.11      show "b \<in> h ` A"
     2.1 --- a/src/HOL/Nat.thy	Thu May 24 17:05:30 2012 +0200
     2.2 +++ b/src/HOL/Nat.thy	Thu May 24 17:25:53 2012 +0200
     2.3 @@ -820,12 +820,12 @@
     2.4  
     2.5  lemma Least_Suc:
     2.6       "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
     2.7 -  apply (case_tac "n", auto)
     2.8 +  apply (cases n, auto)
     2.9    apply (frule LeastI)
    2.10    apply (drule_tac P = "%x. P (Suc x) " in LeastI)
    2.11    apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
    2.12    apply (erule_tac [2] Least_le)
    2.13 -  apply (case_tac "LEAST x. P x", auto)
    2.14 +  apply (cases "LEAST x. P x", auto)
    2.15    apply (drule_tac P = "%x. P (Suc x) " in Least_le)
    2.16    apply (blast intro: order_antisym)
    2.17    done
    2.18 @@ -911,7 +911,7 @@
    2.19  text{* A compact version without explicit base case: *}
    2.20  lemma infinite_descent:
    2.21    "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
    2.22 -by (induct n rule: less_induct, auto)
    2.23 +by (induct n rule: less_induct) auto
    2.24  
    2.25  lemma infinite_descent0[case_names 0 smaller]: 
    2.26    "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
    2.27 @@ -1164,7 +1164,7 @@
    2.28  
    2.29  lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
    2.30    apply (safe intro!: mult_less_mono1)
    2.31 -  apply (case_tac k, auto)
    2.32 +  apply (cases k, auto)
    2.33    apply (simp del: le_0_eq add: linorder_not_le [symmetric])
    2.34    apply (blast intro: mult_le_mono1)
    2.35    done
     3.1 --- a/src/HOL/Nitpick.thy	Thu May 24 17:05:30 2012 +0200
     3.2 +++ b/src/HOL/Nitpick.thy	Thu May 24 17:25:53 2012 +0200
     3.3 @@ -74,7 +74,7 @@
     3.4  
     3.5  lemma [nitpick_simp, no_atp]:
     3.6  "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
     3.7 -by (case_tac n) auto
     3.8 +by (cases n) auto
     3.9  
    3.10  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    3.11  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    3.12 @@ -106,7 +106,7 @@
    3.13  
    3.14  lemma Eps_psimp [nitpick_psimp, no_atp]:
    3.15  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
    3.16 -apply (case_tac "P (Eps P)")
    3.17 +apply (cases "P (Eps P)")
    3.18   apply auto
    3.19  apply (erule contrapos_np)
    3.20  by (rule someI)
    3.21 @@ -122,7 +122,7 @@
    3.22  lemma nat_case_unfold [nitpick_unfold, no_atp]:
    3.23  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    3.24  apply (rule eq_reflection)
    3.25 -by (case_tac n) auto
    3.26 +by (cases n) auto
    3.27  
    3.28  declare nat.cases [nitpick_simp del]
    3.29  
    3.30 @@ -130,7 +130,7 @@
    3.31  "list_size f xs = (if xs = [] then 0
    3.32                     else Suc (f (hd xs) + list_size f (tl xs)))"
    3.33  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
    3.34 -by (case_tac xs) auto
    3.35 +by (cases xs) auto
    3.36  
    3.37  text {*
    3.38  Auxiliary definitions used to provide an alternative representation for
     4.1 --- a/src/HOL/Product_Type.thy	Thu May 24 17:05:30 2012 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Thu May 24 17:25:53 2012 +0200
     4.3 @@ -1028,7 +1028,10 @@
     4.4  by blast
     4.5  
     4.6  lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
     4.7 -  by (auto, case_tac "f x", auto)
     4.8 +  apply auto
     4.9 +  apply (case_tac "f x")
    4.10 +  apply auto
    4.11 +  done
    4.12  
    4.13  lemma swap_inj_on:
    4.14    "inj_on (\<lambda>(i, j). (j, i)) A"
     5.1 --- a/src/HOL/Set_Interval.thy	Thu May 24 17:05:30 2012 +0200
     5.2 +++ b/src/HOL/Set_Interval.thy	Thu May 24 17:25:53 2012 +0200
     5.3 @@ -831,7 +831,7 @@
     5.4    done
     5.5  
     5.6  lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
     5.7 -  apply (case_tac "0 \<le> u")
     5.8 +  apply (cases "0 \<le> u")
     5.9    apply (subst image_atLeastZeroLessThan_int, assumption)
    5.10    apply (rule finite_imageI)
    5.11    apply auto
    5.12 @@ -858,7 +858,7 @@
    5.13  subsubsection {* Cardinality *}
    5.14  
    5.15  lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
    5.16 -  apply (case_tac "0 \<le> u")
    5.17 +  apply (cases "0 \<le> u")
    5.18    apply (subst image_atLeastZeroLessThan_int, assumption)
    5.19    apply (subst card_image)
    5.20    apply (auto simp add: inj_on_def)