src/HOL/Lattices.thy
changeset 28692 a2bc5ce0c9fc
parent 28685 275122631271
child 28823 dcbef866c9e2
     1.1 --- a/src/HOL/Lattices.thy	Mon Oct 27 16:14:51 2008 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Mon Oct 27 16:15:47 2008 +0100
     1.3 @@ -332,7 +332,7 @@
     1.4  
     1.5  subsection {* Complete lattices *}
     1.6  
     1.7 -class complete_lattice = lattice + top + bot +
     1.8 +class complete_lattice = lattice + bot + top +
     1.9    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.10      and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.11    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.12 @@ -383,22 +383,26 @@
    1.13    "\<Squnion>{a, b} = a \<squnion> b"
    1.14    by (simp add: Sup_insert_simp)
    1.15  
    1.16 -lemma top_def:
    1.17 -  "top = \<Sqinter>{}"
    1.18 -  by (auto intro: antisym Inf_greatest)
    1.19 -
    1.20  lemma bot_def:
    1.21    "bot = \<Squnion>{}"
    1.22    by (auto intro: antisym Sup_least)
    1.23  
    1.24 -definition
    1.25 -  SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.26 -where
    1.27 +lemma top_def:
    1.28 +  "top = \<Sqinter>{}"
    1.29 +  by (auto intro: antisym Inf_greatest)
    1.30 +
    1.31 +lemma sup_bot [simp]:
    1.32 +  "x \<squnion> bot = x"
    1.33 +  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
    1.34 +
    1.35 +lemma inf_top [simp]:
    1.36 +  "x \<sqinter> top = x"
    1.37 +  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
    1.38 +
    1.39 +definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.40    "SUPR A f == \<Squnion> (f ` A)"
    1.41  
    1.42 -definition
    1.43 -  INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.44 -where
    1.45 +definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.46    "INFI A f == \<Sqinter> (f ` A)"
    1.47  
    1.48  end