src/HOL/Product_Type.thy
changeset 20588 c847c56edf0c
parent 20415 e3d2d7b01279
child 21046 fe1db2f991a7
     1.1 --- a/src/HOL/Product_Type.thy	Tue Sep 19 15:21:41 2006 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 19 15:21:42 2006 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  typedef unit = "{True}"
     1.6  proof
     1.7 -  show "True : ?unit" by blast
     1.8 +  show "True : ?unit" ..
     1.9  qed
    1.10  
    1.11  constdefs
    1.12 @@ -761,6 +761,29 @@
    1.13  
    1.14  subsection {* Code generator setup *}
    1.15  
    1.16 +instance unit :: eq ..
    1.17 +
    1.18 +lemma [code func]:
    1.19 +  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
    1.20 +
    1.21 +code_instance unit :: eq
    1.22 +  (Haskell -)
    1.23 +
    1.24 +instance * :: (eq, eq) eq ..
    1.25 +
    1.26 +lemma [code func]:
    1.27 +  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
    1.28 +  unfolding eq_def by auto
    1.29 +
    1.30 +code_instance * :: eq
    1.31 +  (Haskell -)
    1.32 +
    1.33 +code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.34 +  (Haskell infixl 4 "==")
    1.35 +
    1.36 +code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.37 +  (Haskell infixl 4 "==")
    1.38 +
    1.39  types_code
    1.40    "*"     ("(_ */ _)")
    1.41  attach (term_of) {*