adding code equations for EX1 on finite types
authorbulwahn
Mon Nov 22 11:34:58 2010 +0100 (2010-11-22)
changeset 406527bdfc1d6b143
parent 40651 9752ba7348b5
child 40653 d921c97bdbd8
adding code equations for EX1 on finite types
src/HOL/Enum.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Nov 22 11:34:57 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:58 2010 +0100
     1.3 @@ -69,6 +69,9 @@
     1.4  lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
     1.5    by (simp add: list_ex_iff enum_all)
     1.6  
     1.7 +lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
     1.8 +unfolding list_ex1_iff enum_all by auto
     1.9 +
    1.10  
    1.11  subsection {* Default instances *}
    1.12  
     2.1 --- a/src/HOL/List.thy	Mon Nov 22 11:34:57 2010 +0100
     2.2 +++ b/src/HOL/List.thy	Mon Nov 22 11:34:58 2010 +0100
     2.3 @@ -4877,6 +4877,10 @@
     2.4  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
     2.5    list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
     2.6  
     2.7 +definition list_ex1
     2.8 +where
     2.9 +  list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
    2.10 +
    2.11  text {*
    2.12    Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
    2.13    over @{const list_all} and @{const list_ex} in specifications.
    2.14 @@ -4892,6 +4896,11 @@
    2.15    "list_ex P [] \<longleftrightarrow> False"
    2.16    by (simp_all add: list_ex_iff)
    2.17  
    2.18 +lemma list_ex1_simps [simp, code]:
    2.19 +  "list_ex1 P [] = False"
    2.20 +  "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)"
    2.21 +unfolding list_ex1_iff list_all_iff by auto
    2.22 +
    2.23  lemma Ball_set_list_all [code_unfold]:
    2.24    "Ball (set xs) P \<longleftrightarrow> list_all P xs"
    2.25    by (simp add: list_all_iff)