executable equality
authorhaftmann
Fri, 22 Mar 2019 19:18:09 +0000
changeset 70129 77a92e8d5167
parent 70128 494934c30f38
child 70135 3544cca7920f
executable equality
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 \<longleftrightarrow> 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 \<Rightarrow> 'a dual \<Rightarrow> bool"
+  is HOL.equal .
+
+instance
+  by (standard; transfer) (simp add: equal)
+
+end
+
 
 subsection \<open>Pointwise ordering\<close>