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"