author nipkow Fri Oct 05 08:38:09 2007 +0200 (2007-10-05) changeset 24853 aab5798e5a33 parent 24852 30da58e0a483 child 24854 0ebcd575d3c6
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Library/Ramsey.thy file | annotate | diff | revisions src/HOL/SetInterval.thy file | annotate | diff | revisions src/HOL/UNITY/Simple/Reach.thy file | annotate | diff | revisions src/HOL/Wellfounded_Relations.thy file | annotate | diff | revisions src/HOL/ex/set.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Oct 04 21:11:06 2007 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Fri Oct 05 08:38:09 2007 +0200
1.3 @@ -1505,10 +1505,10 @@
1.4    "card A == setsum (%x. 1::nat) A"
1.5
1.6  lemma card_empty [simp]: "card {} = 0"
1.7 -  by (simp add: card_def)
1.9
1.10  lemma card_infinite [simp]: "~ finite A ==> card A = 0"
1.11 -  by (simp add: card_def)
1.13
1.14  lemma card_eq_setsum: "card A = setsum (%x. 1) A"
1.16 @@ -1529,24 +1529,33 @@
1.17  lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
1.18  by auto
1.19
1.20 +
1.21  lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
1.22  apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
1.23  apply(simp del:insert_Diff_single)
1.24  done
1.25
1.26  lemma card_Diff_singleton:
1.27 -    "finite A ==> x: A ==> card (A - {x}) = card A - 1"
1.28 -  by (simp add: card_Suc_Diff1 [symmetric])
1.29 +  "finite A ==> x: A ==> card (A - {x}) = card A - 1"
1.30 +by (simp add: card_Suc_Diff1 [symmetric])
1.31
1.32  lemma card_Diff_singleton_if:
1.33 -    "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
1.34 -  by (simp add: card_Diff_singleton)
1.35 +  "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
1.37 +
1.38 +lemma card_Diff_insert[simp]:
1.39 +assumes "finite A" and "a:A" and "a ~: B"
1.40 +shows "card(A - insert a B) = card(A - B) - 1"
1.41 +proof -
1.42 +  have "A - insert a B = (A - B) - {a}" using assms by blast
1.43 +  then show ?thesis using assms by(simp add:card_Diff_singleton)
1.44 +qed
1.45
1.46  lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
1.47 -  by (simp add: card_insert_if card_Suc_Diff1)
1.48 +by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
1.49
1.50  lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
1.51 -  by (simp add: card_insert_if)
1.53
1.54  lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
1.55  by (simp add: card_def setsum_mono2)
1.56 @@ -1561,9 +1570,9 @@
1.57    done
1.58
1.59  lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
1.60 -  apply (simp add: psubset_def linorder_not_le [symmetric])
1.61 -  apply (blast dest: card_seteq)
1.62 -  done
1.63 +apply (simp add: psubset_def linorder_not_le [symmetric])
1.64 +apply (blast dest: card_seteq)
1.65 +done
1.66
1.67  lemma card_Un_Int: "finite A ==> finite B
1.68      ==> card A + card B = card (A Un B) + card (A Int B)"
1.69 @@ -1571,7 +1580,7 @@
1.70
1.71  lemma card_Un_disjoint: "finite A ==> finite B
1.72      ==> A Int B = {} ==> card (A Un B) = card A + card B"
1.73 -  by (simp add: card_Un_Int)
1.75
1.76  lemma card_Diff_subset:
1.77    "finite B ==> B <= A ==> card (A - B) = card A - card B"
1.78 @@ -1579,15 +1588,15 @@
1.79
1.80  lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
1.81    apply (rule Suc_less_SucD)
1.82 -  apply (simp add: card_Suc_Diff1)
1.83 +  apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
1.84    done
1.85
1.86  lemma card_Diff2_less:
1.87      "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
1.88    apply (case_tac "x = y")
1.89 -   apply (simp add: card_Diff1_less)
1.90 +   apply (simp add: card_Diff1_less del:card_Diff_insert)
1.91    apply (rule less_trans)
1.92 -   prefer 2 apply (auto intro!: card_Diff1_less)
1.93 +   prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
1.94    done
1.95
1.96  lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
1.97 @@ -1619,32 +1628,39 @@
1.98  text{*The form of a finite set of given cardinality*}
1.99
1.100  lemma card_eq_SucD:
1.101 -  assumes cardeq: "card A = Suc k" and fin: "finite A"
1.102 -  shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k"
1.103 +assumes "card A = Suc k"
1.104 +shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
1.105  proof -
1.106 -  have "card A \<noteq> 0" using cardeq by auto
1.107 -  then obtain b where b: "b \<in> A" using fin by auto
1.108 +  have fin: "finite A" using assms by (auto intro: ccontr)
1.109 +  moreover have "card A \<noteq> 0" using assms by auto
1.110 +  ultimately obtain b where b: "b \<in> A" by auto
1.111    show ?thesis
1.112    proof (intro exI conjI)
1.113      show "A = insert b (A-{b})" using b by blast
1.114      show "b \<notin> A - {b}" by blast
1.115 -    show "card (A - {b}) = k" by (simp add: fin cardeq b card_Diff_singleton)
1.116 +    show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
1.117 +      using assms b fin by(fastsimp dest:mk_disjoint_insert)+
1.118    qed
1.119  qed
1.120
1.121 -
1.122  lemma card_Suc_eq:
1.123 -  "finite A ==>
1.124 -   (card A = Suc k) = (\<exists>b B. A = insert b B & b \<notin> B & card B = k)"
1.125 -by (auto dest!: card_eq_SucD)
1.126 -
1.127 +  "(card A = Suc k) =
1.128 +   (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
1.129 +apply(rule iffI)
1.130 + apply(erule card_eq_SucD)
1.131 +apply(auto)
1.132 +apply(subst card_insert)
1.133 + apply(auto intro:ccontr)
1.134 +done
1.135 +(*
1.136  lemma card_1_eq:
1.137 -  "finite A ==> (card A = Suc 0) = (\<exists>x. A = {x})"
1.138 -by (auto dest!: card_eq_SucD)
1.139 +  "(card A = Suc 0) = (\<exists>x. A = {x})"
1.140 +by (auto dest!: card_eq_SucD)
1.141
1.142  lemma card_2_eq:
1.143 -  "finite A ==> (card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})"
1.144 -by (auto dest!: card_eq_SucD, blast)
1.145 + "(card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})"
1.146 +by (auto dest!: card_eq_SucD)
1.147 +*)
1.148
1.149
1.150  lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"

     2.1 --- a/src/HOL/Library/Ramsey.thy	Thu Oct 04 21:11:06 2007 +0200
2.2 +++ b/src/HOL/Library/Ramsey.thy	Fri Oct 05 08:38:09 2007 +0200
2.3 @@ -64,7 +64,7 @@
2.4        ==> part r s (Y - {y}) (%u. f (insert y u))"
2.6    apply(drule_tac x="insert y X" in spec)
2.7 -  apply(force simp:card_Diff_singleton_if)
2.8 +  apply(force)
2.9    done
2.10
2.11  lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
2.12 @@ -82,7 +82,7 @@
2.13                    (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
2.14  proof (induct r)
2.15    case 0
2.16 -  thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
2.17 +  thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
2.18  next
2.19    case (Suc r)
2.20    show ?case
2.21 @@ -187,7 +187,7 @@
2.22               qed
2.23               moreover
2.24               have "card (X - {ya}) = r"
2.25 -               by (simp add: card_Diff_singleton_if cardX ya)
2.26 +               by (simp add: cardX ya)
2.27               ultimately show ?thesis
2.28                 using pg [of "LEAST x. x \<in> AA"] fields cardX
2.29  	       by (clarsimp simp del:insert_Diff_single)
2.30 @@ -220,7 +220,7 @@
2.31     "\<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)"
2.32  proof -
2.33    have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
2.34 -    by (auto simp add: numeral_2_eq_2 card_2_eq part)
2.35 +    using part by (fastsimp simp add: nat_number card_Suc_eq)
2.36    obtain Y t
2.37      where "Y \<subseteq> Z" "infinite Y" "t < s"
2.38            "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"

     3.1 --- a/src/HOL/SetInterval.thy	Thu Oct 04 21:11:06 2007 +0200
3.2 +++ b/src/HOL/SetInterval.thy	Fri Oct 05 08:38:09 2007 +0200
3.3 @@ -414,12 +414,34 @@
3.5
3.6  lemma bounded_nat_set_is_finite:
3.7 -    "(ALL i:N. i < (n::nat)) ==> finite N"
3.8 +  "(ALL i:N. i < (n::nat)) ==> finite N"
3.9    -- {* A bounded set of natural numbers is finite. *}
3.10    apply (rule finite_subset)
3.11     apply (rule_tac [2] finite_lessThan, auto)
3.12    done
3.13
3.14 +text{* Any subset of an interval of natural numbers the size of the
3.15 +subset is exactly that interval. *}
3.16 +
3.17 +lemma subset_card_intvl_is_intvl:
3.18 +  "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
3.19 +proof cases
3.20 +  assume "finite A"
3.21 +  thus "PROP ?P"
3.22 +  proof(induct A rule:finite_linorder_induct)
3.23 +    case empty thus ?case by auto
3.24 +  next
3.25 +    case (insert A b)
3.26 +    moreover hence "b ~: A" by auto
3.27 +    moreover have "A <= {k..<k+card A}" and "b = k+card A"
3.28 +      using b ~: A insert by fastsimp+
3.29 +    ultimately show ?case by auto
3.30 +  qed
3.31 +next
3.32 +  assume "~finite A" thus "PROP ?P" by simp
3.33 +qed
3.34 +
3.35 +
3.36  subsubsection {* Cardinality *}
3.37
3.38  lemma card_lessThan [simp]: "card {..<u} = u"
3.39 @@ -495,6 +517,7 @@
3.40  lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
3.41    by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
3.42
3.43 +
3.44  subsubsection {* Cardinality *}
3.45
3.46  lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"

     4.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Thu Oct 04 21:11:06 2007 +0200
4.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Fri Oct 05 08:38:09 2007 +0200
4.3 @@ -121,7 +121,7 @@
4.4  apply (unfold metric_def)
4.5  apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
4.6   prefer 2 apply force
4.8 +apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
4.9  done
4.10
4.11  lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"

     5.1 --- a/src/HOL/Wellfounded_Relations.thy	Thu Oct 04 21:11:06 2007 +0200
5.2 +++ b/src/HOL/Wellfounded_Relations.thy	Fri Oct 05 08:38:09 2007 +0200
5.3 @@ -107,6 +107,39 @@
5.4    shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
5.5    by (rule measure_induct_rule [of f P a]) iprover
5.6
5.7 +(* Should go into Finite_Set, but needs measure.
5.8 +   Maybe move Wf_Rel before Finite_Set and finite_psubset to Finite_set?
5.9 +*)
5.10 +lemma (in linorder)
5.11 +  finite_linorder_induct[consumes 1, case_names empty insert]:
5.12 + "finite A \<Longrightarrow> P {} \<Longrightarrow>
5.13 +  (!!A b. finite A \<Longrightarrow> ALL a:A. a \<^loc>< b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
5.14 +  \<Longrightarrow> P A"
5.15 +proof (induct A rule: measure_induct[where f=card])
5.16 +  fix A :: "'a set"
5.17 +  assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
5.18 +                 (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a\<^loc><b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
5.19 +                  \<longrightarrow> P B"
5.20 +  and "finite A" and "P {}"
5.21 +  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a \<^loc>< b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
5.22 +  show "P A"
5.23 +  proof cases
5.24 +    assume "A = {}" thus "P A" using P {} by simp
5.25 +  next
5.26 +    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
5.27 +    assume "A \<noteq> {}"
5.28 +    with finite A have "Max A : A" by auto
5.29 +    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
5.30 +    note card_Diff1_less[OF finite A Max A : A]
5.31 +    moreover have "finite ?B" using finite A by simp
5.32 +    ultimately have "P ?B" using P {} step IH by blast
5.33 +    moreover have "\<forall>a\<in>?B. a \<^loc>< Max A"
5.34 +      using Max_ge[OF finite A A \<noteq> {}] by fastsimp
5.35 +    ultimately show "P A"
5.36 +      using A insert_Diff_single step[OF finite ?B] by fastsimp
5.37 +  qed
5.38 +qed
5.39 +
5.40
5.41  subsection{*Other Ways of Constructing Wellfounded Relations*}
5.42

     6.1 --- a/src/HOL/ex/set.thy	Thu Oct 04 21:11:06 2007 +0200
6.2 +++ b/src/HOL/ex/set.thy	Fri Oct 05 08:38:09 2007 +0200
6.3 @@ -111,6 +111,51 @@
6.4    done
6.5
6.6
6.7 +subsection {* A simple party theorem *}
6.8 +
6.9 +text{* \emph{At any party there are two people who know the same
6.10 +number of people}. Provided the party consists of at least two people
6.11 +and the knows relation is symmetric. Knowing yourself does not count
6.12 +--- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
6.13 +at TPHOLs 2007.) *}
6.14 +
6.15 +lemma equal_number_of_acquaintances:
6.16 +assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
6.17 +shows "\<not> inj_on (%a. card(R  {a} - {a})) A"
6.18 +proof -
6.19 +  let ?N = "%a. card(R  {a} - {a})"
6.20 +  let ?n = "card A"
6.21 +  have "finite A" using card A \<ge> 2 by(auto intro:ccontr)
6.22 +  have 0: "R  A <= A" using sym R Domain R <= A
6.23 +    unfolding Domain_def sym_def by blast
6.24 +  have h: "ALL a:A. R  {a} <= A" using 0 by blast
6.25 +  hence 1: "ALL a:A. finite(R  {a})" using finite A
6.26 +    by(blast intro: finite_subset)
6.27 +  have sub: "?N  A <= {0..<?n}"
6.28 +  proof -
6.29 +    have "ALL a:A. R  {a} - {a} < A" using h by blast
6.30 +    thus ?thesis using psubset_card_mono[OF finite A] by auto
6.31 +  qed
6.32 +  show "~ inj_on ?N A" (is "~ ?I")
6.33 +  proof
6.34 +    assume ?I
6.35 +    hence "?n = card(?N  A)" by(rule card_image[symmetric])
6.36 +    with sub finite A have 2[simp]: "?N  A = {0..<?n}"
6.37 +      using subset_card_intvl_is_intvl[of _ 0] by(auto)
6.38 +    have "0 : ?N  A" and "?n - 1 : ?N  A"  using card A \<ge> 2 by simp+
6.39 +    then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
6.40 +      by (auto simp del: 2)
6.41 +    have "a \<noteq> b" using Na Nb card A \<ge> 2 by auto
6.42 +    have "R  {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
6.43 +    hence "b \<notin> R  {a}" using a\<noteq>b by blast
6.44 +    hence "a \<notin> R  {b}" by (metis Image_singleton_iff assms(2) sym_def)
6.45 +    hence 3: "R  {b} - {b} <= A - {a,b}" using 0 ab by blast
6.46 +    have 4: "finite (A - {a,b})" using finite A by simp
6.47 +    have "?N b <= ?n - 2" using ab a\<noteq>b finite A card_mono[OF 4 3] by simp
6.48 +    then show False using Nb card A \<ge>  2 by arith
6.49 +  qed
6.50 +qed
6.51 +
6.52  text {*
6.53    From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
6.54    293-314.
`