src/HOL/Library/Infinite_Set.thy

   Beware! Because "infinite" merely abbreviates a negation, these
   lemmas may not work well with @{text "blast"}.
 *}
 
 abbreviation
-  infinite :: "'a set \<Rightarrow> bool"
+  infinite :: "'a set \<Rightarrow> bool" where
   "infinite S == \<not> finite S"
 
 text {*
   Infinite sets are non-empty, and if we remove some elements from an
   infinite set, the result is still infinite.

   (resp., all but finitely many) objects satisfying some predicate, so
   we introduce corresponding binders and their proof rules.
 *}
 
 definition
-  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "INF " 10)
+  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INF " 10) where
   "Inf_many P = infinite {x. P x}"
-  Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
+
+definition
+  Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
   "Alm_all P = (\<not> (INF x. \<not> P x))"
 
 notation (xsymbols)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
 
 notation (HTML output)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
 
 lemma INF_EX:
   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   unfolding Inf_many_def

   A few trivial lemmas about sets that contain at most one element.
   These simplify the reasoning about deterministic automata.
 *}
 
 definition
-  atmost_one :: "'a set \<Rightarrow> bool"
+  atmost_one :: "'a set \<Rightarrow> bool" where
   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
 
 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   by (simp add: atmost_one_def)