moved complete_lattice to Set.thy
authorhaftmann
Thu Mar 05 08:23:09 2009 +0100 (2009-03-05)
changeset 303025ffa9d4dbea7
parent 30301 429612400fe9
child 30303 9c4f4ac0d038
moved complete_lattice to Set.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Thu Mar 05 08:23:08 2009 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Thu Mar 05 08:23:09 2009 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Abstract lattices *}
     1.5  
     1.6  theory Lattices
     1.7 -imports Fun
     1.8 +imports Orderings
     1.9  begin
    1.10  
    1.11  subsection {* Lattices *}
    1.12 @@ -328,135 +328,6 @@
    1.13    min_max.le_infI1 min_max.le_infI2
    1.14  
    1.15  
    1.16 -subsection {* Complete lattices *}
    1.17 -
    1.18 -class complete_lattice = lattice + bot + top +
    1.19 -  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.20 -    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.21 -  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.22 -     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.23 -  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.24 -     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.25 -begin
    1.26 -
    1.27 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
    1.28 -  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    1.29 -
    1.30 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
    1.31 -  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    1.32 -
    1.33 -lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
    1.34 -  unfolding Sup_Inf by auto
    1.35 -
    1.36 -lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
    1.37 -  unfolding Inf_Sup by auto
    1.38 -
    1.39 -lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    1.40 -  by (auto intro: antisym Inf_greatest Inf_lower)
    1.41 -
    1.42 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.43 -  by (auto intro: antisym Sup_least Sup_upper)
    1.44 -
    1.45 -lemma Inf_singleton [simp]:
    1.46 -  "\<Sqinter>{a} = a"
    1.47 -  by (auto intro: antisym Inf_lower Inf_greatest)
    1.48 -
    1.49 -lemma Sup_singleton [simp]:
    1.50 -  "\<Squnion>{a} = a"
    1.51 -  by (auto intro: antisym Sup_upper Sup_least)
    1.52 -
    1.53 -lemma Inf_insert_simp:
    1.54 -  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
    1.55 -  by (cases "A = {}") (simp_all, simp add: Inf_insert)
    1.56 -
    1.57 -lemma Sup_insert_simp:
    1.58 -  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
    1.59 -  by (cases "A = {}") (simp_all, simp add: Sup_insert)
    1.60 -
    1.61 -lemma Inf_binary:
    1.62 -  "\<Sqinter>{a, b} = a \<sqinter> b"
    1.63 -  by (simp add: Inf_insert_simp)
    1.64 -
    1.65 -lemma Sup_binary:
    1.66 -  "\<Squnion>{a, b} = a \<squnion> b"
    1.67 -  by (simp add: Sup_insert_simp)
    1.68 -
    1.69 -lemma bot_def:
    1.70 -  "bot = \<Squnion>{}"
    1.71 -  by (auto intro: antisym Sup_least)
    1.72 -
    1.73 -lemma top_def:
    1.74 -  "top = \<Sqinter>{}"
    1.75 -  by (auto intro: antisym Inf_greatest)
    1.76 -
    1.77 -lemma sup_bot [simp]:
    1.78 -  "x \<squnion> bot = x"
    1.79 -  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
    1.80 -
    1.81 -lemma inf_top [simp]:
    1.82 -  "x \<sqinter> top = x"
    1.83 -  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
    1.84 -
    1.85 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.86 -  "SUPR A f == \<Squnion> (f ` A)"
    1.87 -
    1.88 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.89 -  "INFI A f == \<Sqinter> (f ` A)"
    1.90 -
    1.91 -end
    1.92 -
    1.93 -syntax
    1.94 -  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.95 -  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)
    1.96 -  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.97 -  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 10] 10)
    1.98 -
    1.99 -translations
   1.100 -  "SUP x y. B"   == "SUP x. SUP y. B"
   1.101 -  "SUP x. B"     == "CONST SUPR UNIV (%x. B)"
   1.102 -  "SUP x. B"     == "SUP x:UNIV. B"
   1.103 -  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
   1.104 -  "INF x y. B"   == "INF x. INF y. B"
   1.105 -  "INF x. B"     == "CONST INFI UNIV (%x. B)"
   1.106 -  "INF x. B"     == "INF x:UNIV. B"
   1.107 -  "INF x:A. B"   == "CONST INFI A (%x. B)"
   1.108 -
   1.109 -(* To avoid eta-contraction of body: *)
   1.110 -print_translation {*
   1.111 -let
   1.112 -  fun btr' syn (A :: Abs abs :: ts) =
   1.113 -    let val (x,t) = atomic_abs_tr' abs
   1.114 -    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
   1.115 -  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
   1.116 -in
   1.117 -[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
   1.118 -end
   1.119 -*}
   1.120 -
   1.121 -context complete_lattice
   1.122 -begin
   1.123 -
   1.124 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
   1.125 -  by (auto simp add: SUPR_def intro: Sup_upper)
   1.126 -
   1.127 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
   1.128 -  by (auto simp add: SUPR_def intro: Sup_least)
   1.129 -
   1.130 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
   1.131 -  by (auto simp add: INFI_def intro: Inf_lower)
   1.132 -
   1.133 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
   1.134 -  by (auto simp add: INFI_def intro: Inf_greatest)
   1.135 -
   1.136 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
   1.137 -  by (auto intro: antisym SUP_leI le_SUPI)
   1.138 -
   1.139 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
   1.140 -  by (auto intro: antisym INF_leI le_INFI)
   1.141 -
   1.142 -end
   1.143 -
   1.144 -
   1.145  subsection {* Bool as lattice *}
   1.146  
   1.147  instantiation bool :: distrib_lattice
   1.148 @@ -473,28 +344,6 @@
   1.149  
   1.150  end
   1.151  
   1.152 -instantiation bool :: complete_lattice
   1.153 -begin
   1.154 -
   1.155 -definition
   1.156 -  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
   1.157 -
   1.158 -definition
   1.159 -  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
   1.160 -
   1.161 -instance
   1.162 -  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
   1.163 -
   1.164 -end
   1.165 -
   1.166 -lemma Inf_empty_bool [simp]:
   1.167 -  "\<Sqinter>{}"
   1.168 -  unfolding Inf_bool_def by auto
   1.169 -
   1.170 -lemma not_Sup_empty_bool [simp]:
   1.171 -  "\<not> Sup {}"
   1.172 -  unfolding Sup_bool_def by auto
   1.173 -
   1.174  
   1.175  subsection {* Fun as lattice *}
   1.176  
   1.177 @@ -522,85 +371,6 @@
   1.178  instance "fun" :: (type, distrib_lattice) distrib_lattice
   1.179    by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   1.180  
   1.181 -instantiation "fun" :: (type, complete_lattice) complete_lattice
   1.182 -begin
   1.183 -
   1.184 -definition
   1.185 -  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.186 -
   1.187 -definition
   1.188 -  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.189 -
   1.190 -instance
   1.191 -  by intro_classes
   1.192 -    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   1.193 -      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   1.194 -
   1.195 -end
   1.196 -
   1.197 -lemma Inf_empty_fun:
   1.198 -  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   1.199 -  by rule (auto simp add: Inf_fun_def)
   1.200 -
   1.201 -lemma Sup_empty_fun:
   1.202 -  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   1.203 -  by rule (auto simp add: Sup_fun_def)
   1.204 -
   1.205 -
   1.206 -subsection {* Set as lattice *}
   1.207 -
   1.208 -lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
   1.209 -  apply (rule subset_antisym)
   1.210 -  apply (rule Int_greatest)
   1.211 -  apply (rule inf_le1)
   1.212 -  apply (rule inf_le2)
   1.213 -  apply (rule inf_greatest)
   1.214 -  apply (rule Int_lower1)
   1.215 -  apply (rule Int_lower2)
   1.216 -  done
   1.217 -
   1.218 -lemma sup_set_eq: "A \<squnion> B = A \<union> B"
   1.219 -  apply (rule subset_antisym)
   1.220 -  apply (rule sup_least)
   1.221 -  apply (rule Un_upper1)
   1.222 -  apply (rule Un_upper2)
   1.223 -  apply (rule Un_least)
   1.224 -  apply (rule sup_ge1)
   1.225 -  apply (rule sup_ge2)
   1.226 -  done
   1.227 -
   1.228 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   1.229 -  apply (fold inf_set_eq sup_set_eq)
   1.230 -  apply (erule mono_inf)
   1.231 -  done
   1.232 -
   1.233 -lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   1.234 -  apply (fold inf_set_eq sup_set_eq)
   1.235 -  apply (erule mono_sup)
   1.236 -  done
   1.237 -
   1.238 -lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S"
   1.239 -  apply (rule subset_antisym)
   1.240 -  apply (rule Inter_greatest)
   1.241 -  apply (erule Inf_lower)
   1.242 -  apply (rule Inf_greatest)
   1.243 -  apply (erule Inter_lower)
   1.244 -  done
   1.245 -
   1.246 -lemma Sup_set_eq: "\<Squnion>S = \<Union>S"
   1.247 -  apply (rule subset_antisym)
   1.248 -  apply (rule Sup_least)
   1.249 -  apply (erule Union_upper)
   1.250 -  apply (rule Union_least)
   1.251 -  apply (erule Sup_upper)
   1.252 -  done
   1.253 -  
   1.254 -lemma top_set_eq: "top = UNIV"
   1.255 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   1.256 -
   1.257 -lemma bot_set_eq: "bot = {}"
   1.258 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
   1.259 -
   1.260  
   1.261  text {* redundant bindings *}
   1.262  
   1.263 @@ -611,8 +381,6 @@
   1.264    less_eq  (infix "\<sqsubseteq>" 50) and
   1.265    less (infix "\<sqsubset>" 50) and
   1.266    inf  (infixl "\<sqinter>" 70) and
   1.267 -  sup  (infixl "\<squnion>" 65) and
   1.268 -  Inf  ("\<Sqinter>_" [900] 900) and
   1.269 -  Sup  ("\<Squnion>_" [900] 900)
   1.270 +  sup  (infixl "\<squnion>" 65)
   1.271  
   1.272  end