author wenzelm Thu Feb 28 21:59:58 2019 +0100 (17 months ago ago) changeset 70031 5f993636ac07 parent 70030 09f200c658ed child 70032 29a4f633609e
tuned proofs -- eliminated odd case_tac;
 src/HOL/BNF_Cardinal_Order_Relation.thy file | annotate | diff | revisions src/HOL/BNF_Fixpoint_Base.thy file | annotate | diff | revisions src/HOL/Basic_BNF_LFPs.thy file | annotate | diff | revisions src/HOL/Enum.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 28 21:37:24 2019 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 28 21:59:58 2019 +0100
1.3 @@ -525,7 +525,7 @@
1.4      moreover
1.5      {fix d assume "d \<in> A <+> C"
1.6       hence "g d \<in> B <+> C"  using 1
1.7 -     by(case_tac d, auto simp add: g_def)
1.8 +     by(cases d) (auto simp add: g_def)
1.9      }
1.10      ultimately show ?thesis unfolding inj_on_def by auto
1.11    qed
1.12 @@ -645,12 +645,12 @@
1.13    proof-
1.14      {fix  c1 and c2 assume "?f c1 = ?f c2"
1.15       hence "c1 = c2"
1.16 -     by(case_tac "c1", case_tac "c2", auto, case_tac "c2", auto)
1.17 +     by(cases c1; cases c2) auto
1.18      }
1.19      moreover
1.20      {fix c assume "c \<in> A <+> A"
1.21       hence "?f c \<in> A \<times> (UNIV::bool set)"
1.22 -     by(case_tac c, auto)
1.23 +     by(cases c) auto
1.24      }
1.25      moreover
1.26      {fix a bl assume *: "(a,bl) \<in> A \<times> (UNIV::bool set)"
1.27 @@ -726,10 +726,10 @@
1.28    have "bij_betw ?f UNIV {a1,a2}"
1.29    proof-
1.30      {fix bl1 and bl2 assume "?f  bl1 = ?f bl2"
1.31 -     hence "bl1 = bl2" using assms by (case_tac bl1, case_tac bl2, auto)
1.32 +     hence "bl1 = bl2" using assms by (cases bl1, cases bl2) auto
1.33      }
1.34      moreover
1.35 -    {fix bl have "?f bl \<in> {a1,a2}" by (case_tac bl, auto)
1.36 +    {fix bl have "?f bl \<in> {a1,a2}" by (cases bl) auto
1.37      }
1.38      moreover
1.39      {fix a assume *: "a \<in> {a1,a2}"
1.40 @@ -1678,7 +1678,7 @@
1.41      show "f = g"
1.42      proof
1.43        fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
1.44 -        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
1.45 +        by (cases "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
1.46        then show "f x = g x" by (subst (1 2) surjective_pairing) simp
1.47      qed
1.48    next
```
```     2.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Feb 28 21:37:24 2019 +0100
2.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Feb 28 21:59:58 2019 +0100
2.3 @@ -188,17 +188,17 @@
2.4    by simp_all
2.5
2.6  lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
2.7 -  by (case_tac x) simp
2.8 +  by (cases x) simp
2.9
2.10  lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
2.11 -  by (case_tac x) simp+
2.12 +  by (cases x) simp_all
2.13
2.14  lemma case_sum_transfer:
2.15    "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
2.16    unfolding rel_fun_def by (auto split: sum.splits)
2.17
2.18  lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
2.19 -  by (case_tac x) simp+
2.20 +  by (cases x) simp_all
2.21
2.22  lemma case_prod_o_map_prod: "case_prod f \<circ> map_prod g1 g2 = case_prod (\<lambda>l r. f (g1 l) (g2 r))"
2.23    unfolding comp_def by auto
```
```     3.1 --- a/src/HOL/Basic_BNF_LFPs.thy	Thu Feb 28 21:37:24 2019 +0100
3.2 +++ b/src/HOL/Basic_BNF_LFPs.thy	Thu Feb 28 21:59:58 2019 +0100
3.3 @@ -84,12 +84,12 @@
3.4  lemma map_sum_sel:
3.5    "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
3.6    "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
3.7 -  by (case_tac [!] s) simp_all
3.8 +  by (cases s; simp)+
3.9
3.10  lemma set_sum_sel:
3.11    "isl s \<Longrightarrow> projl s \<in> setl s"
3.12    "\<not> isl s \<Longrightarrow> projr s \<in> setr s"
3.13 -  by (case_tac [!] s) (auto intro: setl.intros setr.intros)
3.14 +  by (cases s; auto intro: setl.intros setr.intros)+
3.15
3.16  lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
3.17    (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
```
```     4.1 --- a/src/HOL/Enum.thy	Thu Feb 28 21:37:24 2019 +0100
4.2 +++ b/src/HOL/Enum.thy	Thu Feb 28 21:59:58 2019 +0100
4.3 @@ -674,7 +674,7 @@
4.4    fix x :: finite_2 and A
4.5    assume "x \<in> A"
4.6    then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
4.7 -    by(case_tac [!] x)(auto simp add: less_eq_finite_2_def less_finite_2_def Inf_finite_2_def Sup_finite_2_def)
4.8 +    by(cases x; auto simp add: less_eq_finite_2_def less_finite_2_def Inf_finite_2_def Sup_finite_2_def)+
4.9  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)
4.10  end
4.11
```
```     5.1 --- a/src/HOL/List.thy	Thu Feb 28 21:37:24 2019 +0100
5.2 +++ b/src/HOL/List.thy	Thu Feb 28 21:59:58 2019 +0100
5.3 @@ -970,7 +970,7 @@
5.4  proof (induct xs arbitrary: ys zs ts)
5.5    case (Cons x xs)
5.6    then show ?case
5.7 -    by (case_tac zs) auto
5.8 +    by (cases zs) auto
5.9  qed fastforce
5.10
5.11  lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
5.12 @@ -1238,11 +1238,13 @@
5.13  by (cases xs) auto
5.14
5.15  lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
5.16 -proof  (induct xs arbitrary: ys)
5.17 -  case (Cons a xs)
5.18 -  then show ?case
5.19 -    by (case_tac ys) auto
5.20 -qed force
5.21 +proof (induct xs arbitrary: ys)
5.22 +  case Nil
5.23 +  then show ?case by force
5.24 +next
5.25 +  case Cons
5.26 +  then show ?case by (cases ys) auto
5.27 +qed
5.28
5.29  lemma inj_on_rev[iff]: "inj_on rev A"
5.31 @@ -2043,16 +2045,22 @@
5.32  lemma take_Suc_conv_app_nth:
5.33    "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
5.34  proof (induct xs arbitrary: i)
5.35 -  case (Cons x xs) then show ?case
5.36 -    by (case_tac i, auto)
5.37 -qed simp
5.38 +  case Nil
5.39 +  then show ?case by simp
5.40 +next
5.41 +  case Cons
5.42 +  then show ?case by (cases i) auto
5.43 +qed
5.44
5.45  lemma Cons_nth_drop_Suc:
5.46    "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
5.47  proof (induct xs arbitrary: i)
5.48 -  case (Cons x xs) then show ?case
5.49 -    by (case_tac i, auto)
5.50 -qed simp
5.51 +  case Nil
5.52 +  then show ?case by simp
5.53 +next
5.54 +  case Cons
5.55 +  then show ?case by (cases i) auto
5.56 +qed
5.57
5.58  lemma length_take [simp]: "length (take n xs) = min (length xs) n"
5.59    by (induct n arbitrary: xs) (auto, case_tac xs, auto)
5.60 @@ -2076,30 +2084,42 @@
5.61
5.62  lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
5.63  proof (induct m arbitrary: xs n)
5.64 -  case (Suc m) then show ?case
5.65 -    by (case_tac xs; case_tac n; simp)
5.66 -qed auto
5.67 +  case 0
5.68 +  then show ?case by simp
5.69 +next
5.70 +  case Suc
5.71 +  then show ?case by (cases xs; cases n) simp_all
5.72 +qed
5.73
5.74  lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
5.75  proof (induct m arbitrary: xs)
5.76 -  case (Suc m) then show ?case
5.77 -    by (case_tac xs; simp)
5.78 -qed auto
5.79 +  case 0
5.80 +  then show ?case by simp
5.81 +next
5.82 +  case Suc
5.83 +  then show ?case by (cases xs) simp_all
5.84 +qed
5.85
5.86  lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
5.87  proof (induct m arbitrary: xs n)
5.88 -  case (Suc m) then show ?case
5.89 -    by (case_tac xs; case_tac n; simp)
5.90 -qed auto
5.91 +  case 0
5.92 +  then show ?case by simp
5.93 +next
5.94 +  case Suc
5.95 +  then show ?case by (cases xs; cases n) simp_all
5.96 +qed
5.97
5.98  lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
5.99    by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
5.100
5.101  lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
5.102  proof (induct n arbitrary: xs)
5.103 -  case (Suc n) then show ?case
5.104 -    by (case_tac xs; simp)
5.105 -qed auto
5.106 +  case 0
5.107 +  then show ?case by simp
5.108 +next
5.109 +  case Suc
5.110 +  then show ?case by (cases xs) simp_all
5.111 +qed
5.112
5.113  lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
5.114    by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
5.115 @@ -2109,27 +2129,39 @@
5.116
5.117  lemma take_map: "take n (map f xs) = map f (take n xs)"
5.118  proof (induct n arbitrary: xs)
5.119 -  case (Suc n) then show ?case
5.120 -    by (case_tac xs; simp)
5.121 -qed auto
5.122 +  case 0
5.123 +  then show ?case by simp
5.124 +next
5.125 +  case Suc
5.126 +  then show ?case by (cases xs) simp_all
5.127 +qed
5.128
5.129  lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
5.130  proof (induct n arbitrary: xs)
5.131 -  case (Suc n) then show ?case
5.132 -    by (case_tac xs; simp)
5.133 -qed auto
5.134 +  case 0
5.135 +  then show ?case by simp
5.136 +next
5.137 +  case Suc
5.138 +  then show ?case by (cases xs) simp_all
5.139 +qed
5.140
5.141  lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
5.142  proof (induct xs arbitrary: i)
5.143 -  case (Cons x xs) then show ?case
5.144 -    by (case_tac i, auto)
5.145 -qed simp
5.146 +  case Nil
5.147 +  then show ?case by simp
5.148 +next
5.149 +  case Cons
5.150 +  then show ?case by (cases i) auto
5.151 +qed
5.152
5.153  lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
5.154  proof (induct xs arbitrary: i)
5.155 -  case (Cons x xs) then show ?case
5.156 -    by (case_tac i, auto)
5.157 -qed simp
5.158 +  case Nil
5.159 +  then show ?case by simp
5.160 +next
5.161 +  case Cons
5.162 +  then show ?case by (cases i) auto
5.163 +qed
5.164
5.165  lemma drop_rev: "drop n (rev xs) = rev (take (length xs - n) xs)"
5.166    by (cases "length xs < n") (auto simp: rev_take)
5.167 @@ -2139,16 +2171,22 @@
5.168
5.169  lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
5.170  proof (induct xs arbitrary: i n)
5.171 -  case (Cons x xs) then show ?case
5.172 -    by (case_tac n; case_tac i; simp)
5.173 -qed auto
5.174 +  case Nil
5.175 +  then show ?case by simp
5.176 +next
5.177 +  case Cons
5.178 +  then show ?case by (cases n; cases i) simp_all
5.179 +qed
5.180
5.181  lemma nth_drop [simp]:
5.182    "n \<le> length xs ==> (drop n xs)!i = xs!(n + i)"
5.183  proof (induct n arbitrary: xs)
5.184 -  case (Suc n) then show ?case
5.185 -    by (case_tac xs; simp)
5.186 -qed auto
5.187 +  case 0
5.188 +  then show ?case by simp
5.189 +next
5.190 +  case Suc
5.191 +  then show ?case by (cases xs) simp_all
5.192 +qed
5.193
5.194  lemma butlast_take:
5.195    "n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
5.196 @@ -2563,27 +2601,39 @@
5.197
5.198  lemma take_zip: "take n (zip xs ys) = zip (take n xs) (take n ys)"
5.199  proof (induct n arbitrary: xs ys)
5.200 -  case (Suc n)
5.201 -  then show ?case
5.202 -    by (case_tac xs; case_tac ys; simp)
5.203 -qed simp
5.204 +  case 0
5.205 +  then show ?case by simp
5.206 +next
5.207 +  case Suc
5.208 +  then show ?case by (cases xs; cases ys) simp_all
5.209 +qed
5.210
5.211  lemma drop_zip: "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
5.212  proof (induct n arbitrary: xs ys)
5.213 -  case (Suc n)
5.214 -  then show ?case
5.215 -    by (case_tac xs; case_tac ys; simp)
5.216 -qed simp
5.217 +  case 0
5.218 +  then show ?case by simp
5.219 +next
5.220 +  case Suc
5.221 +  then show ?case by (cases xs; cases ys) simp_all
5.222 +qed
5.223
5.224  lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
5.225  proof (induct xs arbitrary: ys)
5.226 -  case (Cons x xs) thus ?case by (cases ys) auto
5.227 -qed simp
5.228 +  case Nil
5.229 +  then show ?case by simp
5.230 +next
5.231 +  case Cons
5.232 +  then show ?case by (cases ys) auto
5.233 +qed
5.234
5.235  lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
5.236  proof (induct xs arbitrary: ys)
5.237 -  case (Cons x xs) thus ?case by (cases ys) auto
5.238 -qed simp
5.239 +  case Nil
5.240 +  then show ?case by simp
5.241 +next
5.242 +  case Cons
5.243 +  then show ?case by (cases ys) auto
5.244 +qed
5.245
5.246  lemma set_zip_leftD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
5.247    by (induct xs ys rule:list_induct2') auto
5.248 @@ -3652,11 +3702,18 @@
5.249            using f_mono by (simp add: mono_iff_le_Suc)
5.250        next
5.251          have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
5.252 -          by safe (fastforce, rename_tac x, case_tac x, auto)
5.253 +          apply safe
5.254 +           apply fastforce
5.255 +          subgoal for \<dots> x by (cases x) auto
5.256 +          done
5.257          also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
5.258          proof -
5.259            have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth[of 0] by simp
5.260 -          then show ?thesis by safe (fastforce, rename_tac x, case_tac x, auto)
5.261 +          then show ?thesis
5.262 +            apply safe
5.263 +             apply fastforce
5.264 +            subgoal for \<dots> x by (cases x) auto
5.265 +            done
5.266          qed
5.267          also have "\<dots> = {0 ..< length ys}" by fact
5.268          finally show  "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
5.269 @@ -3682,16 +3739,17 @@
5.270          then have "\<And>i. Suc 0 < f (Suc i)"
5.271            using f_mono
5.272            by (meson Suc_le_mono le0 less_le_trans monoD)
5.273 -        then have "\<And>i. Suc 0 \<noteq> f i" using \<open>f 0 = 0\<close>
5.274 -          by (case_tac i) fastforce+
5.275 +        then have "Suc 0 \<noteq> f i" for i using \<open>f 0 = 0\<close>
5.276 +          by (cases i) fastforce+
5.277          then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
5.278          then show False using f_img \<open>2 \<le> length ys\<close> by auto
5.279        qed
5.280        obtain ys' where "ys = x1 # x2 # ys'"
5.281          using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
5.282          apply (cases ys)
5.283 -        apply (rename_tac  ys', case_tac  ys')
5.284 -        by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
5.285 +         apply (rename_tac  ys', case_tac  ys')
5.286 +          apply (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
5.287 +        done
5.288
5.289        define f' where "f' x = f (Suc x) - 1" for x
5.290
```