# HG changeset patch
# User wenzelm
# Date 1337873153 -7200
# Node ID e4b69e10b990a0af0012f4775af487ee0838d415
# Parent  4e9df6ffcc6ef3eebefdb967ac8c6521c7aaf572
tuned proofs;

diff -r 4e9df6ffcc6e -r e4b69e10b990 src/HOL/Hilbert_Choice.thy
--- 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"
diff -r 4e9df6ffcc6e -r e4b69e10b990 src/HOL/Nat.thy
--- 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
diff -r 4e9df6ffcc6e -r e4b69e10b990 src/HOL/Nitpick.thy
--- 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
diff -r 4e9df6ffcc6e -r e4b69e10b990 src/HOL/Product_Type.thy
--- 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"
diff -r 4e9df6ffcc6e -r e4b69e10b990 src/HOL/Set_Interval.thy
--- 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)