# HG changeset patch # User haftmann # Date 1553282289 0 # Node ID 77a92e8d5167af85a69f5909b8d4285b1010b847 # Parent 494934c30f382234aaff30bb0505f9e5db4e0fb3 executable equality diff -r 494934c30f38 -r 77a92e8d5167 src/HOL/Library/Dual_Ordered_Lattice.thy --- a/src/HOL/Library/Dual_Ordered_Lattice.thy Fri Mar 22 19:18:08 2019 +0000 +++ b/src/HOL/Library/Dual_Ordered_Lattice.thy Fri Mar 22 19:18:09 2019 +0000 @@ -24,6 +24,8 @@ setup_lifting type_definition_dual +code_datatype dual + lemma dual_eqI: "x = y" if "undual x = undual y" using that by transfer assumption @@ -36,7 +38,7 @@ "dual x = dual y \ x = y" by transfer simp -lemma undual_dual [simp]: +lemma undual_dual [simp, code]: "undual (dual x) = x" by transfer rule @@ -84,6 +86,17 @@ by (simp add: surj_dual) qed +instantiation dual :: (equal) equal +begin + +lift_definition equal_dual :: "'a dual \ 'a dual \ bool" + is HOL.equal . + +instance + by (standard; transfer) (simp add: equal) + +end + subsection \Pointwise ordering\