src/HOL/Lattices.thy
changeset 25510 38c15efe603b
parent 25482 4ed49eccb1eb
child 26014 00c2c3525bef
     1.1 --- a/src/HOL/Lattices.thy	Fri Nov 30 16:23:52 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Fri Nov 30 20:13:03 2007 +0100
     1.3 @@ -479,16 +479,34 @@
     1.4  
     1.5  subsection {* Bool as lattice *}
     1.6  
     1.7 -instance bool :: distrib_lattice
     1.8 -  inf_bool_eq: "P \<sqinter> Q \<equiv> P \<and> Q"
     1.9 -  sup_bool_eq: "P \<squnion> Q \<equiv> P \<or> Q"
    1.10 +instantiation bool :: distrib_lattice
    1.11 +begin
    1.12 +
    1.13 +definition
    1.14 +  inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
    1.15 +
    1.16 +definition
    1.17 +  sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    1.18 +
    1.19 +instance
    1.20    by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
    1.21  
    1.22 -instance bool :: complete_lattice
    1.23 -  Inf_bool_def: "\<Sqinter>A \<equiv> \<forall>x\<in>A. x"
    1.24 -  Sup_bool_def: "\<Squnion>A \<equiv> \<exists>x\<in>A. x"
    1.25 +end
    1.26 +
    1.27 +instantiation bool :: complete_lattice
    1.28 +begin
    1.29 +
    1.30 +definition
    1.31 +  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    1.32 +
    1.33 +definition
    1.34 +  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.35 +
    1.36 +instance
    1.37    by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
    1.38  
    1.39 +end
    1.40 +
    1.41  lemma Inf_empty_bool [simp]:
    1.42    "\<Sqinter>{}"
    1.43    unfolding Inf_bool_def by auto
    1.44 @@ -506,12 +524,19 @@
    1.45  
    1.46  subsection {* Set as lattice *}
    1.47  
    1.48 -instance set :: (type) distrib_lattice
    1.49 -  inf_set_eq: "A \<sqinter> B \<equiv> A \<inter> B"
    1.50 -  sup_set_eq: "A \<squnion> B \<equiv> A \<union> B"
    1.51 +instantiation set :: (type) distrib_lattice
    1.52 +begin
    1.53 +
    1.54 +definition
    1.55 +  inf_set_eq [code func del]: "A \<sqinter> B = A \<inter> B"
    1.56 +
    1.57 +definition
    1.58 +  sup_set_eq [code func del]: "A \<squnion> B = A \<union> B"
    1.59 +
    1.60 +instance
    1.61    by intro_classes (auto simp add: inf_set_eq sup_set_eq)
    1.62  
    1.63 -lemmas [code func del] = inf_set_eq sup_set_eq
    1.64 +end
    1.65  
    1.66  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.67    apply (fold inf_set_eq sup_set_eq)
    1.68 @@ -523,12 +548,19 @@
    1.69    apply (erule mono_sup)
    1.70    done
    1.71  
    1.72 -instance set :: (type) complete_lattice
    1.73 -  Inf_set_def: "\<Sqinter>S \<equiv> \<Inter>S"
    1.74 -  Sup_set_def: "\<Squnion>S \<equiv> \<Union>S"
    1.75 +instantiation set :: (type) complete_lattice
    1.76 +begin
    1.77 +
    1.78 +definition
    1.79 +  Inf_set_def [code func del]: "\<Sqinter>S \<equiv> \<Inter>S"
    1.80 +
    1.81 +definition
    1.82 +  Sup_set_def [code func del]: "\<Squnion>S \<equiv> \<Union>S"
    1.83 +
    1.84 +instance
    1.85    by intro_classes (auto simp add: Inf_set_def Sup_set_def)
    1.86  
    1.87 -lemmas [code func del] = Inf_set_def Sup_set_def
    1.88 +end
    1.89  
    1.90  lemma top_set_eq: "top = UNIV"
    1.91    by (iprover intro!: subset_antisym subset_UNIV top_greatest)
    1.92 @@ -539,9 +571,16 @@
    1.93  
    1.94  subsection {* Fun as lattice *}
    1.95  
    1.96 -instance "fun" :: (type, lattice) lattice
    1.97 -  inf_fun_eq: "f \<sqinter> g \<equiv> (\<lambda>x. f x \<sqinter> g x)"
    1.98 -  sup_fun_eq: "f \<squnion> g \<equiv> (\<lambda>x. f x \<squnion> g x)"
    1.99 +instantiation "fun" :: (type, lattice) lattice
   1.100 +begin
   1.101 +
   1.102 +definition
   1.103 +  inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   1.104 +
   1.105 +definition
   1.106 +  sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   1.107 +
   1.108 +instance
   1.109  apply intro_classes
   1.110  unfolding inf_fun_eq sup_fun_eq
   1.111  apply (auto intro: le_funI)
   1.112 @@ -551,19 +590,26 @@
   1.113  apply (auto dest: le_funD)
   1.114  done
   1.115  
   1.116 -lemmas [code func del] = inf_fun_eq sup_fun_eq
   1.117 +end
   1.118  
   1.119  instance "fun" :: (type, distrib_lattice) distrib_lattice
   1.120    by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   1.121  
   1.122 -instance "fun" :: (type, complete_lattice) complete_lattice
   1.123 -  Inf_fun_def: "\<Sqinter>A \<equiv> (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.124 -  Sup_fun_def: "\<Squnion>A \<equiv> (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.125 +instantiation "fun" :: (type, complete_lattice) complete_lattice
   1.126 +begin
   1.127 +
   1.128 +definition
   1.129 +  Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.130 +
   1.131 +definition
   1.132 +  Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.133 +
   1.134 +instance
   1.135    by intro_classes
   1.136      (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   1.137        intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   1.138  
   1.139 -lemmas [code func del] = Inf_fun_def Sup_fun_def
   1.140 +end
   1.141  
   1.142  lemma Inf_empty_fun:
   1.143    "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"