adding code equations for EX1 on finite types
authorbulwahn
Mon, 22 Nov 2010 11:34:58 +0100
changeset 40652 7bdfc1d6b143
parent 40651 9752ba7348b5
child 40653 d921c97bdbd8
adding code equations for EX1 on finite types
src/HOL/Enum.thy
src/HOL/List.thy
--- a/src/HOL/Enum.thy	Mon Nov 22 11:34:57 2010 +0100
+++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:58 2010 +0100
@@ -69,6 +69,9 @@
 lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
   by (simp add: list_ex_iff enum_all)
 
+lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
+unfolding list_ex1_iff enum_all by auto
+
 
 subsection {* Default instances *}
 
--- a/src/HOL/List.thy	Mon Nov 22 11:34:57 2010 +0100
+++ b/src/HOL/List.thy	Mon Nov 22 11:34:58 2010 +0100
@@ -4877,6 +4877,10 @@
 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
 
+definition list_ex1
+where
+  list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
+
 text {*
   Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
   over @{const list_all} and @{const list_ex} in specifications.
@@ -4892,6 +4896,11 @@
   "list_ex P [] \<longleftrightarrow> False"
   by (simp_all add: list_ex_iff)
 
+lemma list_ex1_simps [simp, code]:
+  "list_ex1 P [] = False"
+  "list_ex1 P (x # xs) = (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)"
+unfolding list_ex1_iff list_all_iff by auto
+
 lemma Ball_set_list_all [code_unfold]:
   "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   by (simp add: list_all_iff)