tuned proofs -- eliminated odd case_tac;
authorwenzelm
Thu Feb 28 21:59:58 2019 +0100 (7 weeks ago ago)
changeset 700315f993636ac07
parent 70030 09f200c658ed
child 70032 29a4f633609e
tuned proofs -- eliminated odd case_tac;
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/Basic_BNF_LFPs.thy
src/HOL/Enum.thy
src/HOL/List.thy
     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.30  by(simp add:inj_on_def)
    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 [2] ys', case_tac [2] ys')
   5.284 -        by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
   5.285 +         apply (rename_tac [2] ys', case_tac [2] 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