# HG changeset patch # User bulwahn # Date 1290422098 -3600 # Node ID 7bdfc1d6b1433d0e6011fd96f717e8ef1b75501b # Parent 9752ba7348b5dd7c437328c3aad8e32bb01c45a6 adding code equations for EX1 on finite types diff -r 9752ba7348b5 -r 7bdfc1d6b143 src/HOL/Enum.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]: "(\x. P x) \ list_ex P enum" by (simp add: list_ex_iff enum_all) +lemma exists1_code[code]: "(\!x. P x) \ list_ex1 P enum" +unfolding list_ex1_iff enum_all by auto + subsection {* Default instances *} diff -r 9752ba7348b5 -r 7bdfc1d6b143 src/HOL/List.thy --- 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 \ bool) \ 'a list \ bool" where list_ex_iff [code_post]: "list_ex P xs \ (\x \ set xs. P x)" +definition list_ex1 +where + list_ex1_iff: "list_ex1 P xs \ (\! x. x \ set xs \ P x)" + text {* Usually you should prefer @{text "\x\set xs"} and @{text "\x\set xs"} over @{const list_all} and @{const list_ex} in specifications. @@ -4892,6 +4896,11 @@ "list_ex P [] \ 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 (\y. \ P y \ 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 \ list_all P xs" by (simp add: list_all_iff)