--- a/src/HOL/Finite_Set.thy Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/Finite_Set.thy Fri Oct 05 08:38:09 2007 +0200
@@ -1505,10 +1505,10 @@
"card A == setsum (%x. 1::nat) A"
lemma card_empty [simp]: "card {} = 0"
- by (simp add: card_def)
+by (simp add: card_def)
lemma card_infinite [simp]: "~ finite A ==> card A = 0"
- by (simp add: card_def)
+by (simp add: card_def)
lemma card_eq_setsum: "card A = setsum (%x. 1) A"
by (simp add: card_def)
@@ -1529,24 +1529,33 @@
lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
by auto
+
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
apply(simp del:insert_Diff_single)
done
lemma card_Diff_singleton:
- "finite A ==> x: A ==> card (A - {x}) = card A - 1"
- by (simp add: card_Suc_Diff1 [symmetric])
+ "finite A ==> x: A ==> card (A - {x}) = card A - 1"
+by (simp add: card_Suc_Diff1 [symmetric])
lemma card_Diff_singleton_if:
- "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
- by (simp add: card_Diff_singleton)
+ "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
+by (simp add: card_Diff_singleton)
+
+lemma card_Diff_insert[simp]:
+assumes "finite A" and "a:A" and "a ~: B"
+shows "card(A - insert a B) = card(A - B) - 1"
+proof -
+ have "A - insert a B = (A - B) - {a}" using assms by blast
+ then show ?thesis using assms by(simp add:card_Diff_singleton)
+qed
lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
- by (simp add: card_insert_if card_Suc_Diff1)
+by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
- by (simp add: card_insert_if)
+by (simp add: card_insert_if)
lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
by (simp add: card_def setsum_mono2)
@@ -1561,9 +1570,9 @@
done
lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
- apply (simp add: psubset_def linorder_not_le [symmetric])
- apply (blast dest: card_seteq)
- done
+apply (simp add: psubset_def linorder_not_le [symmetric])
+apply (blast dest: card_seteq)
+done
lemma card_Un_Int: "finite A ==> finite B
==> card A + card B = card (A Un B) + card (A Int B)"
@@ -1571,7 +1580,7 @@
lemma card_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> card (A Un B) = card A + card B"
- by (simp add: card_Un_Int)
+by (simp add: card_Un_Int)
lemma card_Diff_subset:
"finite B ==> B <= A ==> card (A - B) = card A - card B"
@@ -1579,15 +1588,15 @@
lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
apply (rule Suc_less_SucD)
- apply (simp add: card_Suc_Diff1)
+ apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
done
lemma card_Diff2_less:
"finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
apply (case_tac "x = y")
- apply (simp add: card_Diff1_less)
+ apply (simp add: card_Diff1_less del:card_Diff_insert)
apply (rule less_trans)
- prefer 2 apply (auto intro!: card_Diff1_less)
+ prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
done
lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
@@ -1619,32 +1628,39 @@
text{*The form of a finite set of given cardinality*}
lemma card_eq_SucD:
- assumes cardeq: "card A = Suc k" and fin: "finite A"
- shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k"
+assumes "card A = Suc k"
+shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
proof -
- have "card A \<noteq> 0" using cardeq by auto
- then obtain b where b: "b \<in> A" using fin by auto
+ have fin: "finite A" using assms by (auto intro: ccontr)
+ moreover have "card A \<noteq> 0" using assms by auto
+ ultimately obtain b where b: "b \<in> A" by auto
show ?thesis
proof (intro exI conjI)
show "A = insert b (A-{b})" using b by blast
show "b \<notin> A - {b}" by blast
- show "card (A - {b}) = k" by (simp add: fin cardeq b card_Diff_singleton)
+ show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
+ using assms b fin by(fastsimp dest:mk_disjoint_insert)+
qed
qed
-
lemma card_Suc_eq:
- "finite A ==>
- (card A = Suc k) = (\<exists>b B. A = insert b B & b \<notin> B & card B = k)"
-by (auto dest!: card_eq_SucD)
-
+ "(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
+(*
lemma card_1_eq:
- "finite A ==> (card A = Suc 0) = (\<exists>x. A = {x})"
-by (auto dest!: card_eq_SucD)
+ "(card A = Suc 0) = (\<exists>x. A = {x})"
+by (auto dest!: card_eq_SucD)
lemma card_2_eq:
- "finite A ==> (card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})"
-by (auto dest!: card_eq_SucD, blast)
+ "(card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})"
+by (auto dest!: card_eq_SucD)
+*)
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
--- a/src/HOL/Library/Ramsey.thy Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/Library/Ramsey.thy Fri Oct 05 08:38:09 2007 +0200
@@ -64,7 +64,7 @@
==> part r s (Y - {y}) (%u. f (insert y u))"
apply(simp add: part_def, clarify)
apply(drule_tac x="insert y X" in spec)
- apply(force simp:card_Diff_singleton_if)
+ apply(force)
done
lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
@@ -82,7 +82,7 @@
(\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
proof (induct r)
case 0
- thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
+ thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
next
case (Suc r)
show ?case
@@ -187,7 +187,7 @@
qed
moreover
have "card (X - {ya}) = r"
- by (simp add: card_Diff_singleton_if cardX ya)
+ by (simp add: cardX ya)
ultimately show ?thesis
using pg [of "LEAST x. x \<in> AA"] fields cardX
by (clarsimp simp del:insert_Diff_single)
@@ -220,7 +220,7 @@
"\<exists>Y t. Y \<subseteq> Z & infinite Y & t < s & (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y --> f{x,y} = t)"
proof -
have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
- by (auto simp add: numeral_2_eq_2 card_2_eq part)
+ using part by (fastsimp simp add: nat_number card_Suc_eq)
obtain Y t
where "Y \<subseteq> Z" "infinite Y" "t < s"
"(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
--- a/src/HOL/SetInterval.thy Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/SetInterval.thy Fri Oct 05 08:38:09 2007 +0200
@@ -414,12 +414,34 @@
by (simp add: atLeastAtMost_def)
lemma bounded_nat_set_is_finite:
- "(ALL i:N. i < (n::nat)) ==> finite N"
+ "(ALL i:N. i < (n::nat)) ==> finite N"
-- {* A bounded set of natural numbers is finite. *}
apply (rule finite_subset)
apply (rule_tac [2] finite_lessThan, auto)
done
+text{* Any subset of an interval of natural numbers the size of the
+subset is exactly that interval. *}
+
+lemma subset_card_intvl_is_intvl:
+ "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
+proof cases
+ assume "finite A"
+ thus "PROP ?P"
+ proof(induct A rule:finite_linorder_induct)
+ case empty thus ?case by auto
+ next
+ case (insert A b)
+ moreover hence "b ~: A" by auto
+ moreover have "A <= {k..<k+card A}" and "b = k+card A"
+ using `b ~: A` insert by fastsimp+
+ ultimately show ?case by auto
+ qed
+next
+ assume "~finite A" thus "PROP ?P" by simp
+qed
+
+
subsubsection {* Cardinality *}
lemma card_lessThan [simp]: "card {..<u} = u"
@@ -495,6 +517,7 @@
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
+
subsubsection {* Cardinality *}
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
--- a/src/HOL/UNITY/Simple/Reach.thy Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy Fri Oct 05 08:38:09 2007 +0200
@@ -121,7 +121,7 @@
apply (unfold metric_def)
apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
prefer 2 apply force
-apply (simp add: card_Suc_Diff1)
+apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
done
lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"
--- a/src/HOL/Wellfounded_Relations.thy Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/Wellfounded_Relations.thy Fri Oct 05 08:38:09 2007 +0200
@@ -107,6 +107,39 @@
shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
by (rule measure_induct_rule [of f P a]) iprover
+(* Should go into Finite_Set, but needs measure.
+ Maybe move Wf_Rel before Finite_Set and finite_psubset to Finite_set?
+*)
+lemma (in linorder)
+ finite_linorder_induct[consumes 1, case_names empty insert]:
+ "finite A \<Longrightarrow> P {} \<Longrightarrow>
+ (!!A b. finite A \<Longrightarrow> ALL a:A. a \<^loc>< b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
+ \<Longrightarrow> P A"
+proof (induct A rule: measure_induct[where f=card])
+ fix A :: "'a set"
+ assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
+ (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a\<^loc><b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
+ \<longrightarrow> P B"
+ and "finite A" and "P {}"
+ and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a \<^loc>< b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
+ show "P A"
+ proof cases
+ assume "A = {}" thus "P A" using `P {}` by simp
+ next
+ let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
+ assume "A \<noteq> {}"
+ with `finite A` have "Max A : A" by auto
+ hence A: "?A = A" using insert_Diff_single insert_absorb by auto
+ note card_Diff1_less[OF `finite A` `Max A : A`]
+ moreover have "finite ?B" using `finite A` by simp
+ ultimately have "P ?B" using `P {}` step IH by blast
+ moreover have "\<forall>a\<in>?B. a \<^loc>< Max A"
+ using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
+ ultimately show "P A"
+ using A insert_Diff_single step[OF `finite ?B`] by fastsimp
+ qed
+qed
+
subsection{*Other Ways of Constructing Wellfounded Relations*}
--- a/src/HOL/ex/set.thy Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/ex/set.thy Fri Oct 05 08:38:09 2007 +0200
@@ -111,6 +111,51 @@
done
+subsection {* A simple party theorem *}
+
+text{* \emph{At any party there are two people who know the same
+number of people}. Provided the party consists of at least two people
+and the knows relation is symmetric. Knowing yourself does not count
+--- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
+at TPHOLs 2007.) *}
+
+lemma equal_number_of_acquaintances:
+assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
+shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
+proof -
+ let ?N = "%a. card(R `` {a} - {a})"
+ let ?n = "card A"
+ have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
+ have 0: "R `` A <= A" using `sym R` `Domain R <= A`
+ unfolding Domain_def sym_def by blast
+ have h: "ALL a:A. R `` {a} <= A" using 0 by blast
+ hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
+ by(blast intro: finite_subset)
+ have sub: "?N ` A <= {0..<?n}"
+ proof -
+ have "ALL a:A. R `` {a} - {a} < A" using h by blast
+ thus ?thesis using psubset_card_mono[OF `finite A`] by auto
+ qed
+ show "~ inj_on ?N A" (is "~ ?I")
+ proof
+ assume ?I
+ hence "?n = card(?N ` A)" by(rule card_image[symmetric])
+ with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
+ using subset_card_intvl_is_intvl[of _ 0] by(auto)
+ have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
+ then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
+ by (auto simp del: 2)
+ have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
+ have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
+ hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
+ hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
+ hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
+ have 4: "finite (A - {a,b})" using `finite A` by simp
+ have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
+ then show False using Nb `card A \<ge> 2` by arith
+ qed
+qed
+
text {*
From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
293-314.