# HG changeset patch
# User nipkow
# Date 1292917068 -3600
# Node ID 9b3f25c934c8943a6ebdd714ebb91cf0e4842c85
# Parent  ffd730fcf0ac04c141c9e2ac7db6cecf8d514eda
tuned proof

diff -r ffd730fcf0ac -r 9b3f25c934c8 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Tue Dec 21 06:53:20 2010 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Tue Dec 21 08:37:48 2010 +0100
@@ -294,80 +294,69 @@
   finally show "?P (n + 1)" by simp
 qed
 
-lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
-  by auto
-
-lemma card_subsets_nat [rule_format]:
+lemma card_subsets_nat:
   fixes S :: "'a set"
-  assumes "finite S"
-  shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k" 
-      (is "?P S")
-using `finite S`
-proof (induct set: finite)
-  show "?P {}" by (auto simp add: set_explicit)
-  next fix x :: "'a" and F
-  assume iassms: "finite F" "x ~: F"
-  assume ih: "?P F"
-  show "?P (insert x F)" (is "ALL k. ?Q k")
-  proof
-    fix k
-    show "card {T. T \<subseteq> (insert x F) \<and> card T = k} = 
-        card (insert x F) choose k" (is "?Q k")
-    proof (induct k rule: induct'_nat)
-      from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
-        apply auto
-        apply (subst (asm) card_0_eq)
-        apply (auto elim: finite_subset)
-        done
-      thus "?Q 0" 
-        by auto
-      next fix k
-      show "?Q (k + 1)"
-      proof -
-        from iassms have fin: "finite (insert x F)" by auto
-        hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
-          {T. T \<le> F & card T = k + 1} Un 
-          {T. T \<le> insert x F & x : T & card T = k + 1}"
-          by (auto intro!: subsetI)
-        with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
-          card ({T. T \<subseteq> F \<and> card T = k + 1}) + 
-          card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
-          apply (subst card_Un_disjoint [symmetric])
-          apply auto
-          (* note: nice! Didn't have to say anything here *)
-          done
-        also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = 
-          card F choose (k+1)" by auto
-        also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
-          card ({T. T <= F & card T = k})"
-        proof -
-          let ?f = "%T. T Un {x}"
-          from iassms have "inj_on ?f {T. T <= F & card T = k}"
-            unfolding inj_on_def by (auto intro!: subsetI)
-          hence "card ({T. T <= F & card T = k}) = 
-            card(?f ` {T. T <= F & card T = k})"
-            by (rule card_image [symmetric])
-          also from iassms fin have "?f ` {T. T <= F & card T = k} = 
-            {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}"
-            unfolding image_def 
-            (* I can't figure out why this next line takes so long *)
-            apply auto
-            apply (frule (1) finite_subset, force)
-            apply (rule_tac x = "xa - {x}" in exI)
-            apply (subst card_Diff_singleton)
-            apply (auto elim: finite_subset)
-            done
-          finally show ?thesis by (rule sym)
-        qed
-        also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
-          by auto
-        finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
-          card F choose (k + 1) + (card F choose k)".
-        with iassms choose_plus_one_nat show ?thesis
-          by (auto simp del: card.insert)
+  shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
+proof (induct arbitrary: k set: finite)
+  case empty show ?case by (auto simp add: Collect_conv_if)
+next
+  case (insert x F)
+  note iassms = insert(1,2)
+  note ih = insert(3)
+  show ?case
+  proof (induct k rule: induct'_nat)
+    case zero
+    from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
+      by (auto simp: finite_subset)
+    thus ?case by auto
+  next
+    case (plus1 k)
+    from iassms have fin: "finite (insert x F)" by auto
+    hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
+      {T. T \<le> F & card T = k + 1} Un 
+      {T. T \<le> insert x F & x : T & card T = k + 1}"
+      by (auto intro!: subsetI)
+    with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
+      card ({T. T \<subseteq> F \<and> card T = k + 1}) + 
+      card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
+      apply (subst card_Un_disjoint [symmetric])
+      apply auto
+        (* note: nice! Didn't have to say anything here *)
+      done
+    also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = 
+      card F choose (k+1)" by auto
+    also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
+      card ({T. T <= F & card T = k})"
+    proof -
+      let ?f = "%T. T Un {x}"
+      from iassms have "inj_on ?f {T. T <= F & card T = k}"
+        unfolding inj_on_def by (auto intro!: subsetI)
+      hence "card ({T. T <= F & card T = k}) = 
+        card(?f ` {T. T <= F & card T = k})"
+        by (rule card_image [symmetric])
+      also have "?f ` {T. T <= F & card T = k} = 
+        {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
+      proof-
+        { fix S assume "S \<subseteq> F"
+          hence "card(insert x S) = card S +1"
+            using iassms by (auto simp: finite_subset) }
+        moreover
+        { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
+          let ?S = "T - {x}"
+          have "?S <= F & card ?S = k \<and> T = insert x ?S"
+            using 1 fin by (auto simp: finite_subset) }
+        ultimately show ?thesis by(auto simp: image_def)
       qed
+      finally show ?thesis by (rule sym)
     qed
+    also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
+      by auto
+    finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
+      card F choose (k + 1) + (card F choose k)".
+    with iassms choose_plus_one_nat show ?case
+      by (auto simp del: card.insert)
   qed
 qed
 
+
 end