executable equality
authorhaftmann
Fri Mar 22 19:18:09 2019 +0000 (3 weeks ago)
changeset 6994777a92e8d5167
parent 69946 494934c30f38
child 69953 3544cca7920f
executable equality
src/HOL/Library/Dual_Ordered_Lattice.thy
     1.1 --- a/src/HOL/Library/Dual_Ordered_Lattice.thy	Fri Mar 22 19:18:08 2019 +0000
     1.2 +++ b/src/HOL/Library/Dual_Ordered_Lattice.thy	Fri Mar 22 19:18:09 2019 +0000
     1.3 @@ -24,6 +24,8 @@
     1.4  
     1.5  setup_lifting type_definition_dual
     1.6  
     1.7 +code_datatype dual
     1.8 +
     1.9  lemma dual_eqI:
    1.10    "x = y" if "undual x = undual y"
    1.11    using that by transfer assumption
    1.12 @@ -36,7 +38,7 @@
    1.13    "dual x = dual y \<longleftrightarrow> x = y"
    1.14    by transfer simp
    1.15  
    1.16 -lemma undual_dual [simp]:
    1.17 +lemma undual_dual [simp, code]:
    1.18    "undual (dual x) = x"
    1.19    by transfer rule
    1.20  
    1.21 @@ -84,6 +86,17 @@
    1.22      by (simp add: surj_dual)
    1.23  qed
    1.24  
    1.25 +instantiation dual :: (equal) equal
    1.26 +begin
    1.27 +
    1.28 +lift_definition equal_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
    1.29 +  is HOL.equal .
    1.30 +
    1.31 +instance
    1.32 +  by (standard; transfer) (simp add: equal)
    1.33 +
    1.34 +end
    1.35 +
    1.36  
    1.37  subsection \<open>Pointwise ordering\<close>
    1.38