# HG changeset patch
# User paulson
# Date 1385253110 0
# Node ID 002b8729f22802d984a6255f267d8ed0ceb6a7c6
# Parent  e51a0c4965f7a3d74571e73ce5c9491e5930e22c
polished some ancient proofs

diff -r e51a0c4965f7 -r 002b8729f228 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Nov 23 16:41:37 2013 +0000
+++ b/src/HOL/Finite_Set.thy	Sun Nov 24 00:31:50 2013 +0000
@@ -1488,12 +1488,10 @@
 lemma card_Suc_eq:
   "(card A = Suc k) =
    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
-apply(rule iffI)
- apply(erule card_eq_SucD)
-apply(auto)
-apply(subst card.insert)
- apply(auto intro:ccontr)
-done
+ apply(auto elim!: card_eq_SucD)
+ apply(subst card.insert)
+ apply(auto simp add: intro:ccontr)
+ done
 
 lemma card_le_Suc_iff: "finite A \<Longrightarrow>
   Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
@@ -1520,11 +1518,8 @@
 
 subsubsection {* Cardinality of image *}
 
-lemma card_image_le: "finite A ==> card (f ` A) <= card A"
-apply (induct rule: finite_induct)
- apply simp
-apply (simp add: le_SucI card_insert_if)
-done
+lemma card_image_le: "finite A ==> card (f ` A) \<le> card A"
+  by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)
 
 lemma card_image:
   assumes "inj_on f A"
@@ -1543,24 +1538,27 @@
 by (simp add: card_seteq card_image)
 
 lemma eq_card_imp_inj_on:
-  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
-apply (induct rule:finite_induct)
-apply simp
-apply(frule card_image_le[where f = f])
-apply(simp add:card_insert_if split:if_splits)
-done
+  assumes "finite A" "card(f ` A) = card A" shows "inj_on f A"
+using assms
+proof (induct rule:finite_induct)
+  case empty show ?case by simp
+next
+  case (insert x A)
+  then show ?case using card_image_le [of A f]
+    by (simp add: card_insert_if split: if_splits)
+qed
 
-lemma inj_on_iff_eq_card:
-  "finite A ==> inj_on f A = (card(f ` A) = card A)"
-by(blast intro: card_image eq_card_imp_inj_on)
-
+lemma inj_on_iff_eq_card: "finite A \<Longrightarrow> inj_on f A \<longleftrightarrow> card(f ` A) = card A"
+  by (blast intro: card_image eq_card_imp_inj_on)
 
 lemma card_inj_on_le:
-  "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
-apply (subgoal_tac "finite A") 
- apply (force intro: card_mono simp add: card_image [symmetric])
-apply (blast intro: finite_imageD dest: finite_subset) 
-done
+  assumes "inj_on f A" "f ` A \<subseteq> B" "finite B" shows "card A \<le> card B"
+proof -
+  have "finite A" using assms
+    by (blast intro: finite_imageD dest: finite_subset)
+  then show ?thesis using assms 
+   by (force intro: card_mono simp: card_image [symmetric])
+qed
 
 lemma card_bij_eq:
   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
@@ -1642,44 +1640,52 @@
 
 subsubsection {* Cardinality of the Powerset *}
 
-lemma card_Pow: "finite A ==> card (Pow A) = 2 ^ card A"
-apply (induct rule: finite_induct)
- apply (simp_all add: Pow_insert)
-apply (subst card_Un_disjoint, blast)
-  apply (blast, blast)
-apply (subgoal_tac "inj_on (insert x) (Pow F)")
- apply (subst mult_2)
- apply (simp add: card_image Pow_insert)
-apply (unfold inj_on_def)
-apply (blast elim!: equalityE)
-done
+lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
+proof (induct rule: finite_induct)
+  case empty 
+    show ?case by auto
+next
+  case (insert x A)
+  then have "inj_on (insert x) (Pow A)" 
+    unfolding inj_on_def by (blast elim!: equalityE)
+  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" 
+    by (simp add: mult_2 card_image Pow_insert insert.hyps)
+  then show ?case using insert
+    apply (simp add: Pow_insert)
+    apply (subst card_Un_disjoint, auto)
+    done
+qed
 
 text {* Relates to equivalence classes.  Based on a theorem of F. Kamm\"uller.  *}
 
 lemma dvd_partition:
-  "finite (Union C) ==>
-    ALL c : C. k dvd card c ==>
-    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
-  k dvd card (Union C)"
-apply (frule finite_UnionD)
-apply (rotate_tac -1)
-apply (induct rule: finite_induct)
-apply simp_all
-apply clarify
-apply (subst card_Un_disjoint)
-   apply (auto simp add: disjoint_eq_subset_Compl)
-done
-
+  assumes f: "finite (\<Union>C)" and "\<forall>c\<in>C. k dvd card c" "\<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}"
+    shows "k dvd card (\<Union>C)"
+proof -
+  have "finite C" 
+    by (rule finite_UnionD [OF f])
+  then show ?thesis using assms
+  proof (induct rule: finite_induct)
+    case empty show ?case by simp
+  next
+    case (insert c C)
+    then show ?case 
+      apply simp
+      apply (subst card_Un_disjoint)
+      apply (auto simp add: disjoint_eq_subset_Compl)
+      done
+  qed
+qed
 
 subsubsection {* Relating injectivity and surjectivity *}
 
-lemma finite_surj_inj: "finite A \<Longrightarrow> A \<subseteq> f ` A \<Longrightarrow> inj_on f A"
-apply(rule eq_card_imp_inj_on, assumption)
-apply(frule finite_imageI)
-apply(drule (1) card_seteq)
- apply(erule card_image_le)
-apply simp
-done
+lemma finite_surj_inj: assumes "finite A" "A \<subseteq> f ` A" shows "inj_on f A"
+proof -
+  have "f ` A = A" 
+    by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le)
+  then show ?thesis using assms
+    by (simp add: eq_card_imp_inj_on)
+qed
 
 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"