equal
deleted
inserted
replaced
51 |
51 |
52 lemma order_fun [code]: |
52 lemma order_fun [code]: |
53 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" |
53 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" |
54 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum" |
54 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum" |
55 and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum" |
55 and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum" |
56 by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def less_fun_def order_less_le) |
56 by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le) |
57 |
57 |
58 |
58 |
59 subsection {* Quantifiers *} |
59 subsection {* Quantifiers *} |
60 |
60 |
61 lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum" |
61 lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum" |