# HG changeset patch
# User wenzelm
# Date 1435270450 -7200
# Node ID a645a0e6d790379ab78aead96fbd13d1885c619a
# Parent  d694f217ee41dd0db24efbe9e7118ada8ab6d885
tuned proofs;

diff -r d694f217ee41 -r a645a0e6d790 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu Jun 25 23:51:54 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Jun 26 00:14:10 2015 +0200
@@ -470,23 +470,39 @@
   in if n = 0 then False else 
         let xs' = remdups xs; ys' = remdups ys 
         in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
-  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
-  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
-  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
-  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
-proof -
-  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
-  proof
-    assume ?lhs thus ?rhs
-      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
-  next
-    assume ?rhs
-    moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
-    ultimately show ?lhs
-      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
-  qed
-  thus ?thesis2 unfolding eq_set_def by blast
-  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
+  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
+  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
+  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+proof goals
+  {
+    case 1
+    show ?case (is "?lhs \<longleftrightarrow> ?rhs")
+    proof
+      show ?rhs if ?lhs
+        using that
+        by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+          card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
+          Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+      show ?lhs if ?rhs
+      proof - 
+        have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
+        with that show ?thesis
+          by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+            card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
+            dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
+      qed
+    qed
+  }
+  moreover
+  case 2
+  ultimately show ?case unfolding eq_set_def by blast
+next
+  case 3
+  show ?case unfolding eq_set_def List.coset_def by blast
+next
+  case 4
+  show ?case unfolding eq_set_def List.coset_def by blast
 qed
 
 end
diff -r d694f217ee41 -r a645a0e6d790 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Thu Jun 25 23:51:54 2015 +0200
+++ b/src/HOL/Library/FinFun.thy	Fri Jun 26 00:14:10 2015 +0200
@@ -1320,11 +1320,10 @@
 lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
   and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
   and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
-proof -
-  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
+proof (atomize (full))
+  show "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
     unfolding finfun_to_list_def
     by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
-  thus ?thesis1 ?thesis2 ?thesis3 by simp_all
 qed
 
 lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
diff -r d694f217ee41 -r a645a0e6d790 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Thu Jun 25 23:51:54 2015 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 26 00:14:10 2015 +0200
@@ -119,15 +119,20 @@
 qed
 
 lemma mark_out_aux_simps [simp, code]:
-  "mark_out_aux n m [] = []" (is ?thesis1)
-  "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs" (is ?thesis2)
-  "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs" (is ?thesis3)
-proof -
-  show ?thesis1
+  "mark_out_aux n m [] = []"
+  "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs"
+  "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs"
+proof goals
+  case 1
+  show ?case
     by (simp add: mark_out_aux_def)
-  show ?thesis2
+next
+  case 2
+  show ?case
     by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
       enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
+next
+  case 3
   { def v \<equiv> "Suc m" and w \<equiv> "Suc n"
     fix q
     assume "m + n \<le> q"
@@ -150,7 +155,7 @@
       Suc n dvd Suc (Suc (q + n - m mod Suc n))"
       by (simp add: v_def w_def Suc_diff_le trans_le_add2)
   }
-  then show ?thesis3
+  then show ?case
     by (auto simp add: mark_out_aux_def
       enumerate_Suc_eq in_set_enumerate_eq not_less)
 qed