equal
deleted
inserted
replaced
5214 lemma in_set_member (* FIXME delete candidate *): |
5214 lemma in_set_member (* FIXME delete candidate *): |
5215 "x \<in> set xs \<longleftrightarrow> member xs x" |
5215 "x \<in> set xs \<longleftrightarrow> member xs x" |
5216 by (simp add: member_def) |
5216 by (simp add: member_def) |
5217 |
5217 |
5218 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5218 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5219 [code_abbrev]: list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P" |
5219 list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P" |
5220 |
5220 |
5221 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5221 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5222 [code_abbrev]: list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P" |
5222 list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P" |
5223 |
5223 |
5224 definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5224 definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5225 list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)" |
5225 list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)" |
5226 |
5226 |
5227 text {* |
5227 text {* |