# 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 \ A" - thus "h a \ B" using SUB1 2 3 by (case_tac "a \ A'", auto) + thus "h a \ B" using SUB1 2 3 by (cases "a \ A'") auto next fix b assume *: "b \ B" show "b \ 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) \ 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: "\ !!n::nat. \ P n \ \m P m \ \ P n" -by (induct n rule: less_induct, auto) +by (induct n rule: less_induct) auto lemma infinite_descent0[case_names 0 smaller]: "\ P 0; !!n. n>0 \ \ P n \ (\m::nat. m < n \ \P m) \ \ 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 \ 'b set \ ('a \ 'b) set" where "prod A B = {(a, b). a \ A \ b \ B}" @@ -106,7 +106,7 @@ lemma Eps_psimp [nitpick_psimp, no_atp]: "\P x; \ P y; Eps P = y\ \ 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 \ 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 \ B) = ((fst \ f) -` A) \ ((snd \ 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 (\(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 (cases "0 \ 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") + apply (cases "0 \ u") apply (subst image_atLeastZeroLessThan_int, assumption) apply (subst card_image) apply (auto simp add: inj_on_def)