109 apply blast |
109 apply blast |
110 apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) |
110 apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) |
111 done |
111 done |
112 |
112 |
113 |
113 |
|
114 subsection {* A simple party theorem *} |
|
115 |
|
116 text{* \emph{At any party there are two people who know the same |
|
117 number of people}. Provided the party consists of at least two people |
|
118 and the knows relation is symmetric. Knowing yourself does not count |
|
119 --- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk |
|
120 at TPHOLs 2007.) *} |
|
121 |
|
122 lemma equal_number_of_acquaintances: |
|
123 assumes "Domain R <= A" and "sym R" and "card A \<ge> 2" |
|
124 shows "\<not> inj_on (%a. card(R `` {a} - {a})) A" |
|
125 proof - |
|
126 let ?N = "%a. card(R `` {a} - {a})" |
|
127 let ?n = "card A" |
|
128 have "finite A" using `card A \<ge> 2` by(auto intro:ccontr) |
|
129 have 0: "R `` A <= A" using `sym R` `Domain R <= A` |
|
130 unfolding Domain_def sym_def by blast |
|
131 have h: "ALL a:A. R `` {a} <= A" using 0 by blast |
|
132 hence 1: "ALL a:A. finite(R `` {a})" using `finite A` |
|
133 by(blast intro: finite_subset) |
|
134 have sub: "?N ` A <= {0..<?n}" |
|
135 proof - |
|
136 have "ALL a:A. R `` {a} - {a} < A" using h by blast |
|
137 thus ?thesis using psubset_card_mono[OF `finite A`] by auto |
|
138 qed |
|
139 show "~ inj_on ?N A" (is "~ ?I") |
|
140 proof |
|
141 assume ?I |
|
142 hence "?n = card(?N ` A)" by(rule card_image[symmetric]) |
|
143 with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}" |
|
144 using subset_card_intvl_is_intvl[of _ 0] by(auto) |
|
145 have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+ |
|
146 then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1" |
|
147 by (auto simp del: 2) |
|
148 have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto |
|
149 have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff) |
|
150 hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast |
|
151 hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def) |
|
152 hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast |
|
153 have 4: "finite (A - {a,b})" using `finite A` by simp |
|
154 have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp |
|
155 then show False using Nb `card A \<ge> 2` by arith |
|
156 qed |
|
157 qed |
|
158 |
114 text {* |
159 text {* |
115 From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages |
160 From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages |
116 293-314. |
161 293-314. |
117 |
162 |
118 Isabelle can prove the easy examples without any special mechanisms, |
163 Isabelle can prove the easy examples without any special mechanisms, |