--- a/src/HOL/Hilbert_Choice.thy Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu May 24 17:25:53 2012 +0200
@@ -443,7 +443,7 @@
have "h ` A = B"
proof safe
fix a assume "a \<in> A"
- thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto)
+ thus "h a \<in> B" using SUB1 2 3 by (cases "a \<in> A'") auto
next
fix b assume *: "b \<in> B"
show "b \<in> h ` A"
--- a/src/HOL/Nat.thy Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Nat.thy Thu May 24 17:25:53 2012 +0200
@@ -820,12 +820,12 @@
lemma Least_Suc:
"[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
- apply (case_tac "n", auto)
+ apply (cases n, auto)
apply (frule LeastI)
apply (drule_tac P = "%x. P (Suc x) " in LeastI)
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
apply (erule_tac [2] Least_le)
- apply (case_tac "LEAST x. P x", auto)
+ apply (cases "LEAST x. P x", auto)
apply (drule_tac P = "%x. P (Suc x) " in Least_le)
apply (blast intro: order_antisym)
done
@@ -911,7 +911,7 @@
text{* A compact version without explicit base case: *}
lemma infinite_descent:
"\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m \<rbrakk> \<Longrightarrow> P n"
-by (induct n rule: less_induct, auto)
+by (induct n rule: less_induct) auto
lemma infinite_descent0[case_names 0 smaller]:
"\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
@@ -1164,7 +1164,7 @@
lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
apply (safe intro!: mult_less_mono1)
- apply (case_tac k, auto)
+ apply (cases k, auto)
apply (simp del: le_0_eq add: linorder_not_le [symmetric])
apply (blast intro: mult_le_mono1)
done
--- a/src/HOL/Nitpick.thy Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Nitpick.thy Thu May 24 17:25:53 2012 +0200
@@ -74,7 +74,7 @@
lemma [nitpick_simp, no_atp]:
"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
-by (case_tac n) auto
+by (cases n) auto
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
@@ -106,7 +106,7 @@
lemma Eps_psimp [nitpick_psimp, no_atp]:
"\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
-apply (case_tac "P (Eps P)")
+apply (cases "P (Eps P)")
apply auto
apply (erule contrapos_np)
by (rule someI)
@@ -122,7 +122,7 @@
lemma nat_case_unfold [nitpick_unfold, no_atp]:
"nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
apply (rule eq_reflection)
-by (case_tac n) auto
+by (cases n) auto
declare nat.cases [nitpick_simp del]
@@ -130,7 +130,7 @@
"list_size f xs = (if xs = [] then 0
else Suc (f (hd xs) + list_size f (tl xs)))"
"size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
-by (case_tac xs) auto
+by (cases xs) auto
text {*
Auxiliary definitions used to provide an alternative representation for
--- a/src/HOL/Product_Type.thy Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Product_Type.thy Thu May 24 17:25:53 2012 +0200
@@ -1028,7 +1028,10 @@
by blast
lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
- by (auto, case_tac "f x", auto)
+ apply auto
+ apply (case_tac "f x")
+ apply auto
+ done
lemma swap_inj_on:
"inj_on (\<lambda>(i, j). (j, i)) A"
--- a/src/HOL/Set_Interval.thy Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Set_Interval.thy Thu May 24 17:25:53 2012 +0200
@@ -831,7 +831,7 @@
done
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
- apply (case_tac "0 \<le> u")
+ apply (cases "0 \<le> u")
apply (subst image_atLeastZeroLessThan_int, assumption)
apply (rule finite_imageI)
apply auto
@@ -858,7 +858,7 @@
subsubsection {* Cardinality *}
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
- apply (case_tac "0 \<le> u")
+ apply (cases "0 \<le> u")
apply (subst image_atLeastZeroLessThan_int, assumption)
apply (subst card_image)
apply (auto simp add: inj_on_def)