src/HOL/Product_Type.thy
changeset 28346 b8390cd56b8f
parent 28262 aa7ca36d67fd
child 28537 1e84256d1a8a
     1.1 --- a/src/HOL/Product_Type.thy	Wed Sep 24 19:39:25 2008 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Sep 25 09:28:03 2008 +0200
     1.3 @@ -22,13 +22,15 @@
     1.4  declare case_split [cases type: bool]
     1.5    -- "prefer plain propositional version"
     1.6  
     1.7 -lemma [code func]:
     1.8 -  shows "False = P \<longleftrightarrow> \<not> P"
     1.9 -    and "True = P \<longleftrightarrow> P" 
    1.10 -    and "P = False \<longleftrightarrow> \<not> P" 
    1.11 -    and "P = True \<longleftrightarrow> P" by simp_all
    1.12 +lemma
    1.13 +  shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
    1.14 +    and [code func]: "eq_class.eq True P \<longleftrightarrow> P" 
    1.15 +    and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
    1.16 +    and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
    1.17 +    and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
    1.18 +  by (simp_all add: eq)
    1.19  
    1.20 -code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.21 +code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.22    (Haskell infixl 4 "==")
    1.23  
    1.24  code_instance bool :: eq
    1.25 @@ -88,7 +90,7 @@
    1.26  instance unit :: eq ..
    1.27  
    1.28  lemma [code func]:
    1.29 -  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
    1.30 +  "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
    1.31  
    1.32  code_type unit
    1.33    (SML "unit")
    1.34 @@ -98,7 +100,7 @@
    1.35  code_instance unit :: eq
    1.36    (Haskell -)
    1.37  
    1.38 -code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.39 +code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.40    (Haskell infixl 4 "==")
    1.41  
    1.42  code_const Unity
    1.43 @@ -916,7 +918,7 @@
    1.44  instance * :: (eq, eq) eq ..
    1.45  
    1.46  lemma [code func]:
    1.47 -  "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
    1.48 +  "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
    1.49  
    1.50  lemma split_case_cert:
    1.51    assumes "CASE \<equiv> split f"
    1.52 @@ -935,7 +937,7 @@
    1.53  code_instance * :: eq
    1.54    (Haskell -)
    1.55  
    1.56 -code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.57 +code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.58    (Haskell infixl 4 "==")
    1.59  
    1.60  code_const Pair