src/HOL/Library/Infinite_Set.thy
changeset 64697 47c1e6b0886f
parent 63993 9c0ff0c12116
child 64967 1ab49aa7f3c0
equal deleted inserted replaced
64696:e991a4fab0dc 64697:47c1e6b0886f
   150 
   150 
   151 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   151 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   152   by (simp add: eventually_frequently)
   152   by (simp add: eventually_frequently)
   153 
   153 
   154 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   154 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   155   by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
   155   by (simp add: cofinite_eq_sequentially)
   156 
   156 
   157 lemma
   157 lemma
   158   shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   158   shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   159     and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   159     and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   160   by (simp_all add: MOST_Suc_iff)
   160   by (simp_all add: MOST_Suc_iff)
   315   shows "A = {}"
   315   shows "A = {}"
   316 using \<open>finite A\<close> A
   316 using \<open>finite A\<close> A
   317 proof (induction A)
   317 proof (induction A)
   318   case (insert a A)
   318   case (insert a A)
   319   with R show ?case
   319   with R show ?case
   320     by (metis empty_iff insert_iff) 
   320     by (metis empty_iff insert_iff)
   321 qed simp
   321 qed simp
   322 
   322 
   323 corollary Union_maximal_sets:
   323 corollary Union_maximal_sets:
   324   assumes "finite \<F>"
   324   assumes "finite \<F>"
   325     shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>"
   325     shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>"