# HG changeset patch
# User wenzelm
# Date 1551387598 -3600
# Node ID 5f993636ac079a85514d08c3c59515fd734f61f7
# Parent  09f200c658ed2443828bb86c4132ff112492eead
tuned proofs -- eliminated odd case_tac;

diff -r 09f200c658ed -r 5f993636ac07 src/HOL/BNF_Cardinal_Order_Relation.thy
--- 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
diff -r 09f200c658ed -r 5f993636ac07 src/HOL/BNF_Fixpoint_Base.thy
--- 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
diff -r 09f200c658ed -r 5f993636ac07 src/HOL/Basic_BNF_LFPs.thy
--- 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>
diff -r 09f200c658ed -r 5f993636ac07 src/HOL/Enum.thy
--- 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
 
diff -r 09f200c658ed -r 5f993636ac07 src/HOL/List.thy
--- 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