src/HOL/Infinite_Set.thy
changeset 19537 213ff8b0c60c
parent 19457 b6eb4b4546fa
child 19656 09be06943252
equal deleted 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