--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Feb 28 21:37:24 2019 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Feb 28 21:59:58 2019 +0100
@@ -525,7 +525,7 @@
moreover
{fix d assume "d \<in> A <+> C"
hence "g d \<in> B <+> C" using 1
- by(case_tac d, auto simp add: g_def)
+ by(cases d) (auto simp add: g_def)
}
ultimately show ?thesis unfolding inj_on_def by auto
qed
@@ -645,12 +645,12 @@
proof-
{fix c1 and c2 assume "?f c1 = ?f c2"
hence "c1 = c2"
- by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)
+ by(cases c1; cases c2) auto
}
moreover
{fix c assume "c \<in> A <+> A"
hence "?f c \<in> A \<times> (UNIV::bool set)"
- by(case_tac c, auto)
+ by(cases c) auto
}
moreover
{fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"
@@ -726,10 +726,10 @@
have "bij_betw ?f UNIV {a1,a2}"
proof-
{fix bl1 and bl2 assume "?f bl1 = ?f bl2"
- hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
+ hence "bl1 = bl2" using assms by (cases bl1, cases bl2) auto
}
moreover
- {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
+ {fix bl have "?f bl \<in> {a1,a2}" by (cases bl) auto
}
moreover
{fix a assume *: "a \<in> {a1,a2}"
@@ -1678,7 +1678,7 @@
show "f = g"
proof
fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
- by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
+ by (cases "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
then show "f x = g x" by (subst (1 2) surjective_pairing) simp
qed
next
--- a/src/HOL/BNF_Fixpoint_Base.thy Thu Feb 28 21:37:24 2019 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy Thu Feb 28 21:59:58 2019 +0100
@@ -188,17 +188,17 @@
by simp_all
lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
- by (case_tac x) simp
+ by (cases x) simp
lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
- by (case_tac x) simp+
+ by (cases x) simp_all
lemma case_sum_transfer:
"rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
unfolding rel_fun_def by (auto split: sum.splits)
lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
- by (case_tac x) simp+
+ by (cases x) simp_all
lemma case_prod_o_map_prod: "case_prod f \<circ> map_prod g1 g2 = case_prod (\<lambda>l r. f (g1 l) (g2 r))"
unfolding comp_def by auto
--- a/src/HOL/Basic_BNF_LFPs.thy Thu Feb 28 21:37:24 2019 +0100
+++ b/src/HOL/Basic_BNF_LFPs.thy Thu Feb 28 21:59:58 2019 +0100
@@ -84,12 +84,12 @@
lemma map_sum_sel:
"isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
"\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
- by (case_tac [!] s) simp_all
+ by (cases s; simp)+
lemma set_sum_sel:
"isl s \<Longrightarrow> projl s \<in> setl s"
"\<not> isl s \<Longrightarrow> projr s \<in> setr s"
- by (case_tac [!] s) (auto intro: setl.intros setr.intros)
+ by (cases s; auto intro: setl.intros setr.intros)+
lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
(isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
--- a/src/HOL/Enum.thy Thu Feb 28 21:37:24 2019 +0100
+++ b/src/HOL/Enum.thy Thu Feb 28 21:59:58 2019 +0100
@@ -674,7 +674,7 @@
fix x :: finite_2 and A
assume "x \<in> A"
then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
- by(case_tac [!] x)(auto simp add: less_eq_finite_2_def less_finite_2_def Inf_finite_2_def Sup_finite_2_def)
+ by(cases x; auto simp add: less_eq_finite_2_def less_finite_2_def Inf_finite_2_def Sup_finite_2_def)+
qed(auto simp add: less_eq_finite_2_def less_finite_2_def inf_finite_2_def sup_finite_2_def Inf_finite_2_def Sup_finite_2_def)
end
--- a/src/HOL/List.thy Thu Feb 28 21:37:24 2019 +0100
+++ b/src/HOL/List.thy Thu Feb 28 21:59:58 2019 +0100
@@ -970,7 +970,7 @@
proof (induct xs arbitrary: ys zs ts)
case (Cons x xs)
then show ?case
- by (case_tac zs) auto
+ by (cases zs) auto
qed fastforce
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
@@ -1238,11 +1238,13 @@
by (cases xs) auto
lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
-proof (induct xs arbitrary: ys)
- case (Cons a xs)
- then show ?case
- by (case_tac ys) auto
-qed force
+proof (induct xs arbitrary: ys)
+ case Nil
+ then show ?case by force
+next
+ case Cons
+ then show ?case by (cases ys) auto
+qed
lemma inj_on_rev[iff]: "inj_on rev A"
by(simp add:inj_on_def)
@@ -2043,16 +2045,22 @@
lemma take_Suc_conv_app_nth:
"i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
proof (induct xs arbitrary: i)
- case (Cons x xs) then show ?case
- by (case_tac i, auto)
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases i) auto
+qed
lemma Cons_nth_drop_Suc:
"i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
proof (induct xs arbitrary: i)
- case (Cons x xs) then show ?case
- by (case_tac i, auto)
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases i) auto
+qed
lemma length_take [simp]: "length (take n xs) = min (length xs) n"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
@@ -2076,30 +2084,42 @@
lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
proof (induct m arbitrary: xs n)
- case (Suc m) then show ?case
- by (case_tac xs; case_tac n; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs; cases n) simp_all
+qed
lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
proof (induct m arbitrary: xs)
- case (Suc m) then show ?case
- by (case_tac xs; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs) simp_all
+qed
lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
proof (induct m arbitrary: xs n)
- case (Suc m) then show ?case
- by (case_tac xs; case_tac n; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs; cases n) simp_all
+qed
lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
proof (induct n arbitrary: xs)
- case (Suc n) then show ?case
- by (case_tac xs; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs) simp_all
+qed
lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
@@ -2109,27 +2129,39 @@
lemma take_map: "take n (map f xs) = map f (take n xs)"
proof (induct n arbitrary: xs)
- case (Suc n) then show ?case
- by (case_tac xs; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs) simp_all
+qed
lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
proof (induct n arbitrary: xs)
- case (Suc n) then show ?case
- by (case_tac xs; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs) simp_all
+qed
lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
proof (induct xs arbitrary: i)
- case (Cons x xs) then show ?case
- by (case_tac i, auto)
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases i) auto
+qed
lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
proof (induct xs arbitrary: i)
- case (Cons x xs) then show ?case
- by (case_tac i, auto)
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases i) auto
+qed
lemma drop_rev: "drop n (rev xs) = rev (take (length xs - n) xs)"
by (cases "length xs < n") (auto simp: rev_take)
@@ -2139,16 +2171,22 @@
lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
proof (induct xs arbitrary: i n)
- case (Cons x xs) then show ?case
- by (case_tac n; case_tac i; simp)
-qed auto
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases n; cases i) simp_all
+qed
lemma nth_drop [simp]:
"n \<le> length xs ==> (drop n xs)!i = xs!(n + i)"
proof (induct n arbitrary: xs)
- case (Suc n) then show ?case
- by (case_tac xs; simp)
-qed auto
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs) simp_all
+qed
lemma butlast_take:
"n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
@@ -2563,27 +2601,39 @@
lemma take_zip: "take n (zip xs ys) = zip (take n xs) (take n ys)"
proof (induct n arbitrary: xs ys)
- case (Suc n)
- then show ?case
- by (case_tac xs; case_tac ys; simp)
-qed simp
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs; cases ys) simp_all
+qed
lemma drop_zip: "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
proof (induct n arbitrary: xs ys)
- case (Suc n)
- then show ?case
- by (case_tac xs; case_tac ys; simp)
-qed simp
+ case 0
+ then show ?case by simp
+next
+ case Suc
+ then show ?case by (cases xs; cases ys) simp_all
+qed
lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
proof (induct xs arbitrary: ys)
- case (Cons x xs) thus ?case by (cases ys) auto
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases ys) auto
+qed
lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
proof (induct xs arbitrary: ys)
- case (Cons x xs) thus ?case by (cases ys) auto
-qed simp
+ case Nil
+ then show ?case by simp
+next
+ case Cons
+ then show ?case by (cases ys) auto
+qed
lemma set_zip_leftD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
by (induct xs ys rule:list_induct2') auto
@@ -3652,11 +3702,18 @@
using f_mono by (simp add: mono_iff_le_Suc)
next
have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
- by safe (fastforce, rename_tac x, case_tac x, auto)
+ apply safe
+ apply fastforce
+ subgoal for \<dots> x by (cases x) auto
+ done
also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
proof -
have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth[of 0] by simp
- then show ?thesis by safe (fastforce, rename_tac x, case_tac x, auto)
+ then show ?thesis
+ apply safe
+ apply fastforce
+ subgoal for \<dots> x by (cases x) auto
+ done
qed
also have "\<dots> = {0 ..< length ys}" by fact
finally show "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
@@ -3682,16 +3739,17 @@
then have "\<And>i. Suc 0 < f (Suc i)"
using f_mono
by (meson Suc_le_mono le0 less_le_trans monoD)
- then have "\<And>i. Suc 0 \<noteq> f i" using \<open>f 0 = 0\<close>
- by (case_tac i) fastforce+
+ then have "Suc 0 \<noteq> f i" for i using \<open>f 0 = 0\<close>
+ by (cases i) fastforce+
then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
then show False using f_img \<open>2 \<le> length ys\<close> by auto
qed
obtain ys' where "ys = x1 # x2 # ys'"
using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
apply (cases ys)
- apply (rename_tac [2] ys', case_tac [2] ys')
- by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
+ apply (rename_tac [2] ys', case_tac [2] ys')
+ apply (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
+ done
define f' where "f' x = f (Suc x) - 1" for x