src/HOL/Infinite_Set.thy
 changeset 19537 213ff8b0c60c parent 19457 b6eb4b4546fa child 19656 09be06943252
equal inserted replaced
19536:1a3a3cf8b4fa 19537:213ff8b0c60c
`    22   from an infinite set, the result is still infinite.`
`    22   from an infinite set, the result is still infinite.`
`    23 *}`
`    23 *}`
`    24 `
`    24 `
`    25 lemma infinite_nonempty:`
`    25 lemma infinite_nonempty:`
`    26   "\<not> (infinite {})"`
`    26   "\<not> (infinite {})"`
`    27 by simp`
`    27   by simp`
`    28 `
`    28 `
`    29 lemma infinite_remove:`
`    29 lemma infinite_remove:`
`    30   "infinite S \<Longrightarrow> infinite (S - {a})"`
`    30   "infinite S \<Longrightarrow> infinite (S - {a})"`
`    31 by simp`
`    31   by simp`
`    32 `
`    32 `
`    33 lemma Diff_infinite_finite:`
`    33 lemma Diff_infinite_finite:`
`    34   assumes T: "finite T" and S: "infinite S"`
`    34   assumes T: "finite T" and S: "infinite S"`
`    35   shows "infinite (S-T)"`
`    35   shows "infinite (S-T)"`
`    36 using T`
`    36   using T`
`    37 proof (induct)`
`    37 proof induct`
`    38   from S`
`    38   from S`
`    39   show "infinite (S - {})" by auto`
`    39   show "infinite (S - {})" by auto`
`    40 next`
`    40 next`
`    41   fix T x`
`    41   fix T x`
`    42   assume ih: "infinite (S-T)"`
`    42   assume ih: "infinite (S-T)"`
`    47     by (simp add: infinite_remove)`
`    47     by (simp add: infinite_remove)`
`    48 qed`
`    48 qed`
`    49 `
`    49 `
`    50 lemma Un_infinite:`
`    50 lemma Un_infinite:`
`    51   "infinite S \<Longrightarrow> infinite (S \<union> T)"`
`    51   "infinite S \<Longrightarrow> infinite (S \<union> T)"`
`    52 by simp`
`    52   by simp`
`    53 `
`    53 `
`    54 lemma infinite_super:`
`    54 lemma infinite_super:`
`    55   assumes T: "S \<subseteq> T" and S: "infinite S"`
`    55   assumes T: "S \<subseteq> T" and S: "infinite S"`
`    56   shows "infinite T"`
`    56   shows "infinite T"`
`    57 proof (rule ccontr)`
`    57 proof (rule ccontr)`
`    58   assume "\<not>(infinite T)"`
`    58   assume "\<not>(infinite T)"`
`    59   with T`
`    59   with T have "finite S" by (simp add: finite_subset)`
`    60   have "finite S" by (simp add: finite_subset)`
`    60   with S show False by simp`
`    61   with S`
`       `
`    62   show False by simp`
`       `
`    63 qed`
`    61 qed`
`    64 `
`    62 `
`    65 text {*`
`    63 text {*`
`    66   As a concrete example, we prove that the set of natural`
`    64   As a concrete example, we prove that the set of natural`
`    67   numbers is infinite.`
`    65   numbers is infinite.`
`   354 `
`   352 `
`   355 defs`
`   353 defs`
`   356   INF_def:  "Inf_many P \<equiv> infinite {x. P x}"`
`   354   INF_def:  "Inf_many P \<equiv> infinite {x. P x}"`
`   357   MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"`
`   355   MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"`
`   358 `
`   356 `
`   359 syntax (xsymbols)`
`   357 abbreviation (xsymbols)`
`   360   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)`
`   358   Inf_many1  (binder "\<exists>\<^sub>\<infinity>" 10)`
`   361   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)`
`   359   "Inf_many1 == Inf_many"`
`   362 `
`   360   Alm_all1  (binder "\<forall>\<^sub>\<infinity>" 10)`
`   363 syntax (HTML output)`
`   361   "Alm_all1 == Alm_all"`
`   364   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)`
`   362 `
`   365   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)`
`   363 abbreviation (HTML output)`
`       `
`   364   Inf_many2  (binder "\<exists>\<^sub>\<infinity>" 10)`
`       `
`   365   "Inf_many2 == Inf_many"`
`       `
`   366   Alm_all2  (binder "\<forall>\<^sub>\<infinity>" 10)`
`       `
`   367   "Alm_all2 == Alm_all"`
`   366 `
`   368 `
`   367 lemma INF_EX:`
`   369 lemma INF_EX:`
`   368   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"`
`   370   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"`
`   369 proof (unfold INF_def, rule ccontr)`
`   371 proof (unfold INF_def, rule ccontr)`
`   370   assume inf: "infinite {x. P x}"`
`   372   assume inf: "infinite {x. P x}"`
`   419 constdefs`
`   421 constdefs`
`   420   atmost_one :: "'a set \<Rightarrow> bool"`
`   422   atmost_one :: "'a set \<Rightarrow> bool"`
`   421   "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"`
`   423   "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"`
`   422 `
`   424 `
`   423 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"`
`   425 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"`
`   424 by (simp add: atmost_one_def)`
`   426   by (simp add: atmost_one_def)`
`   425 `
`   427 `
`   426 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"`
`   428 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"`
`   427 by (simp add: atmost_one_def)`
`   429   by (simp add: atmost_one_def)`
`   428 `
`   430 `
`   429 lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x"`
`   431 lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x"`
`   430 by (simp add: atmost_one_def)`
`   432   by (simp add: atmost_one_def)`
`   431 `
`   433 `
`   432 end`
`   434 end`