- Now imports Fun rather than Orderings
authorberghofe
Wed May 07 10:56:36 2008 +0200 (2008-05-07)
changeset 26794354c3844dfde
parent 26793 e36a92ff543e
child 26795 a27607030a1c
- Now imports Fun rather than Orderings
- Moved "Set as lattice" section behind "Fun as lattice" section, since
sets are just functions.
- The instantiations
instantiation set :: (type) distrib_lattice
instantiation set :: (type) complete_lattice
are no longer needed, and the former definitions inf_set_eq, sup_set_eq,
Inf_set_def, and Sup_set_def can now be derived from abstract properties
of sup, inf, etc.
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Wed May 07 10:56:35 2008 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Wed May 07 10:56:36 2008 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Abstract lattices *}
     1.5  
     1.6  theory Lattices
     1.7 -imports Orderings
     1.8 +imports Fun
     1.9  begin
    1.10  
    1.11  subsection{* Lattices *}
    1.12 @@ -506,53 +506,6 @@
    1.13    by (iprover intro!: order_antisym le_boolI bot_least)
    1.14  
    1.15  
    1.16 -subsection {* Set as lattice *}
    1.17 -
    1.18 -instantiation set :: (type) distrib_lattice
    1.19 -begin
    1.20 -
    1.21 -definition
    1.22 -  inf_set_eq [code func del]: "A \<sqinter> B = A \<inter> B"
    1.23 -
    1.24 -definition
    1.25 -  sup_set_eq [code func del]: "A \<squnion> B = A \<union> B"
    1.26 -
    1.27 -instance
    1.28 -  by intro_classes (auto simp add: inf_set_eq sup_set_eq)
    1.29 -
    1.30 -end
    1.31 -
    1.32 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.33 -  apply (fold inf_set_eq sup_set_eq)
    1.34 -  apply (erule mono_inf)
    1.35 -  done
    1.36 -
    1.37 -lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
    1.38 -  apply (fold inf_set_eq sup_set_eq)
    1.39 -  apply (erule mono_sup)
    1.40 -  done
    1.41 -
    1.42 -instantiation set :: (type) complete_lattice
    1.43 -begin
    1.44 -
    1.45 -definition
    1.46 -  Inf_set_def [code func del]: "\<Sqinter>S \<equiv> \<Inter>S"
    1.47 -
    1.48 -definition
    1.49 -  Sup_set_def [code func del]: "\<Squnion>S \<equiv> \<Union>S"
    1.50 -
    1.51 -instance
    1.52 -  by intro_classes (auto simp add: Inf_set_def Sup_set_def)
    1.53 -
    1.54 -end
    1.55 -
    1.56 -lemma top_set_eq: "top = UNIV"
    1.57 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
    1.58 -
    1.59 -lemma bot_set_eq: "bot = {}"
    1.60 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
    1.61 -
    1.62 -
    1.63  subsection {* Fun as lattice *}
    1.64  
    1.65  instantiation "fun" :: (type, lattice) lattice
    1.66 @@ -610,6 +563,61 @@
    1.67    by (iprover intro!: order_antisym le_funI bot_least)
    1.68  
    1.69  
    1.70 +subsection {* Set as lattice *}
    1.71 +
    1.72 +lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
    1.73 +  apply (rule subset_antisym)
    1.74 +  apply (rule Int_greatest)
    1.75 +  apply (rule inf_le1)
    1.76 +  apply (rule inf_le2)
    1.77 +  apply (rule inf_greatest)
    1.78 +  apply (rule Int_lower1)
    1.79 +  apply (rule Int_lower2)
    1.80 +  done
    1.81 +
    1.82 +lemma sup_set_eq: "A \<squnion> B = A \<union> B"
    1.83 +  apply (rule subset_antisym)
    1.84 +  apply (rule sup_least)
    1.85 +  apply (rule Un_upper1)
    1.86 +  apply (rule Un_upper2)
    1.87 +  apply (rule Un_least)
    1.88 +  apply (rule sup_ge1)
    1.89 +  apply (rule sup_ge2)
    1.90 +  done
    1.91 +
    1.92 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.93 +  apply (fold inf_set_eq sup_set_eq)
    1.94 +  apply (erule mono_inf)
    1.95 +  done
    1.96 +
    1.97 +lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
    1.98 +  apply (fold inf_set_eq sup_set_eq)
    1.99 +  apply (erule mono_sup)
   1.100 +  done
   1.101 +
   1.102 +lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S"
   1.103 +  apply (rule subset_antisym)
   1.104 +  apply (rule Inter_greatest)
   1.105 +  apply (erule Inf_lower)
   1.106 +  apply (rule Inf_greatest)
   1.107 +  apply (erule Inter_lower)
   1.108 +  done
   1.109 +
   1.110 +lemma Sup_set_eq: "\<Squnion>S = \<Union>S"
   1.111 +  apply (rule subset_antisym)
   1.112 +  apply (rule Sup_least)
   1.113 +  apply (erule Union_upper)
   1.114 +  apply (rule Union_least)
   1.115 +  apply (erule Sup_upper)
   1.116 +  done
   1.117 +  
   1.118 +lemma top_set_eq: "top = UNIV"
   1.119 +  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   1.120 +
   1.121 +lemma bot_set_eq: "bot = {}"
   1.122 +  by (iprover intro!: subset_antisym empty_subsetI bot_least)
   1.123 +
   1.124 +
   1.125  text {* redundant bindings *}
   1.126  
   1.127  lemmas inf_aci = inf_ACI