merged

--- a/src/HOL/Finite_Set.thy	Wed Feb 27 17:32:17 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 27 17:44:08 2013 +0100
@@ -356,6 +356,16 @@
   "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)"
   by (unfold Sigma_def) blast
 
+lemma finite_SigmaI2:
+  assumes "finite {x\<in>A. B x \<noteq> {}}"
+  and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
+  shows "finite (Sigma A B)"
+proof -
+  from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)" by auto
+  also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" by auto
+  finally show ?thesis .
+qed
+
 lemma finite_cartesian_product:
   "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)"
   by (rule finite_SigmaI)

--- a/src/HOL/Library/Numeral_Type.thy	Wed Feb 27 17:32:17 2013 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Feb 27 17:44:08 2013 +0100
@@ -287,10 +287,9 @@
 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
 
-subsection {* Linorder instance *}
+subsection {* Order instances *}
 
 instantiation bit0 and bit1 :: (finite) linorder begin
-
 definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
 definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
 definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"
@@ -299,8 +298,23 @@
 instance
   by(intro_classes)
     (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
+end
 
-end
+lemma (in preorder) tranclp_less: "op <\<^sup>+\<^sup>+ = op <"
+by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
+
+instance bit0 and bit1 :: (finite) wellorder
+proof -
+  have "wf {(x :: 'a bit0, y). x < y}"
+    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
+  thus "OFCLASS('a bit0, wellorder_class)"
+    by(rule wf_wellorderI) intro_classes
+next
+  have "wf {(x :: 'a bit1, y). x < y}"
+    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
+  thus "OFCLASS('a bit1, wellorder_class)"
+    by(rule wf_wellorderI) intro_classes
+qed
 
 subsection {* Code setup and type classes for code generation *}
 

--- a/src/HOL/Number_Theory/Binomial.thy	Wed Feb 27 17:32:17 2013 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Wed Feb 27 17:44:08 2013 +0100
@@ -362,4 +362,76 @@
  finally show ?thesis .
 qed
 
+lemma card_UNION:
+  assumes "finite A" and "\<forall>k \<in> A. finite k"
+  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
+  (is "?lhs = ?rhs")
+proof -
+  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
+  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
+    by(subst setsum_right_distrib) simp
+  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
+    using assms by(subst setsum_Sigma)(auto)
+  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
+    by(rule setsum_reindex_cong[where f="\<lambda>(x, y). (y, x)"])(auto intro: inj_onI simp add: split_beta)
+  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
+    using assms by(auto intro!: setsum_mono_zero_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
+  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. -1 ^ (card I + 1)))" 
+    using assms by(subst setsum_Sigma) auto
+  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
+  proof(rule setsum_cong[OF refl])
+    fix x
+    assume x: "x \<in> \<Union>A"
+    def K \<equiv> "{X \<in> A. x \<in> X}"
+    with `finite A` have K: "finite K" by auto
+
+    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
+    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
+      using assms by(auto intro!: inj_onI)
+    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
+      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq] One_nat_def dest: finite_subset intro: card_mono)
+    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
+      by(rule setsum_reindex_cong[where f=snd]) fastforce
+    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
+      using assms by(subst setsum_Sigma) auto
+    also have "\<dots> = (\<Sum>i=1..card A. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
+      by(subst setsum_right_distrib) simp
+    also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
+    proof(rule setsum_mono_zero_cong_right[rule_format])
+      show "{1..card K} \<subseteq> {1..card A}" using `finite A`
+        by(auto simp add: K_def intro: card_mono)
+    next
+      fix i
+      assume "i \<in> {1..card A} - {1..card K}"
+      hence i: "i \<le> card A" "card K < i" by auto
+      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}" 
+        by(auto simp add: K_def)
+      also have "\<dots> = {}" using `finite A` i
+        by(auto simp add: K_def dest: card_mono[rotated 1])
+      finally show "-1 ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
+        by(simp only:) simp
+    next
+      fix i
+      have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
+        (is "?lhs = ?rhs")
+        by(rule setsum_cong)(auto simp add: K_def)
+      thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp
+    qed simp
+    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
+      by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
+    hence "?rhs = (\<Sum>i = 0..card K. -1 ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
+      by(subst (2) setsum_head_Suc)(simp_all add: One_nat_def)
+    also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
+      using K by(subst card_subsets_nat[symmetric]) simp_all
+    also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
+      by(subst setsum_right_distrib[symmetric]) simp
+    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
+      by(subst binomial)(simp add: mult_ac)
+    also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
+    finally show "?lhs x = 1" .
+  qed
+  also have "nat \<dots> = card (\<Union>A)" by simp
+  finally show ?thesis ..
+qed
+
 end