src/HOL/Library/Infinite_Set.thy
 author Christian Sternagel Wed Aug 29 12:23:14 2012 +0900 (2012-08-29) changeset 49083 01081bca31b6 parent 46783 3e89a5cab8d7 child 50134 13211e07d931 permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
1 (*  Title:      HOL/Library/Infinite_Set.thy
2     Author:     Stephan Merz
3 *)
5 header {* Infinite Sets and Related Concepts *}
7 theory Infinite_Set
8 imports Main
9 begin
11 subsection "Infinite Sets"
13 text {*
14   Some elementary facts about infinite sets, mostly by Stefan Merz.
15   Beware! Because "infinite" merely abbreviates a negation, these
16   lemmas may not work well with @{text "blast"}.
17 *}
19 abbreviation
20   infinite :: "'a set \<Rightarrow> bool" where
21   "infinite S == \<not> finite S"
23 text {*
24   Infinite sets are non-empty, and if we remove some elements from an
25   infinite set, the result is still infinite.
26 *}
28 lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
29   by auto
31 lemma infinite_remove:
32   "infinite S \<Longrightarrow> infinite (S - {a})"
33   by simp
35 lemma Diff_infinite_finite:
36   assumes T: "finite T" and S: "infinite S"
37   shows "infinite (S - T)"
38   using T
39 proof induct
40   from S
41   show "infinite (S - {})" by auto
42 next
43   fix T x
44   assume ih: "infinite (S - T)"
45   have "S - (insert x T) = (S - T) - {x}"
46     by (rule Diff_insert)
47   with ih
48   show "infinite (S - (insert x T))"
49     by (simp add: infinite_remove)
50 qed
52 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
53   by simp
55 lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
56   by simp
58 lemma infinite_super:
59   assumes T: "S \<subseteq> T" and S: "infinite S"
60   shows "infinite T"
61 proof
62   assume "finite T"
63   with T have "finite S" by (simp add: finite_subset)
64   with S show False by simp
65 qed
67 text {*
68   As a concrete example, we prove that the set of natural numbers is
69   infinite.
70 *}
72 lemma finite_nat_bounded:
73   assumes S: "finite (S::nat set)"
74   shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
75 using S
76 proof induct
77   have "?bounded {} 0" by simp
78   then show "\<exists>k. ?bounded {} k" ..
79 next
80   fix S x
81   assume "\<exists>k. ?bounded S k"
82   then obtain k where k: "?bounded S k" ..
83   show "\<exists>k. ?bounded (insert x S) k"
84   proof (cases "x < k")
85     case True
86     with k show ?thesis by auto
87   next
88     case False
89     with k have "?bounded S (Suc x)" by auto
90     then show ?thesis by auto
91   qed
92 qed
94 lemma finite_nat_iff_bounded:
95   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
96 proof
97   assume ?lhs
98   then show ?rhs by (rule finite_nat_bounded)
99 next
100   assume ?rhs
101   then obtain k where "S \<subseteq> {..<k}" ..
102   then show "finite S"
103     by (rule finite_subset) simp
104 qed
106 lemma finite_nat_iff_bounded_le:
107   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
108 proof
109   assume ?lhs
110   then obtain k where "S \<subseteq> {..<k}"
111     by (blast dest: finite_nat_bounded)
112   then have "S \<subseteq> {..k}" by auto
113   then show ?rhs ..
114 next
115   assume ?rhs
116   then obtain k where "S \<subseteq> {..k}" ..
117   then show "finite S"
118     by (rule finite_subset) simp
119 qed
121 lemma infinite_nat_iff_unbounded:
122   "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
123   (is "?lhs = ?rhs")
124 proof
125   assume ?lhs
126   show ?rhs
127   proof (rule ccontr)
128     assume "\<not> ?rhs"
129     then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
130     then have "S \<subseteq> {..m}"
131       by (auto simp add: sym [OF linorder_not_less])
132     with `?lhs` show False
133       by (simp add: finite_nat_iff_bounded_le)
134   qed
135 next
136   assume ?rhs
137   show ?lhs
138   proof
139     assume "finite S"
140     then obtain m where "S \<subseteq> {..m}"
141       by (auto simp add: finite_nat_iff_bounded_le)
142     then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
143     with `?rhs` show False by blast
144   qed
145 qed
147 lemma infinite_nat_iff_unbounded_le:
148   "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
149   (is "?lhs = ?rhs")
150 proof
151   assume ?lhs
152   show ?rhs
153   proof
154     fix m
155     from `?lhs` obtain n where "m<n \<and> n\<in>S"
156       by (auto simp add: infinite_nat_iff_unbounded)
157     then have "m\<le>n \<and> n\<in>S" by simp
158     then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
159   qed
160 next
161   assume ?rhs
162   show ?lhs
163   proof (auto simp add: infinite_nat_iff_unbounded)
164     fix m
165     from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
166       by blast
167     then have "m<n \<and> n\<in>S" by simp
168     then show "\<exists>n. m < n \<and> n \<in> S" ..
169   qed
170 qed
172 text {*
173   For a set of natural numbers to be infinite, it is enough to know
174   that for any number larger than some @{text k}, there is some larger
175   number that is an element of the set.
176 *}
178 lemma unbounded_k_infinite:
179   assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
180   shows "infinite (S::nat set)"
181 proof -
182   {
183     fix m have "\<exists>n. m<n \<and> n\<in>S"
184     proof (cases "k<m")
185       case True
186       with k show ?thesis by blast
187     next
188       case False
189       from k obtain n where "Suc k < n \<and> n\<in>S" by auto
190       with False have "m<n \<and> n\<in>S" by auto
191       then show ?thesis ..
192     qed
193   }
194   then show ?thesis
195     by (auto simp add: infinite_nat_iff_unbounded)
196 qed
198 (* duplicates Finite_Set.infinite_UNIV_nat *)
199 lemma nat_infinite: "infinite (UNIV :: nat set)"
200   by (auto simp add: infinite_nat_iff_unbounded)
202 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
203   by simp
205 text {*
206   Every infinite set contains a countable subset. More precisely we
207   show that a set @{text S} is infinite if and only if there exists an
208   injective function from the naturals into @{text S}.
209 *}
211 lemma range_inj_infinite:
212   "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
213 proof
214   assume "finite (range f)" and "inj f"
215   then have "finite (UNIV::nat set)"
216     by (rule finite_imageD)
217   then show False by simp
218 qed
220 lemma int_infinite [simp]:
221   shows "infinite (UNIV::int set)"
222 proof -
223   from inj_int have "infinite (range int)" by (rule range_inj_infinite)
224   moreover
225   have "range int \<subseteq> (UNIV::int set)" by simp
226   ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
227 qed
229 text {*
230   The ``only if'' direction is harder because it requires the
231   construction of a sequence of pairwise different elements of an
232   infinite set @{text S}. The idea is to construct a sequence of
233   non-empty and infinite subsets of @{text S} obtained by successively
234   removing elements of @{text S}.
235 *}
237 lemma linorder_injI:
238   assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
239   shows "inj f"
240 proof (rule inj_onI)
241   fix x y
242   assume f_eq: "f x = f y"
243   show "x = y"
244   proof (rule linorder_cases)
245     assume "x < y"
246     with hyp have "f x \<noteq> f y" by blast
247     with f_eq show ?thesis by simp
248   next
249     assume "x = y"
250     then show ?thesis .
251   next
252     assume "y < x"
253     with hyp have "f y \<noteq> f x" by blast
254     with f_eq show ?thesis by simp
255   qed
256 qed
258 lemma infinite_countable_subset:
259   assumes inf: "infinite (S::'a set)"
260   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
261 proof -
262   def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
263   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
264   have Sseq_inf: "\<And>n. infinite (Sseq n)"
265   proof -
266     fix n
267     show "infinite (Sseq n)"
268     proof (induct n)
269       from inf show "infinite (Sseq 0)"
270         by (simp add: Sseq_def)
271     next
272       fix n
273       assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
274         by (simp add: Sseq_def infinite_remove)
275     qed
276   qed
277   have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
278   proof -
279     fix n
280     show "Sseq n \<subseteq> S"
281       by (induct n) (auto simp add: Sseq_def)
282   qed
283   have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
284   proof -
285     fix n
286     show "pick n \<in> Sseq n"
287     proof (unfold pick_def, rule someI_ex)
288       from Sseq_inf have "infinite (Sseq n)" .
289       then have "Sseq n \<noteq> {}" by auto
290       then show "\<exists>x. x \<in> Sseq n" by auto
291     qed
292   qed
293   with Sseq_S have rng: "range pick \<subseteq> S"
294     by auto
295   have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
296   proof -
297     fix n m
298     show "pick n \<notin> Sseq (n + Suc m)"
299       by (induct m) (auto simp add: Sseq_def pick_def)
300   qed
301   have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
302   proof -
303     fix n m
304     from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
305     moreover from pick_Sseq_gt
306     have "pick n \<notin> Sseq (n + Suc m)" .
307     ultimately show "pick n \<noteq> pick (n + Suc m)"
308       by auto
309   qed
310   have inj: "inj pick"
311   proof (rule linorder_injI)
312     fix i j :: nat
313     assume "i < j"
314     show "pick i \<noteq> pick j"
315     proof
316       assume eq: "pick i = pick j"
317       from `i < j` obtain k where "j = i + Suc k"
319       with pick_pick have "pick i \<noteq> pick j" by simp
320       with eq show False by simp
321     qed
322   qed
323   from rng inj show ?thesis by auto
324 qed
326 lemma infinite_iff_countable_subset:
327     "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
328   by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
330 text {*
331   For any function with infinite domain and finite range there is some
332   element that is the image of infinitely many domain elements.  In
333   particular, any infinite sequence of elements from a finite set
334   contains some element that occurs infinitely often.
335 *}
337 lemma inf_img_fin_dom:
338   assumes img: "finite (f`A)" and dom: "infinite A"
339   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
340 proof (rule ccontr)
341   assume "\<not> ?thesis"
342   with img have "finite (UN y:f`A. f -` {y})" by blast
343   moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
344   moreover note dom
345   ultimately show False by (simp add: infinite_super)
346 qed
348 lemma inf_img_fin_domE:
349   assumes "finite (f`A)" and "infinite A"
350   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
351   using assms by (blast dest: inf_img_fin_dom)
354 subsection "Infinitely Many and Almost All"
356 text {*
357   We often need to reason about the existence of infinitely many
358   (resp., all but finitely many) objects satisfying some predicate, so
359   we introduce corresponding binders and their proof rules.
360 *}
362 definition
363   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
364   "Inf_many P = infinite {x. P x}"
366 definition
367   Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
368   "Alm_all P = (\<not> (INFM x. \<not> P x))"
370 notation (xsymbols)
371   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
372   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
374 notation (HTML output)
375   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
376   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
378 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
379   unfolding Inf_many_def ..
381 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
382   unfolding Alm_all_def Inf_many_def by simp
384 (* legacy name *)
385 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
387 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
388   unfolding Alm_all_def not_not ..
390 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
391   unfolding Alm_all_def not_not ..
393 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
394   unfolding Inf_many_def by simp
396 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
397   unfolding Alm_all_def by simp
399 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
400   by (erule contrapos_pp, simp)
402 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
403   by simp
405 lemma INFM_E: assumes "INFM x. P x" obtains x where "P x"
406   using INFM_EX [OF assms] by (rule exE)
408 lemma MOST_I: assumes "\<And>x. P x" shows "MOST x. P x"
409   using assms by simp
411 lemma INFM_mono:
412   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
413   shows "\<exists>\<^sub>\<infinity>x. Q x"
414 proof -
415   from inf have "infinite {x. P x}" unfolding Inf_many_def .
416   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
417   ultimately show ?thesis
418     by (simp add: Inf_many_def infinite_super)
419 qed
421 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
422   unfolding Alm_all_def by (blast intro: INFM_mono)
424 lemma INFM_disj_distrib:
425   "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
426   unfolding Inf_many_def by (simp add: Collect_disj_eq)
428 lemma INFM_imp_distrib:
429   "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
430   by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
432 lemma MOST_conj_distrib:
433   "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
434   unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
436 lemma MOST_conjI:
437   "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
438   by (simp add: MOST_conj_distrib)
440 lemma INFM_conjI:
441   "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
442   unfolding MOST_iff_cofinite INFM_iff_infinite
443   apply (drule (1) Diff_infinite_finite)
444   apply (simp add: Collect_conj_eq Collect_neg_eq)
445   done
447 lemma MOST_rev_mp:
448   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
449   shows "\<forall>\<^sub>\<infinity>x. Q x"
450 proof -
451   have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
452     using assms by (rule MOST_conjI)
453   thus ?thesis by (rule MOST_mono) simp
454 qed
456 lemma MOST_imp_iff:
457   assumes "MOST x. P x"
458   shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
459 proof
460   assume "MOST x. P x \<longrightarrow> Q x"
461   with assms show "MOST x. Q x" by (rule MOST_rev_mp)
462 next
463   assume "MOST x. Q x"
464   then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
465 qed
467 lemma INFM_MOST_simps [simp]:
468   "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
469   "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
470   "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
471   "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
472   "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
473   "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
474   unfolding Alm_all_def Inf_many_def
475   by (simp_all add: Collect_conj_eq)
477 text {* Properties of quantifiers with injective functions. *}
479 lemma INFM_inj:
480   "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
481   unfolding INFM_iff_infinite
482   by (clarify, drule (1) finite_vimageI, simp)
484 lemma MOST_inj:
485   "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
486   unfolding MOST_iff_cofinite
487   by (drule (1) finite_vimageI, simp)
489 text {* Properties of quantifiers with singletons. *}
491 lemma not_INFM_eq [simp]:
492   "\<not> (INFM x. x = a)"
493   "\<not> (INFM x. a = x)"
494   unfolding INFM_iff_infinite by simp_all
496 lemma MOST_neq [simp]:
497   "MOST x. x \<noteq> a"
498   "MOST x. a \<noteq> x"
499   unfolding MOST_iff_cofinite by simp_all
501 lemma INFM_neq [simp]:
502   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
503   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
504   unfolding INFM_iff_infinite by simp_all
506 lemma MOST_eq [simp]:
507   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
508   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
509   unfolding MOST_iff_cofinite by simp_all
511 lemma MOST_eq_imp:
512   "MOST x. x = a \<longrightarrow> P x"
513   "MOST x. a = x \<longrightarrow> P x"
514   unfolding MOST_iff_cofinite by simp_all
516 text {* Properties of quantifiers over the naturals. *}
518 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
519   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
521 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
522   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
524 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
525   by (simp add: Alm_all_def INFM_nat)
527 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
528   by (simp add: Alm_all_def INFM_nat_le)
531 subsection "Enumeration of an Infinite Set"
533 text {*
534   The set's element type must be wellordered (e.g. the natural numbers).
535 *}
537 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
538     enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
539   | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
541 lemma enumerate_Suc':
542     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
543   by simp
545 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
546 apply (induct n arbitrary: S)
547  apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
548 apply simp
549 apply (metis DiffE infinite_remove)
550 done
552 declare enumerate_0 [simp del] enumerate_Suc [simp del]
554 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
555   apply (induct n arbitrary: S)
556    apply (rule order_le_neq_trans)
557     apply (simp add: enumerate_0 Least_le enumerate_in_set)
558    apply (simp only: enumerate_Suc')
559    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
560     apply (blast intro: sym)
561    apply (simp add: enumerate_in_set del: Diff_iff)
562   apply (simp add: enumerate_Suc')
563   done
565 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
566   apply (erule less_Suc_induct)
567   apply (auto intro: enumerate_step)
568   done
571 subsection "Miscellaneous"
573 text {*
574   A few trivial lemmas about sets that contain at most one element.
575   These simplify the reasoning about deterministic automata.
576 *}
578 definition
579   atmost_one :: "'a set \<Rightarrow> bool" where
580   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
582 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
583   by (simp add: atmost_one_def)
585 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
586   by (simp add: atmost_one_def)
588 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
589   by (simp add: atmost_one_def)
591 end