added lemmas
authornipkow
Fri Oct 05 08:38:09 2007 +0200 (2007-10-05)
changeset 24853aab5798e5a33
parent 24852 30da58e0a483
child 24854 0ebcd575d3c6
added lemmas
src/HOL/Finite_Set.thy
src/HOL/Library/Ramsey.thy
src/HOL/SetInterval.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/Wellfounded_Relations.thy
src/HOL/ex/set.thy
     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.8 +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.12 +by (simp add: card_def)
    1.13  
    1.14  lemma card_eq_setsum: "card A = setsum (%x. 1) A"
    1.15  by (simp add: card_def)
    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.36 +by (simp add: card_Diff_singleton)
    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.52 +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.74 +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.5    apply(simp add: part_def, clarify)
     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.4  by (simp add: atLeastAtMost_def)
     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.7 -apply (simp add: card_Suc_Diff1)
     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.