equal
deleted
inserted
replaced
44 instance proof |
44 instance proof |
45 qed (simp_all add: equal_fun_def enum_all fun_eq_iff) |
45 qed (simp_all add: equal_fun_def enum_all fun_eq_iff) |
46 |
46 |
47 end |
47 end |
48 |
48 |
|
49 lemma [code]: |
|
50 "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum" |
|
51 by (auto simp add: list_all_iff enum_all equal fun_eq_iff) |
|
52 |
49 lemma [code nbe]: |
53 lemma [code nbe]: |
50 "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True" |
54 "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True" |
51 by (fact equal_refl) |
55 by (fact equal_refl) |
52 |
|
53 lemma [code]: |
|
54 "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum" |
|
55 by (auto simp add: list_all_iff enum_all equal fun_eq_iff) |
|
56 |
56 |
57 lemma order_fun [code]: |
57 lemma order_fun [code]: |
58 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" |
58 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" |
59 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum" |
59 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum" |
60 and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum" |
60 and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum" |