author nipkow Fri, 05 Oct 2007 08:38:09 +0200 changeset 24853 aab5798e5a33 parent 24852 30da58e0a483 child 24854 0ebcd575d3c6
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Library/Ramsey.thy file | annotate | diff | comparison | revisions src/HOL/SetInterval.thy file | annotate | diff | comparison | revisions src/HOL/UNITY/Simple/Reach.thy file | annotate | diff | comparison | revisions src/HOL/Wellfounded_Relations.thy file | annotate | diff | comparison | revisions src/HOL/ex/set.thy file | annotate | diff | comparison | revisions
--- 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"

lemma card_infinite [simp]: "~ finite A ==> card A = 0"

lemma card_eq_setsum: "card A = setsum (%x. 1) A"
@@ -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"

lemma card_Diff_singleton_if:
-    "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
+  "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
+
+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)"

lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
@@ -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"

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 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 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(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 @@

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
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.`