# HG changeset patch
# User haftmann
# Date 1211551502 -7200
# Node ID bb0a56a66180a91b34f0374c2dd9e05f495f46ad
# Parent  27f60aaa5a7bb7512094f5dd322976200aa696f4
added code for quantifiers

diff -r 27f60aaa5a7b -r bb0a56a66180 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Fri May 23 16:04:59 2008 +0200
+++ b/src/HOL/Library/Enum.thy	Fri May 23 16:05:02 2008 +0200
@@ -51,9 +51,18 @@
 
 lemma order_fun [code func]:
   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
-  shows "f \<le> g \<longleftrightarrow> (\<forall>x \<in> set enum. f x \<le> g x)"
-    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x \<in> set enum. f x \<noteq> g x)"
-  by (simp_all add: enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
+  shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
+    and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
+  by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
+
+
+subsection {* Quantifiers *}
+
+lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
+  by (simp add: list_all_iff enum_all)
+
+lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
+  by (simp add: list_all_iff enum_all)
 
 
 subsection {* Default instances *}