moved theory Infinite_Set to Library;
authorwenzelm
Sun Oct 01 18:29:26 2006 +0200 (2006-10-01)
changeset 208096c4fd0b4b63a
parent 20808 96d413f78870
child 20810 3377a830b727
moved theory Infinite_Set to Library;
src/HOL/Complex/ROOT.ML
src/HOL/Hyperreal/Filter.thy
src/HOL/Infinite_Set.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Library.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/ROOT.ML
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/ROOT.ML
src/HOL/Reconstruction.thy
     1.1 --- a/src/HOL/Complex/ROOT.ML	Sun Oct 01 18:29:25 2006 +0200
     1.2 +++ b/src/HOL/Complex/ROOT.ML	Sun Oct 01 18:29:26 2006 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  The Complex Numbers
     1.5  *)
     1.6  
     1.7 +no_document use_thy "Infinite_Set";
     1.8  with_path "../Real"      use_thy "Float";
     1.9  with_path "../Hyperreal" use_thy "Hyperreal";
    1.10  time_use_thy "Complex_Main";
     2.1 --- a/src/HOL/Hyperreal/Filter.thy	Sun Oct 01 18:29:25 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/Filter.thy	Sun Oct 01 18:29:26 2006 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Filters and Ultrafilters *}
     2.5  
     2.6  theory Filter
     2.7 -imports Zorn
     2.8 +imports Zorn Infinite_Set
     2.9  begin
    2.10  
    2.11  subsection {* Definitions and basic properties *}
     3.1 --- a/src/HOL/Infinite_Set.thy	Sun Oct 01 18:29:25 2006 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,470 +0,0 @@
     3.4 -(*  Title:      HOL/Infnite_Set.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Stephan Merz 
     3.7 -*)
     3.8 -
     3.9 -header {* Infinite Sets and Related Concepts*}
    3.10 -
    3.11 -theory Infinite_Set
    3.12 -imports Hilbert_Choice Binomial
    3.13 -begin
    3.14 -
    3.15 -subsection "Infinite Sets"
    3.16 -
    3.17 -text {* Some elementary facts about infinite sets, mostly by Stefan Merz.
    3.18 -Beware! Because "infinite" merely abbreviates a negation, these lemmas may
    3.19 -not work well with "blast". *}
    3.20 -
    3.21 -abbreviation
    3.22 -  infinite :: "'a set \<Rightarrow> bool"
    3.23 -  "infinite S == \<not> finite S"
    3.24 -
    3.25 -text {*
    3.26 -  Infinite sets are non-empty, and if we remove some elements
    3.27 -  from an infinite set, the result is still infinite.
    3.28 -*}
    3.29 -
    3.30 -lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
    3.31 -  by auto
    3.32 -
    3.33 -lemma infinite_remove:
    3.34 -  "infinite S \<Longrightarrow> infinite (S - {a})"
    3.35 -  by simp
    3.36 -
    3.37 -lemma Diff_infinite_finite:
    3.38 -  assumes T: "finite T" and S: "infinite S"
    3.39 -  shows "infinite (S-T)"
    3.40 -  using T
    3.41 -proof induct
    3.42 -  from S
    3.43 -  show "infinite (S - {})" by auto
    3.44 -next
    3.45 -  fix T x
    3.46 -  assume ih: "infinite (S-T)"
    3.47 -  have "S - (insert x T) = (S-T) - {x}"
    3.48 -    by (rule Diff_insert)
    3.49 -  with ih
    3.50 -  show "infinite (S - (insert x T))"
    3.51 -    by (simp add: infinite_remove)
    3.52 -qed
    3.53 -
    3.54 -lemma Un_infinite:
    3.55 -  "infinite S \<Longrightarrow> infinite (S \<union> T)"
    3.56 -  by simp
    3.57 -
    3.58 -lemma infinite_super:
    3.59 -  assumes T: "S \<subseteq> T" and S: "infinite S"
    3.60 -  shows "infinite T"
    3.61 -proof (rule ccontr)
    3.62 -  assume "\<not>(infinite T)"
    3.63 -  with T have "finite S" by (simp add: finite_subset)
    3.64 -  with S show False by simp
    3.65 -qed
    3.66 -
    3.67 -text {*
    3.68 -  As a concrete example, we prove that the set of natural
    3.69 -  numbers is infinite.
    3.70 -*}
    3.71 -
    3.72 -lemma finite_nat_bounded:
    3.73 -  assumes S: "finite (S::nat set)"
    3.74 -  shows "\<exists>k. S \<subseteq> {..<k}" (is "\<exists>k. ?bounded S k")
    3.75 -using S
    3.76 -proof (induct)
    3.77 -  have "?bounded {} 0" by simp
    3.78 -  thus "\<exists>k. ?bounded {} k" ..
    3.79 -next
    3.80 -  fix S x
    3.81 -  assume "\<exists>k. ?bounded S k"
    3.82 -  then obtain k where k: "?bounded S k" ..
    3.83 -  show "\<exists>k. ?bounded (insert x S) k"
    3.84 -  proof (cases "x<k")
    3.85 -    case True
    3.86 -    with k show ?thesis by auto
    3.87 -  next
    3.88 -    case False
    3.89 -    with k have "?bounded S (Suc x)" by auto
    3.90 -    thus ?thesis by auto
    3.91 -  qed
    3.92 -qed
    3.93 -
    3.94 -lemma finite_nat_iff_bounded:
    3.95 -  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})" (is "?lhs = ?rhs")
    3.96 -proof
    3.97 -  assume ?lhs
    3.98 -  thus ?rhs by (rule finite_nat_bounded)
    3.99 -next
   3.100 -  assume ?rhs
   3.101 -  then obtain k where "S \<subseteq> {..<k}" ..
   3.102 -  thus "finite S"
   3.103 -    by (rule finite_subset, simp)
   3.104 -qed
   3.105 -
   3.106 -lemma finite_nat_iff_bounded_le:
   3.107 -  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})" (is "?lhs = ?rhs")
   3.108 -proof
   3.109 -  assume ?lhs
   3.110 -  then obtain k where "S \<subseteq> {..<k}" 
   3.111 -    by (blast dest: finite_nat_bounded)
   3.112 -  hence "S \<subseteq> {..k}" by auto
   3.113 -  thus ?rhs ..
   3.114 -next
   3.115 -  assume ?rhs
   3.116 -  then obtain k where "S \<subseteq> {..k}" ..
   3.117 -  thus "finite S"
   3.118 -    by (rule finite_subset, simp)
   3.119 -qed
   3.120 -
   3.121 -lemma infinite_nat_iff_unbounded:
   3.122 -  "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
   3.123 -  (is "?lhs = ?rhs")
   3.124 -proof
   3.125 -  assume inf: ?lhs
   3.126 -  show ?rhs
   3.127 -  proof (rule ccontr)
   3.128 -    assume "\<not> ?rhs"
   3.129 -    then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
   3.130 -    hence "S \<subseteq> {..m}"
   3.131 -      by (auto simp add: sym[OF linorder_not_less])
   3.132 -    with inf show "False" 
   3.133 -      by (simp add: finite_nat_iff_bounded_le)
   3.134 -  qed
   3.135 -next
   3.136 -  assume unbounded: ?rhs
   3.137 -  show ?lhs
   3.138 -  proof
   3.139 -    assume "finite S"
   3.140 -    then obtain m where "S \<subseteq> {..m}"
   3.141 -      by (auto simp add: finite_nat_iff_bounded_le)
   3.142 -    hence "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
   3.143 -    with unbounded show "False" by blast
   3.144 -  qed
   3.145 -qed
   3.146 -
   3.147 -lemma infinite_nat_iff_unbounded_le:
   3.148 -  "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
   3.149 -  (is "?lhs = ?rhs")
   3.150 -proof
   3.151 -  assume inf: ?lhs
   3.152 -  show ?rhs
   3.153 -  proof
   3.154 -    fix m
   3.155 -    from inf obtain n where "m<n \<and> n\<in>S"
   3.156 -      by (auto simp add: infinite_nat_iff_unbounded)
   3.157 -    hence "m\<le>n \<and> n\<in>S" by auto
   3.158 -    thus "\<exists>n. m \<le> n \<and> n \<in> S" ..
   3.159 -  qed
   3.160 -next
   3.161 -  assume unbounded: ?rhs
   3.162 -  show ?lhs
   3.163 -  proof (auto simp add: infinite_nat_iff_unbounded)
   3.164 -    fix m
   3.165 -    from unbounded obtain n where "(Suc m)\<le>n \<and> n\<in>S"
   3.166 -      by blast
   3.167 -    hence "m<n \<and> n\<in>S" by auto
   3.168 -    thus "\<exists>n. m < n \<and> n \<in> S" ..
   3.169 -  qed
   3.170 -qed
   3.171 -
   3.172 -text {*
   3.173 -  For a set of natural numbers to be infinite, it is enough
   3.174 -  to know that for any number larger than some @{text k}, there
   3.175 -  is some larger number that is an element of the set.
   3.176 -*}
   3.177 -
   3.178 -lemma unbounded_k_infinite:
   3.179 -  assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
   3.180 -  shows "infinite (S::nat set)"
   3.181 -proof (auto simp add: infinite_nat_iff_unbounded)
   3.182 -  fix m show "\<exists>n. m<n \<and> n\<in>S"
   3.183 -  proof (cases "k<m")
   3.184 -    case True
   3.185 -    with k show ?thesis by blast
   3.186 -  next
   3.187 -    case False
   3.188 -    from k obtain n where "Suc k < n \<and> n\<in>S" by auto
   3.189 -    with False have "m<n \<and> n\<in>S" by auto
   3.190 -    thus ?thesis ..
   3.191 -  qed
   3.192 -qed
   3.193 -
   3.194 -theorem nat_infinite [simp]:
   3.195 -  "infinite (UNIV :: nat set)"
   3.196 -by (auto simp add: infinite_nat_iff_unbounded)
   3.197 -
   3.198 -theorem nat_not_finite [elim]:
   3.199 -  "finite (UNIV::nat set) \<Longrightarrow> R"
   3.200 -by simp
   3.201 -
   3.202 -text {*
   3.203 -  Every infinite set contains a countable subset. More precisely
   3.204 -  we show that a set @{text S} is infinite if and only if there exists 
   3.205 -  an injective function from the naturals into @{text S}.
   3.206 -*}
   3.207 -
   3.208 -lemma range_inj_infinite:
   3.209 -  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
   3.210 -proof
   3.211 -  assume "inj f"
   3.212 -    and  "finite (range f)"
   3.213 -  hence "finite (UNIV::nat set)"
   3.214 -    by (auto intro: finite_imageD simp del: nat_infinite)
   3.215 -  thus "False" by simp
   3.216 -qed
   3.217 -
   3.218 -text {*
   3.219 -  The ``only if'' direction is harder because it requires the
   3.220 -  construction of a sequence of pairwise different elements of
   3.221 -  an infinite set @{text S}. The idea is to construct a sequence of
   3.222 -  non-empty and infinite subsets of @{text S} obtained by successively
   3.223 -  removing elements of @{text S}.
   3.224 -*}
   3.225 -
   3.226 -lemma linorder_injI:
   3.227 -  assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
   3.228 -  shows "inj f"
   3.229 -proof (rule inj_onI)
   3.230 -  fix x y
   3.231 -  assume f_eq: "f x = f y"
   3.232 -  show "x = y"
   3.233 -  proof (rule linorder_cases)
   3.234 -    assume "x < y"
   3.235 -    with hyp have "f x \<noteq> f y" by blast
   3.236 -    with f_eq show ?thesis by simp
   3.237 -  next
   3.238 -    assume "x = y"
   3.239 -    thus ?thesis .
   3.240 -  next
   3.241 -    assume "y < x"
   3.242 -    with hyp have "f y \<noteq> f x" by blast
   3.243 -    with f_eq show ?thesis by simp
   3.244 -  qed
   3.245 -qed
   3.246 -
   3.247 -lemma infinite_countable_subset:
   3.248 -  assumes inf: "infinite (S::'a set)"
   3.249 -  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   3.250 -proof -
   3.251 -  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
   3.252 -  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   3.253 -  have Sseq_inf: "\<And>n. infinite (Sseq n)"
   3.254 -  proof -
   3.255 -    fix n
   3.256 -    show "infinite (Sseq n)"
   3.257 -    proof (induct n)
   3.258 -      from inf show "infinite (Sseq 0)"
   3.259 -	by (simp add: Sseq_def)
   3.260 -    next
   3.261 -      fix n
   3.262 -      assume "infinite (Sseq n)" thus "infinite (Sseq (Suc n))"
   3.263 -	by (simp add: Sseq_def infinite_remove)
   3.264 -    qed
   3.265 -  qed
   3.266 -  have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
   3.267 -  proof -
   3.268 -    fix n
   3.269 -    show "Sseq n \<subseteq> S"
   3.270 -      by (induct n, auto simp add: Sseq_def)
   3.271 -  qed
   3.272 -  have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
   3.273 -  proof -
   3.274 -    fix n
   3.275 -    show "pick n \<in> Sseq n"
   3.276 -    proof (unfold pick_def, rule someI_ex)
   3.277 -      from Sseq_inf have "infinite (Sseq n)" .
   3.278 -      hence "Sseq n \<noteq> {}" by auto
   3.279 -      thus "\<exists>x. x \<in> Sseq n" by auto
   3.280 -    qed
   3.281 -  qed
   3.282 -  with Sseq_S have rng: "range pick \<subseteq> S"
   3.283 -    by auto
   3.284 -  have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
   3.285 -  proof -
   3.286 -    fix n m
   3.287 -    show "pick n \<notin> Sseq (n + Suc m)"
   3.288 -      by (induct m, auto simp add: Sseq_def pick_def)
   3.289 -  qed
   3.290 -  have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   3.291 -  proof -
   3.292 -    fix n m
   3.293 -    from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   3.294 -    moreover from pick_Sseq_gt
   3.295 -    have "pick n \<notin> Sseq (n + Suc m)" .
   3.296 -    ultimately show "pick n \<noteq> pick (n + Suc m)"
   3.297 -      by auto
   3.298 -  qed
   3.299 -  have inj: "inj pick"
   3.300 -  proof (rule linorder_injI)
   3.301 -    show "!!i j. i<(j::nat) ==> pick i \<noteq> pick j"
   3.302 -    proof
   3.303 -      fix i j
   3.304 -      assume ij: "i<(j::nat)"
   3.305 -	and eq: "pick i = pick j"
   3.306 -      from ij obtain k where "j = i + (Suc k)"
   3.307 -	by (auto simp add: less_iff_Suc_add)
   3.308 -      with pick_pick have "pick i \<noteq> pick j" by simp
   3.309 -      with eq show "False" by simp
   3.310 -    qed
   3.311 -  qed
   3.312 -  from rng inj show ?thesis by auto
   3.313 -qed
   3.314 -
   3.315 -theorem infinite_iff_countable_subset:
   3.316 -  "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   3.317 -  (is "?lhs = ?rhs")
   3.318 -by (auto simp add: infinite_countable_subset
   3.319 -                   range_inj_infinite infinite_super)
   3.320 -
   3.321 -text {*
   3.322 -  For any function with infinite domain and finite range
   3.323 -  there is some element that is the image of infinitely
   3.324 -  many domain elements. In particular, any infinite sequence
   3.325 -  of elements from a finite set contains some element that
   3.326 -  occurs infinitely often.
   3.327 -*}
   3.328 -
   3.329 -theorem inf_img_fin_dom:
   3.330 -  assumes img: "finite (f`A)" and dom: "infinite A"
   3.331 -  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   3.332 -proof (rule ccontr)
   3.333 -  assume "\<not> (\<exists>y\<in>f ` A. infinite (f -` {y}))"
   3.334 -  with img have "finite (UN y:f`A. f -` {y})"
   3.335 -    by (blast intro: finite_UN_I)
   3.336 -  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   3.337 -  moreover note dom
   3.338 -  ultimately show "False"
   3.339 -    by (simp add: infinite_super)
   3.340 -qed
   3.341 -
   3.342 -theorems inf_img_fin_domE = inf_img_fin_dom[THEN bexE]
   3.343 -
   3.344 -
   3.345 -subsection "Infinitely Many and Almost All"
   3.346 -
   3.347 -text {*
   3.348 -  We often need to reason about the existence of infinitely many
   3.349 -  (resp., all but finitely many) objects satisfying some predicate,
   3.350 -  so we introduce corresponding binders and their proof rules.
   3.351 -*}
   3.352 -
   3.353 -definition
   3.354 -  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "INF " 10)
   3.355 -  INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
   3.356 -  Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
   3.357 -  MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
   3.358 -
   3.359 -const_syntax (xsymbols)
   3.360 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
   3.361 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   3.362 -
   3.363 -const_syntax (HTML output)
   3.364 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
   3.365 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   3.366 -
   3.367 -lemma INF_EX:
   3.368 -  "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   3.369 -  unfolding INF_def
   3.370 -proof (rule ccontr)
   3.371 -  assume inf: "infinite {x. P x}"
   3.372 -    and notP: "\<not>(\<exists>x. P x)"
   3.373 -  from notP have "{x. P x} = {}" by simp
   3.374 -  hence "finite {x. P x}" by simp
   3.375 -  with inf show "False" by simp
   3.376 -qed
   3.377 -
   3.378 -lemma MOST_iff_finiteNeg:
   3.379 -  "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
   3.380 -by (simp add: MOST_def INF_def)
   3.381 -
   3.382 -lemma ALL_MOST:
   3.383 -  "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   3.384 -by (simp add: MOST_iff_finiteNeg)
   3.385 -
   3.386 -lemma INF_mono:
   3.387 -  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   3.388 -  shows "\<exists>\<^sub>\<infinity>x. Q x"
   3.389 -proof -
   3.390 -  from inf have "infinite {x. P x}" by (unfold INF_def)
   3.391 -  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   3.392 -  ultimately show ?thesis
   3.393 -    by (simp add: INF_def infinite_super)
   3.394 -qed
   3.395 -
   3.396 -lemma MOST_mono:
   3.397 -  "\<lbrakk> \<forall>\<^sub>\<infinity>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   3.398 -by (unfold MOST_def, blast intro: INF_mono)
   3.399 -
   3.400 -lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   3.401 -by (simp add: INF_def infinite_nat_iff_unbounded)
   3.402 -
   3.403 -lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   3.404 -by (simp add: INF_def infinite_nat_iff_unbounded_le)
   3.405 -
   3.406 -lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   3.407 -by (simp add: MOST_def INF_nat)
   3.408 -
   3.409 -lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   3.410 -by (simp add: MOST_def INF_nat_le)
   3.411 -
   3.412 -
   3.413 -subsection "Enumeration of an Infinite Set"
   3.414 -
   3.415 -text{*The set's element type must be wellordered (e.g. the natural numbers)*}
   3.416 -consts
   3.417 -  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
   3.418 -
   3.419 -primrec
   3.420 -  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   3.421 -  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   3.422 -
   3.423 -lemma enumerate_Suc':
   3.424 -   "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   3.425 -by simp
   3.426 -
   3.427 -lemma enumerate_in_set [rule_format]: "\<forall>S. infinite S --> enumerate S n : S"
   3.428 -apply (induct n) 
   3.429 - apply (force intro: LeastI dest!:infinite_imp_nonempty)
   3.430 -apply (auto iff: finite_Diff_singleton) 
   3.431 -done
   3.432 -
   3.433 -declare enumerate_0 [simp del] enumerate_Suc [simp del]
   3.434 -
   3.435 -lemma enumerate_step [rule_format]:
   3.436 -     "\<forall>S. infinite S --> enumerate S n < enumerate S (Suc n)"
   3.437 -apply (induct n, clarify) 
   3.438 - apply (rule order_le_neq_trans)
   3.439 -  apply (simp add: enumerate_0 Least_le enumerate_in_set) 
   3.440 - apply (simp only: enumerate_Suc') 
   3.441 - apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   3.442 -  apply (blast intro: sym)
   3.443 - apply (simp add: enumerate_in_set del: Diff_iff) 
   3.444 -apply (simp add: enumerate_Suc') 
   3.445 -done
   3.446 -
   3.447 -lemma enumerate_mono: "[|m<n; infinite S|] ==> enumerate S m < enumerate S n"
   3.448 -apply (erule less_Suc_induct) 
   3.449 -apply (auto intro: enumerate_step) 
   3.450 -done
   3.451 -
   3.452 -
   3.453 -subsection "Miscellaneous"
   3.454 -
   3.455 -text {*
   3.456 -  A few trivial lemmas about sets that contain at most one element.
   3.457 -  These simplify the reasoning about deterministic automata.
   3.458 -*}
   3.459 -
   3.460 -definition
   3.461 -  atmost_one :: "'a set \<Rightarrow> bool"
   3.462 -  "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
   3.463 -
   3.464 -lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"
   3.465 -  by (simp add: atmost_one_def)
   3.466 -
   3.467 -lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   3.468 -  by (simp add: atmost_one_def)
   3.469 -
   3.470 -lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x"
   3.471 -  by (simp add: atmost_one_def)
   3.472 -
   3.473 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Infinite_Set.thy	Sun Oct 01 18:29:26 2006 +0200
     4.3 @@ -0,0 +1,468 @@
     4.4 +(*  Title:      HOL/Infnite_Set.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Stephan Merz
     4.7 +*)
     4.8 +
     4.9 +header {* Infinite Sets and Related Concepts *}
    4.10 +
    4.11 +theory Infinite_Set
    4.12 +imports Hilbert_Choice Binomial
    4.13 +begin
    4.14 +
    4.15 +subsection "Infinite Sets"
    4.16 +
    4.17 +text {*
    4.18 +  Some elementary facts about infinite sets, mostly by Stefan Merz.
    4.19 +  Beware! Because "infinite" merely abbreviates a negation, these
    4.20 +  lemmas may not work well with @{text "blast"}.
    4.21 +*}
    4.22 +
    4.23 +abbreviation
    4.24 +  infinite :: "'a set \<Rightarrow> bool"
    4.25 +  "infinite S == \<not> finite S"
    4.26 +
    4.27 +text {*
    4.28 +  Infinite sets are non-empty, and if we remove some elements from an
    4.29 +  infinite set, the result is still infinite.
    4.30 +*}
    4.31 +
    4.32 +lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
    4.33 +  by auto
    4.34 +
    4.35 +lemma infinite_remove:
    4.36 +  "infinite S \<Longrightarrow> infinite (S - {a})"
    4.37 +  by simp
    4.38 +
    4.39 +lemma Diff_infinite_finite:
    4.40 +  assumes T: "finite T" and S: "infinite S"
    4.41 +  shows "infinite (S - T)"
    4.42 +  using T
    4.43 +proof induct
    4.44 +  from S
    4.45 +  show "infinite (S - {})" by auto
    4.46 +next
    4.47 +  fix T x
    4.48 +  assume ih: "infinite (S - T)"
    4.49 +  have "S - (insert x T) = (S - T) - {x}"
    4.50 +    by (rule Diff_insert)
    4.51 +  with ih
    4.52 +  show "infinite (S - (insert x T))"
    4.53 +    by (simp add: infinite_remove)
    4.54 +qed
    4.55 +
    4.56 +lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
    4.57 +  by simp
    4.58 +
    4.59 +lemma infinite_super:
    4.60 +  assumes T: "S \<subseteq> T" and S: "infinite S"
    4.61 +  shows "infinite T"
    4.62 +proof
    4.63 +  assume "finite T"
    4.64 +  with T have "finite S" by (simp add: finite_subset)
    4.65 +  with S show False by simp
    4.66 +qed
    4.67 +
    4.68 +text {*
    4.69 +  As a concrete example, we prove that the set of natural numbers is
    4.70 +  infinite.
    4.71 +*}
    4.72 +
    4.73 +lemma finite_nat_bounded:
    4.74 +  assumes S: "finite (S::nat set)"
    4.75 +  shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
    4.76 +using S
    4.77 +proof induct
    4.78 +  have "?bounded {} 0" by simp
    4.79 +  then show "\<exists>k. ?bounded {} k" ..
    4.80 +next
    4.81 +  fix S x
    4.82 +  assume "\<exists>k. ?bounded S k"
    4.83 +  then obtain k where k: "?bounded S k" ..
    4.84 +  show "\<exists>k. ?bounded (insert x S) k"
    4.85 +  proof (cases "x < k")
    4.86 +    case True
    4.87 +    with k show ?thesis by auto
    4.88 +  next
    4.89 +    case False
    4.90 +    with k have "?bounded S (Suc x)" by auto
    4.91 +    then show ?thesis by auto
    4.92 +  qed
    4.93 +qed
    4.94 +
    4.95 +lemma finite_nat_iff_bounded:
    4.96 +  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
    4.97 +proof
    4.98 +  assume ?lhs
    4.99 +  then show ?rhs by (rule finite_nat_bounded)
   4.100 +next
   4.101 +  assume ?rhs
   4.102 +  then obtain k where "S \<subseteq> {..<k}" ..
   4.103 +  then show "finite S"
   4.104 +    by (rule finite_subset) simp
   4.105 +qed
   4.106 +
   4.107 +lemma finite_nat_iff_bounded_le:
   4.108 +  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
   4.109 +proof
   4.110 +  assume ?lhs
   4.111 +  then obtain k where "S \<subseteq> {..<k}"
   4.112 +    by (blast dest: finite_nat_bounded)
   4.113 +  then have "S \<subseteq> {..k}" by auto
   4.114 +  then show ?rhs ..
   4.115 +next
   4.116 +  assume ?rhs
   4.117 +  then obtain k where "S \<subseteq> {..k}" ..
   4.118 +  then show "finite S"
   4.119 +    by (rule finite_subset) simp
   4.120 +qed
   4.121 +
   4.122 +lemma infinite_nat_iff_unbounded:
   4.123 +  "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
   4.124 +  (is "?lhs = ?rhs")
   4.125 +proof
   4.126 +  assume ?lhs
   4.127 +  show ?rhs
   4.128 +  proof (rule ccontr)
   4.129 +    assume "\<not> ?rhs"
   4.130 +    then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
   4.131 +    then have "S \<subseteq> {..m}"
   4.132 +      by (auto simp add: sym [OF linorder_not_less])
   4.133 +    with `?lhs` show False
   4.134 +      by (simp add: finite_nat_iff_bounded_le)
   4.135 +  qed
   4.136 +next
   4.137 +  assume ?rhs
   4.138 +  show ?lhs
   4.139 +  proof
   4.140 +    assume "finite S"
   4.141 +    then obtain m where "S \<subseteq> {..m}"
   4.142 +      by (auto simp add: finite_nat_iff_bounded_le)
   4.143 +    then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
   4.144 +    with `?rhs` show False by blast
   4.145 +  qed
   4.146 +qed
   4.147 +
   4.148 +lemma infinite_nat_iff_unbounded_le:
   4.149 +  "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
   4.150 +  (is "?lhs = ?rhs")
   4.151 +proof
   4.152 +  assume ?lhs
   4.153 +  show ?rhs
   4.154 +  proof
   4.155 +    fix m
   4.156 +    from `?lhs` obtain n where "m<n \<and> n\<in>S"
   4.157 +      by (auto simp add: infinite_nat_iff_unbounded)
   4.158 +    then have "m\<le>n \<and> n\<in>S" by simp
   4.159 +    then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
   4.160 +  qed
   4.161 +next
   4.162 +  assume ?rhs
   4.163 +  show ?lhs
   4.164 +  proof (auto simp add: infinite_nat_iff_unbounded)
   4.165 +    fix m
   4.166 +    from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
   4.167 +      by blast
   4.168 +    then have "m<n \<and> n\<in>S" by simp
   4.169 +    then show "\<exists>n. m < n \<and> n \<in> S" ..
   4.170 +  qed
   4.171 +qed
   4.172 +
   4.173 +text {*
   4.174 +  For a set of natural numbers to be infinite, it is enough to know
   4.175 +  that for any number larger than some @{text k}, there is some larger
   4.176 +  number that is an element of the set.
   4.177 +*}
   4.178 +
   4.179 +lemma unbounded_k_infinite:
   4.180 +  assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
   4.181 +  shows "infinite (S::nat set)"
   4.182 +proof -
   4.183 +  {
   4.184 +    fix m have "\<exists>n. m<n \<and> n\<in>S"
   4.185 +    proof (cases "k<m")
   4.186 +      case True
   4.187 +      with k show ?thesis by blast
   4.188 +    next
   4.189 +      case False
   4.190 +      from k obtain n where "Suc k < n \<and> n\<in>S" by auto
   4.191 +      with False have "m<n \<and> n\<in>S" by auto
   4.192 +      then show ?thesis ..
   4.193 +    qed
   4.194 +  }
   4.195 +  then show ?thesis
   4.196 +    by (auto simp add: infinite_nat_iff_unbounded)
   4.197 +qed
   4.198 +
   4.199 +lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
   4.200 +  by (auto simp add: infinite_nat_iff_unbounded)
   4.201 +
   4.202 +lemma nat_not_finite [elim]: "finite (UNIV::nat set) \<Longrightarrow> R"
   4.203 +  by simp
   4.204 +
   4.205 +text {*
   4.206 +  Every infinite set contains a countable subset. More precisely we
   4.207 +  show that a set @{text S} is infinite if and only if there exists an
   4.208 +  injective function from the naturals into @{text S}.
   4.209 +*}
   4.210 +
   4.211 +lemma range_inj_infinite:
   4.212 +  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
   4.213 +proof
   4.214 +  assume "inj f"
   4.215 +    and  "finite (range f)"
   4.216 +  then have "finite (UNIV::nat set)"
   4.217 +    by (auto intro: finite_imageD simp del: nat_infinite)
   4.218 +  then show False by simp
   4.219 +qed
   4.220 +
   4.221 +text {*
   4.222 +  The ``only if'' direction is harder because it requires the
   4.223 +  construction of a sequence of pairwise different elements of an
   4.224 +  infinite set @{text S}. The idea is to construct a sequence of
   4.225 +  non-empty and infinite subsets of @{text S} obtained by successively
   4.226 +  removing elements of @{text S}.
   4.227 +*}
   4.228 +
   4.229 +lemma linorder_injI:
   4.230 +  assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
   4.231 +  shows "inj f"
   4.232 +proof (rule inj_onI)
   4.233 +  fix x y
   4.234 +  assume f_eq: "f x = f y"
   4.235 +  show "x = y"
   4.236 +  proof (rule linorder_cases)
   4.237 +    assume "x < y"
   4.238 +    with hyp have "f x \<noteq> f y" by blast
   4.239 +    with f_eq show ?thesis by simp
   4.240 +  next
   4.241 +    assume "x = y"
   4.242 +    then show ?thesis .
   4.243 +  next
   4.244 +    assume "y < x"
   4.245 +    with hyp have "f y \<noteq> f x" by blast
   4.246 +    with f_eq show ?thesis by simp
   4.247 +  qed
   4.248 +qed
   4.249 +
   4.250 +lemma infinite_countable_subset:
   4.251 +  assumes inf: "infinite (S::'a set)"
   4.252 +  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   4.253 +proof -
   4.254 +  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
   4.255 +  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   4.256 +  have Sseq_inf: "\<And>n. infinite (Sseq n)"
   4.257 +  proof -
   4.258 +    fix n
   4.259 +    show "infinite (Sseq n)"
   4.260 +    proof (induct n)
   4.261 +      from inf show "infinite (Sseq 0)"
   4.262 +        by (simp add: Sseq_def)
   4.263 +    next
   4.264 +      fix n
   4.265 +      assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
   4.266 +        by (simp add: Sseq_def infinite_remove)
   4.267 +    qed
   4.268 +  qed
   4.269 +  have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
   4.270 +  proof -
   4.271 +    fix n
   4.272 +    show "Sseq n \<subseteq> S"
   4.273 +      by (induct n) (auto simp add: Sseq_def)
   4.274 +  qed
   4.275 +  have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
   4.276 +  proof -
   4.277 +    fix n
   4.278 +    show "pick n \<in> Sseq n"
   4.279 +    proof (unfold pick_def, rule someI_ex)
   4.280 +      from Sseq_inf have "infinite (Sseq n)" .
   4.281 +      then have "Sseq n \<noteq> {}" by auto
   4.282 +      then show "\<exists>x. x \<in> Sseq n" by auto
   4.283 +    qed
   4.284 +  qed
   4.285 +  with Sseq_S have rng: "range pick \<subseteq> S"
   4.286 +    by auto
   4.287 +  have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
   4.288 +  proof -
   4.289 +    fix n m
   4.290 +    show "pick n \<notin> Sseq (n + Suc m)"
   4.291 +      by (induct m) (auto simp add: Sseq_def pick_def)
   4.292 +  qed
   4.293 +  have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   4.294 +  proof -
   4.295 +    fix n m
   4.296 +    from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   4.297 +    moreover from pick_Sseq_gt
   4.298 +    have "pick n \<notin> Sseq (n + Suc m)" .
   4.299 +    ultimately show "pick n \<noteq> pick (n + Suc m)"
   4.300 +      by auto
   4.301 +  qed
   4.302 +  have inj: "inj pick"
   4.303 +  proof (rule linorder_injI)
   4.304 +    fix i j :: nat
   4.305 +    assume "i < j"
   4.306 +    show "pick i \<noteq> pick j"
   4.307 +    proof
   4.308 +      assume eq: "pick i = pick j"
   4.309 +      from `i < j` obtain k where "j = i + Suc k"
   4.310 +        by (auto simp add: less_iff_Suc_add)
   4.311 +      with pick_pick have "pick i \<noteq> pick j" by simp
   4.312 +      with eq show False by simp
   4.313 +    qed
   4.314 +  qed
   4.315 +  from rng inj show ?thesis by auto
   4.316 +qed
   4.317 +
   4.318 +lemma infinite_iff_countable_subset:
   4.319 +    "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   4.320 +  by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
   4.321 +
   4.322 +text {*
   4.323 +  For any function with infinite domain and finite range there is some
   4.324 +  element that is the image of infinitely many domain elements.  In
   4.325 +  particular, any infinite sequence of elements from a finite set
   4.326 +  contains some element that occurs infinitely often.
   4.327 +*}
   4.328 +
   4.329 +lemma inf_img_fin_dom:
   4.330 +  assumes img: "finite (f`A)" and dom: "infinite A"
   4.331 +  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   4.332 +proof (rule ccontr)
   4.333 +  assume "\<not> ?thesis"
   4.334 +  with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
   4.335 +  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   4.336 +  moreover note dom
   4.337 +  ultimately show False by (simp add: infinite_super)
   4.338 +qed
   4.339 +
   4.340 +lemma inf_img_fin_domE:
   4.341 +  assumes "finite (f`A)" and "infinite A"
   4.342 +  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   4.343 +  using prems by (blast dest: inf_img_fin_dom)
   4.344 +
   4.345 +
   4.346 +subsection "Infinitely Many and Almost All"
   4.347 +
   4.348 +text {*
   4.349 +  We often need to reason about the existence of infinitely many
   4.350 +  (resp., all but finitely many) objects satisfying some predicate, so
   4.351 +  we introduce corresponding binders and their proof rules.
   4.352 +*}
   4.353 +
   4.354 +definition
   4.355 +  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "INF " 10)
   4.356 +  "Inf_many P = infinite {x. P x}"
   4.357 +  Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
   4.358 +  "Alm_all P = (\<not> (INF x. \<not> P x))"
   4.359 +
   4.360 +const_syntax (xsymbols)
   4.361 +  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
   4.362 +  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   4.363 +
   4.364 +const_syntax (HTML output)
   4.365 +  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
   4.366 +  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   4.367 +
   4.368 +lemma INF_EX:
   4.369 +  "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   4.370 +  unfolding Inf_many_def
   4.371 +proof (rule ccontr)
   4.372 +  assume inf: "infinite {x. P x}"
   4.373 +  assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
   4.374 +  then have "finite {x. P x}" by simp
   4.375 +  with inf show False by simp
   4.376 +qed
   4.377 +
   4.378 +lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
   4.379 +  by (simp add: Alm_all_def Inf_many_def)
   4.380 +
   4.381 +lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   4.382 +  by (simp add: MOST_iff_finiteNeg)
   4.383 +
   4.384 +lemma INF_mono:
   4.385 +  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   4.386 +  shows "\<exists>\<^sub>\<infinity>x. Q x"
   4.387 +proof -
   4.388 +  from inf have "infinite {x. P x}" unfolding Inf_many_def .
   4.389 +  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   4.390 +  ultimately show ?thesis
   4.391 +    by (simp add: Inf_many_def infinite_super)
   4.392 +qed
   4.393 +
   4.394 +lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   4.395 +  unfolding Alm_all_def by (blast intro: INF_mono)
   4.396 +
   4.397 +lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   4.398 +  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   4.399 +
   4.400 +lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   4.401 +  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   4.402 +
   4.403 +lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   4.404 +  by (simp add: Alm_all_def INF_nat)
   4.405 +
   4.406 +lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   4.407 +  by (simp add: Alm_all_def INF_nat_le)
   4.408 +
   4.409 +
   4.410 +subsection "Enumeration of an Infinite Set"
   4.411 +
   4.412 +text {*
   4.413 +  The set's element type must be wellordered (e.g. the natural numbers).
   4.414 +*}
   4.415 +
   4.416 +consts
   4.417 +  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
   4.418 +primrec
   4.419 +  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   4.420 +  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   4.421 +
   4.422 +lemma enumerate_Suc':
   4.423 +    "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   4.424 +  by simp
   4.425 +
   4.426 +lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   4.427 +  apply (induct n arbitrary: S)
   4.428 +   apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   4.429 +  apply (fastsimp iff: finite_Diff_singleton)
   4.430 +  done
   4.431 +
   4.432 +declare enumerate_0 [simp del] enumerate_Suc [simp del]
   4.433 +
   4.434 +lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   4.435 +  apply (induct n arbitrary: S)
   4.436 +   apply (rule order_le_neq_trans)
   4.437 +    apply (simp add: enumerate_0 Least_le enumerate_in_set)
   4.438 +   apply (simp only: enumerate_Suc')
   4.439 +   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   4.440 +    apply (blast intro: sym)
   4.441 +   apply (simp add: enumerate_in_set del: Diff_iff)
   4.442 +  apply (simp add: enumerate_Suc')
   4.443 +  done
   4.444 +
   4.445 +lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   4.446 +  apply (erule less_Suc_induct)
   4.447 +  apply (auto intro: enumerate_step)
   4.448 +  done
   4.449 +
   4.450 +
   4.451 +subsection "Miscellaneous"
   4.452 +
   4.453 +text {*
   4.454 +  A few trivial lemmas about sets that contain at most one element.
   4.455 +  These simplify the reasoning about deterministic automata.
   4.456 +*}
   4.457 +
   4.458 +definition
   4.459 +  atmost_one :: "'a set \<Rightarrow> bool"
   4.460 +  "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   4.461 +
   4.462 +lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   4.463 +  by (simp add: atmost_one_def)
   4.464 +
   4.465 +lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   4.466 +  by (simp add: atmost_one_def)
   4.467 +
   4.468 +lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   4.469 +  by (simp add: atmost_one_def)
   4.470 +
   4.471 +end
     5.1 --- a/src/HOL/Library/Library.thy	Sun Oct 01 18:29:25 2006 +0200
     5.2 +++ b/src/HOL/Library/Library.thy	Sun Oct 01 18:29:26 2006 +0200
     5.3 @@ -1,3 +1,4 @@
     5.4 +(* $Id$ *)
     5.5  (*<*)
     5.6  theory Library
     5.7  imports
     5.8 @@ -23,6 +24,7 @@
     5.9    Commutative_Ring
    5.10    Coinductive_List
    5.11    AssocList
    5.12 +  Infinite_Set
    5.13  begin
    5.14  end
    5.15  (*>*)
     6.1 --- a/src/HOL/Nominal/Nominal.thy	Sun Oct 01 18:29:25 2006 +0200
     6.2 +++ b/src/HOL/Nominal/Nominal.thy	Sun Oct 01 18:29:26 2006 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (* $Id$ *)
     6.5  
     6.6  theory Nominal 
     6.7 -imports Main
     6.8 +imports Main Infinite_Set
     6.9  uses
    6.10    ("nominal_atoms.ML")
    6.11    ("nominal_package.ML")
     7.1 --- a/src/HOL/Nominal/ROOT.ML	Sun Oct 01 18:29:25 2006 +0200
     7.2 +++ b/src/HOL/Nominal/ROOT.ML	Sun Oct 01 18:29:26 2006 +0200
     7.3 @@ -5,4 +5,5 @@
     7.4  The nominal datatype package.
     7.5  *)
     7.6  
     7.7 +no_document use_thy "Infinite_Set";
     7.8  use_thy "Nominal";
     8.1 --- a/src/HOL/NumberTheory/Finite2.thy	Sun Oct 01 18:29:25 2006 +0200
     8.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Sun Oct 01 18:29:26 2006 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  header {*Finite Sets and Finite Sums*}
     8.5  
     8.6  theory Finite2
     8.7 -imports IntFact
     8.8 +imports IntFact Infinite_Set
     8.9  begin
    8.10  
    8.11  text{*
     9.1 --- a/src/HOL/NumberTheory/ROOT.ML	Sun Oct 01 18:29:25 2006 +0200
     9.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Sun Oct 01 18:29:26 2006 +0200
     9.3 @@ -1,5 +1,6 @@
     9.4  (* $Id$ *)
     9.5  
     9.6 +no_document use_thy "Infinite_Set";
     9.7  no_document use_thy "Permutation";
     9.8  no_document use_thy "Primes";
     9.9  
    10.1 --- a/src/HOL/Reconstruction.thy	Sun Oct 01 18:29:25 2006 +0200
    10.2 +++ b/src/HOL/Reconstruction.thy	Sun Oct 01 18:29:26 2006 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  header{* Reconstructing external resolution proofs *}
    10.5  
    10.6  theory Reconstruction
    10.7 -imports Hilbert_Choice Map Infinite_Set Extraction
    10.8 +imports Hilbert_Choice Map Extraction
    10.9  uses 	 "Tools/polyhash.ML"
   10.10  	 "Tools/ATP/AtpCommunication.ML"
   10.11  	 "Tools/ATP/watcher.ML"