src/HOL/Complete_Lattice.thy
 changeset 34007 aea892559fc5 parent 32879 7f5ce7af45fd child 35115 446c5063e4fd
```     1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Dec 05 10:18:23 2009 +0100
1.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Dec 05 20:02:21 2009 +0100
1.3 @@ -7,10 +7,10 @@
1.4  begin
1.5
1.6  notation
1.7 -  less_eq  (infix "\<sqsubseteq>" 50) and
1.8 +  less_eq (infix "\<sqsubseteq>" 50) and
1.9    less (infix "\<sqsubset>" 50) and
1.10 -  inf  (infixl "\<sqinter>" 70) and
1.11 -  sup  (infixl "\<squnion>" 65) and
1.12 +  inf (infixl "\<sqinter>" 70) and
1.13 +  sup (infixl "\<squnion>" 65) and
1.14    top ("\<top>") and
1.15    bot ("\<bottom>")
1.16
1.17 @@ -25,7 +25,7 @@
1.18
1.19  subsection {* Abstract complete lattices *}
1.20
1.21 -class complete_lattice = lattice + bot + top + Inf + Sup +
1.22 +class complete_lattice = bounded_lattice + Inf + Sup +
1.23    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
1.24       and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
1.25    assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
1.26 @@ -34,22 +34,23 @@
1.27
1.28  lemma dual_complete_lattice:
1.29    "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
1.30 -  by (auto intro!: complete_lattice.intro dual_lattice
1.31 -    bot.intro top.intro dual_preorder, unfold_locales)
1.32 -      (fact bot_least top_greatest
1.33 -        Sup_upper Sup_least Inf_lower Inf_greatest)+
1.34 +  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
1.35 +    (unfold_locales, (fact bot_least top_greatest
1.36 +        Sup_upper Sup_least Inf_lower Inf_greatest)+)
1.37
1.38 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
1.39 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
1.40    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
1.41
1.42 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
1.43 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
1.44    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
1.45
1.46 -lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
1.47 -  unfolding Sup_Inf by auto
1.48 +lemma Inf_empty:
1.49 +  "\<Sqinter>{} = \<top>"
1.50 +  by (auto intro: antisym Inf_greatest)
1.51
1.52 -lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
1.53 -  unfolding Inf_Sup by auto
1.54 +lemma Sup_empty:
1.55 +  "\<Squnion>{} = \<bottom>"
1.56 +  by (auto intro: antisym Sup_least)
1.57
1.58  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
1.59    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
1.60 @@ -65,37 +66,21 @@
1.61    "\<Squnion>{a} = a"
1.62    by (auto intro: antisym Sup_upper Sup_least)
1.63
1.64 -lemma Inf_insert_simp:
1.65 -  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
1.66 -  by (cases "A = {}") (simp_all, simp add: Inf_insert)
1.67 -
1.68 -lemma Sup_insert_simp:
1.69 -  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
1.70 -  by (cases "A = {}") (simp_all, simp add: Sup_insert)
1.71 -
1.72  lemma Inf_binary:
1.73    "\<Sqinter>{a, b} = a \<sqinter> b"
1.74 -  by (auto simp add: Inf_insert_simp)
1.75 +  by (simp add: Inf_empty Inf_insert)
1.76
1.77  lemma Sup_binary:
1.78    "\<Squnion>{a, b} = a \<squnion> b"
1.79 -  by (auto simp add: Sup_insert_simp)
1.80 -
1.81 -lemma bot_def:
1.82 -  "bot = \<Squnion>{}"
1.83 -  by (auto intro: antisym Sup_least)
1.84 +  by (simp add: Sup_empty Sup_insert)
1.85
1.86 -lemma top_def:
1.87 -  "top = \<Sqinter>{}"
1.88 -  by (auto intro: antisym Inf_greatest)
1.89 +lemma Inf_UNIV:
1.90 +  "\<Sqinter>UNIV = bot"
1.91 +  by (simp add: Sup_Inf Sup_empty [symmetric])
1.92
1.93 -lemma sup_bot [simp]:
1.94 -  "x \<squnion> bot = x"
1.95 -  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
1.96 -
1.97 -lemma inf_top [simp]:
1.98 -  "x \<sqinter> top = x"
1.99 -  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
1.100 +lemma Sup_UNIV:
1.101 +  "\<Squnion>UNIV = top"
1.102 +  by (simp add: Inf_Sup Inf_empty [symmetric])
1.103
1.104  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.105    "SUPR A f = \<Squnion> (f ` A)"
1.106 @@ -129,16 +114,16 @@
1.107  context complete_lattice
1.108  begin
1.109
1.110 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
1.111 +lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
1.112    by (auto simp add: SUPR_def intro: Sup_upper)
1.113
1.114 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
1.115 +lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
1.116    by (auto simp add: SUPR_def intro: Sup_least)
1.117
1.118 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
1.119 +lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
1.120    by (auto simp add: INFI_def intro: Inf_lower)
1.121
1.122 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
1.123 +lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
1.124    by (auto simp add: INFI_def intro: Inf_greatest)
1.125
1.126  lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
```