tuned lattices theory fragements; generlized some lemmas from sets to lattices
authorhaftmann
Sat Dec 05 20:02:21 2009 +0100 (2009-12-05)
changeset 34007aea892559fc5
parent 33996 e4fb0daadcff
child 34008 1ce58e8c02ee
tuned lattices theory fragements; generlized some lemmas from sets to lattices
NEWS
src/HOL/Complete_Lattice.thy
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
src/HOL/Library/List_Set.thy
src/HOL/List.thy
src/HOL/Predicate.thy
     1.1 --- a/NEWS	Sat Dec 05 10:18:23 2009 +0100
     1.2 +++ b/NEWS	Sat Dec 05 20:02:21 2009 +0100
     1.3 @@ -11,6 +11,25 @@
     1.4  
     1.5  * Code generation: ML and OCaml code is decorated with signatures.
     1.6  
     1.7 +* Complete_Lattice.thy: lemmas top_def and bot_def have been replaced
     1.8 +by the more convenient lemmas Inf_empty and Sup_empty.  Dropped lemmas
     1.9 +Inf_insert_simp adn Sup_insert_simp, which are subsumed by Inf_insert and
    1.10 +Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
    1.11 +Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot respectively.
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14 +* Finite_Set.thy and List.thy: some lemmas have been generalized from sets to lattices:
    1.15 +  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
    1.16 +  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
    1.17 +  inter_Inter_fold_inter        ~> inf_Inf_fold_inf
    1.18 +  union_Union_fold_union        ~> sup_Sup_fold_sup
    1.19 +  Inter_fold_inter              ~> Inf_fold_inf
    1.20 +  Union_fold_union              ~> Sup_fold_sup
    1.21 +  inter_INTER_fold_inter        ~> inf_INFI_fold_inf
    1.22 +  union_UNION_fold_union        ~> sup_SUPR_fold_sup
    1.23 +  INTER_fold_inter              ~> INFI_fold_inf
    1.24 +  UNION_fold_union              ~> SUPR_fold_sup
    1.25 +
    1.26  
    1.27  *** ML ***
    1.28  
     2.1 --- a/src/HOL/Complete_Lattice.thy	Sat Dec 05 10:18:23 2009 +0100
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Dec 05 20:02:21 2009 +0100
     2.3 @@ -7,10 +7,10 @@
     2.4  begin
     2.5  
     2.6  notation
     2.7 -  less_eq  (infix "\<sqsubseteq>" 50) and
     2.8 +  less_eq (infix "\<sqsubseteq>" 50) and
     2.9    less (infix "\<sqsubset>" 50) and
    2.10 -  inf  (infixl "\<sqinter>" 70) and
    2.11 -  sup  (infixl "\<squnion>" 65) and
    2.12 +  inf (infixl "\<sqinter>" 70) and
    2.13 +  sup (infixl "\<squnion>" 65) and
    2.14    top ("\<top>") and
    2.15    bot ("\<bottom>")
    2.16  
    2.17 @@ -25,7 +25,7 @@
    2.18  
    2.19  subsection {* Abstract complete lattices *}
    2.20  
    2.21 -class complete_lattice = lattice + bot + top + Inf + Sup +
    2.22 +class complete_lattice = bounded_lattice + Inf + Sup +
    2.23    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    2.24       and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    2.25    assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    2.26 @@ -34,22 +34,23 @@
    2.27  
    2.28  lemma dual_complete_lattice:
    2.29    "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    2.30 -  by (auto intro!: complete_lattice.intro dual_lattice
    2.31 -    bot.intro top.intro dual_preorder, unfold_locales)
    2.32 -      (fact bot_least top_greatest
    2.33 -        Sup_upper Sup_least Inf_lower Inf_greatest)+
    2.34 +  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
    2.35 +    (unfold_locales, (fact bot_least top_greatest
    2.36 +        Sup_upper Sup_least Inf_lower Inf_greatest)+)
    2.37  
    2.38 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
    2.39 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
    2.40    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    2.41  
    2.42 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
    2.43 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
    2.44    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    2.45  
    2.46 -lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
    2.47 -  unfolding Sup_Inf by auto
    2.48 +lemma Inf_empty:
    2.49 +  "\<Sqinter>{} = \<top>"
    2.50 +  by (auto intro: antisym Inf_greatest)
    2.51  
    2.52 -lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
    2.53 -  unfolding Inf_Sup by auto
    2.54 +lemma Sup_empty:
    2.55 +  "\<Squnion>{} = \<bottom>"
    2.56 +  by (auto intro: antisym Sup_least)
    2.57  
    2.58  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.59    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    2.60 @@ -65,37 +66,21 @@
    2.61    "\<Squnion>{a} = a"
    2.62    by (auto intro: antisym Sup_upper Sup_least)
    2.63  
    2.64 -lemma Inf_insert_simp:
    2.65 -  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
    2.66 -  by (cases "A = {}") (simp_all, simp add: Inf_insert)
    2.67 -
    2.68 -lemma Sup_insert_simp:
    2.69 -  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
    2.70 -  by (cases "A = {}") (simp_all, simp add: Sup_insert)
    2.71 -
    2.72  lemma Inf_binary:
    2.73    "\<Sqinter>{a, b} = a \<sqinter> b"
    2.74 -  by (auto simp add: Inf_insert_simp)
    2.75 +  by (simp add: Inf_empty Inf_insert)
    2.76  
    2.77  lemma Sup_binary:
    2.78    "\<Squnion>{a, b} = a \<squnion> b"
    2.79 -  by (auto simp add: Sup_insert_simp)
    2.80 -
    2.81 -lemma bot_def:
    2.82 -  "bot = \<Squnion>{}"
    2.83 -  by (auto intro: antisym Sup_least)
    2.84 +  by (simp add: Sup_empty Sup_insert)
    2.85  
    2.86 -lemma top_def:
    2.87 -  "top = \<Sqinter>{}"
    2.88 -  by (auto intro: antisym Inf_greatest)
    2.89 +lemma Inf_UNIV:
    2.90 +  "\<Sqinter>UNIV = bot"
    2.91 +  by (simp add: Sup_Inf Sup_empty [symmetric])
    2.92  
    2.93 -lemma sup_bot [simp]:
    2.94 -  "x \<squnion> bot = x"
    2.95 -  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
    2.96 -
    2.97 -lemma inf_top [simp]:
    2.98 -  "x \<sqinter> top = x"
    2.99 -  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
   2.100 +lemma Sup_UNIV:
   2.101 +  "\<Squnion>UNIV = top"
   2.102 +  by (simp add: Inf_Sup Inf_empty [symmetric])
   2.103  
   2.104  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.105    "SUPR A f = \<Squnion> (f ` A)"
   2.106 @@ -129,16 +114,16 @@
   2.107  context complete_lattice
   2.108  begin
   2.109  
   2.110 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
   2.111 +lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
   2.112    by (auto simp add: SUPR_def intro: Sup_upper)
   2.113  
   2.114 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
   2.115 +lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
   2.116    by (auto simp add: SUPR_def intro: Sup_least)
   2.117  
   2.118 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
   2.119 +lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
   2.120    by (auto simp add: INFI_def intro: Inf_lower)
   2.121  
   2.122 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
   2.123 +lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
   2.124    by (auto simp add: INFI_def intro: Inf_greatest)
   2.125  
   2.126  lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
     3.1 --- a/src/HOL/Finite_Set.thy	Sat Dec 05 10:18:23 2009 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Sat Dec 05 20:02:21 2009 +0100
     3.3 @@ -2937,37 +2937,6 @@
     3.4  
     3.5  end
     3.6  
     3.7 -context complete_lattice
     3.8 -begin
     3.9 -
    3.10 -text {*
    3.11 -  Coincidence on finite sets in complete lattices:
    3.12 -*}
    3.13 -
    3.14 -lemma Inf_fin_Inf:
    3.15 -  assumes "finite A" and "A \<noteq> {}"
    3.16 -  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
    3.17 -proof -
    3.18 -    interpret ab_semigroup_idem_mult inf
    3.19 -    by (rule ab_semigroup_idem_mult_inf)
    3.20 -  from assms show ?thesis
    3.21 -  unfolding Inf_fin_def by (induct A set: finite)
    3.22 -    (simp_all add: Inf_insert_simp)
    3.23 -qed
    3.24 -
    3.25 -lemma Sup_fin_Sup:
    3.26 -  assumes "finite A" and "A \<noteq> {}"
    3.27 -  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
    3.28 -proof -
    3.29 -  interpret ab_semigroup_idem_mult sup
    3.30 -    by (rule ab_semigroup_idem_mult_sup)
    3.31 -  from assms show ?thesis
    3.32 -  unfolding Sup_fin_def by (induct A set: finite)
    3.33 -    (simp_all add: Sup_insert_simp)
    3.34 -qed
    3.35 -
    3.36 -end
    3.37 -
    3.38  
    3.39  subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
    3.40  
    3.41 @@ -3345,15 +3314,15 @@
    3.42  proof
    3.43  qed auto
    3.44  
    3.45 -lemma fun_left_comm_idem_inter:
    3.46 -  "fun_left_comm_idem op \<inter>"
    3.47 +lemma (in lower_semilattice) fun_left_comm_idem_inf:
    3.48 +  "fun_left_comm_idem inf"
    3.49  proof
    3.50 -qed auto
    3.51 -
    3.52 -lemma fun_left_comm_idem_union:
    3.53 -  "fun_left_comm_idem op \<union>"
    3.54 +qed (auto simp add: inf_left_commute)
    3.55 +
    3.56 +lemma (in upper_semilattice) fun_left_comm_idem_sup:
    3.57 +  "fun_left_comm_idem sup"
    3.58  proof
    3.59 -qed auto
    3.60 +qed (auto simp add: sup_left_commute)
    3.61  
    3.62  lemma union_fold_insert:
    3.63    assumes "finite A"
    3.64 @@ -3371,60 +3340,95 @@
    3.65    from `finite A` show ?thesis by (induct A arbitrary: B) auto
    3.66  qed
    3.67  
    3.68 -lemma inter_Inter_fold_inter:
    3.69 +context complete_lattice
    3.70 +begin
    3.71 +
    3.72 +lemma inf_Inf_fold_inf:
    3.73    assumes "finite A"
    3.74 -  shows "B \<inter> Inter A = fold (op \<inter>) B A"
    3.75 +  shows "inf B (Inf A) = fold inf B A"
    3.76  proof -
    3.77 -  interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
    3.78 +  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
    3.79    from `finite A` show ?thesis by (induct A arbitrary: B)
    3.80 -    (simp_all add: fold_fun_comm Int_commute)
    3.81 +    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
    3.82  qed
    3.83  
    3.84 -lemma union_Union_fold_union:
    3.85 +lemma sup_Sup_fold_sup:
    3.86    assumes "finite A"
    3.87 -  shows "B \<union> Union A = fold (op \<union>) B A"
    3.88 +  shows "sup B (Sup A) = fold sup B A"
    3.89  proof -
    3.90 -  interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
    3.91 +  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
    3.92    from `finite A` show ?thesis by (induct A arbitrary: B)
    3.93 -    (simp_all add: fold_fun_comm Un_commute)
    3.94 +    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
    3.95  qed
    3.96  
    3.97 -lemma Inter_fold_inter:
    3.98 +lemma Inf_fold_inf:
    3.99    assumes "finite A"
   3.100 -  shows "Inter A = fold (op \<inter>) UNIV A"
   3.101 -  using assms inter_Inter_fold_inter [of A UNIV] by simp
   3.102 -
   3.103 -lemma Union_fold_union:
   3.104 +  shows "Inf A = fold inf top A"
   3.105 +  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
   3.106 +
   3.107 +lemma Sup_fold_sup:
   3.108    assumes "finite A"
   3.109 -  shows "Union A = fold (op \<union>) {} A"
   3.110 -  using assms union_Union_fold_union [of A "{}"] by simp
   3.111 -
   3.112 -lemma inter_INTER_fold_inter:
   3.113 -  assumes "finite A"
   3.114 -  shows "B \<inter> INTER A f = fold (\<lambda>A. op \<inter> (f A)) B A" (is "?inter = ?fold") 
   3.115 -proof (rule sym)
   3.116 -  interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
   3.117 -  interpret fun_left_comm_idem "\<lambda>A. op \<inter> (f A)" by (fact fun_left_comm_idem_apply)
   3.118 -  from `finite A` show "?fold = ?inter" by (induct A arbitrary: B) auto
   3.119 +  shows "Sup A = fold sup bot A"
   3.120 +  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
   3.121 +
   3.122 +lemma Inf_fin_Inf:
   3.123 +  assumes "finite A" and "A \<noteq> {}"
   3.124 +  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
   3.125 +proof -
   3.126 +  interpret ab_semigroup_idem_mult inf
   3.127 +    by (rule ab_semigroup_idem_mult_inf)
   3.128 +  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
   3.129 +  moreover with `finite A` have "finite B" by simp
   3.130 +  ultimately show ?thesis  
   3.131 +  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
   3.132 +    (simp add: Inf_fold_inf)
   3.133  qed
   3.134  
   3.135 -lemma union_UNION_fold_union:
   3.136 +lemma Sup_fin_Sup:
   3.137 +  assumes "finite A" and "A \<noteq> {}"
   3.138 +  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
   3.139 +proof -
   3.140 +  interpret ab_semigroup_idem_mult sup
   3.141 +    by (rule ab_semigroup_idem_mult_sup)
   3.142 +  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
   3.143 +  moreover with `finite A` have "finite B" by simp
   3.144 +  ultimately show ?thesis  
   3.145 +  by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
   3.146 +    (simp add: Sup_fold_sup)
   3.147 +qed
   3.148 +
   3.149 +lemma inf_INFI_fold_inf:
   3.150    assumes "finite A"
   3.151 -  shows "B \<union> UNION A f = fold (\<lambda>A. op \<union> (f A)) B A" (is "?union = ?fold") 
   3.152 +  shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
   3.153  proof (rule sym)
   3.154 -  interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
   3.155 -  interpret fun_left_comm_idem "\<lambda>A. op \<union> (f A)" by (fact fun_left_comm_idem_apply)
   3.156 -  from `finite A` show "?fold = ?union" by (induct A arbitrary: B) auto
   3.157 +  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
   3.158 +  interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
   3.159 +  from `finite A` show "?fold = ?inf"
   3.160 +  by (induct A arbitrary: B)
   3.161 +    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
   3.162  qed
   3.163  
   3.164 -lemma INTER_fold_inter:
   3.165 +lemma sup_SUPR_fold_sup:
   3.166    assumes "finite A"
   3.167 -  shows "INTER A f = fold (\<lambda>A. op \<inter> (f A)) UNIV A"
   3.168 -  using assms inter_INTER_fold_inter [of A UNIV] by simp
   3.169 -
   3.170 -lemma UNION_fold_union:
   3.171 +  shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
   3.172 +proof (rule sym)
   3.173 +  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
   3.174 +  interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
   3.175 +  from `finite A` show "?fold = ?sup"
   3.176 +  by (induct A arbitrary: B)
   3.177 +    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
   3.178 +qed
   3.179 +
   3.180 +lemma INFI_fold_inf:
   3.181    assumes "finite A"
   3.182 -  shows "UNION A f = fold (\<lambda>A. op \<union> (f A)) {} A"
   3.183 -  using assms union_UNION_fold_union [of A "{}"] by simp
   3.184 +  shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
   3.185 +  using assms inf_INFI_fold_inf [of A top] by simp
   3.186 +
   3.187 +lemma SUPR_fold_sup:
   3.188 +  assumes "finite A"
   3.189 +  shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
   3.190 +  using assms sup_SUPR_fold_sup [of A bot] by simp
   3.191  
   3.192  end
   3.193 +
   3.194 +end
     4.1 --- a/src/HOL/Lattices.thy	Sat Dec 05 10:18:23 2009 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Sat Dec 05 20:02:21 2009 +0100
     4.3 @@ -70,7 +70,7 @@
     4.4  
     4.5  lemma mono_inf:
     4.6    fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
     4.7 -  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B"
     4.8 +  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
     4.9    by (auto simp add: mono_def intro: Lattices.inf_greatest)
    4.10  
    4.11  end
    4.12 @@ -104,7 +104,7 @@
    4.13  
    4.14  lemma mono_sup:
    4.15    fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
    4.16 -  shows "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)"
    4.17 +  shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
    4.18    by (auto simp add: mono_def intro: Lattices.sup_least)
    4.19  
    4.20  end
    4.21 @@ -241,22 +241,22 @@
    4.22  begin
    4.23  
    4.24  lemma less_supI1:
    4.25 -  "x < a \<Longrightarrow> x < a \<squnion> b"
    4.26 +  "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    4.27  proof -
    4.28    interpret dual: lower_semilattice "op \<ge>" "op >" sup
    4.29      by (fact dual_semilattice)
    4.30 -  assume "x < a"
    4.31 -  then show "x < a \<squnion> b"
    4.32 +  assume "x \<sqsubset> a"
    4.33 +  then show "x \<sqsubset> a \<squnion> b"
    4.34      by (fact dual.less_infI1)
    4.35  qed
    4.36  
    4.37  lemma less_supI2:
    4.38 -  "x < b \<Longrightarrow> x < a \<squnion> b"
    4.39 +  "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    4.40  proof -
    4.41    interpret dual: lower_semilattice "op \<ge>" "op >" sup
    4.42      by (fact dual_semilattice)
    4.43 -  assume "x < b"
    4.44 -  then show "x < a \<squnion> b"
    4.45 +  assume "x \<sqsubset> b"
    4.46 +  then show "x \<sqsubset> a \<squnion> b"
    4.47      by (fact dual.less_infI2)
    4.48  qed
    4.49  
    4.50 @@ -294,58 +294,46 @@
    4.51  end
    4.52  
    4.53  
    4.54 -subsection {* Boolean algebras *}
    4.55 +subsection {* Bounded lattices and boolean algebras *}
    4.56  
    4.57 -class boolean_algebra = distrib_lattice + top + bot + minus + uminus +
    4.58 -  assumes inf_compl_bot: "x \<sqinter> - x = bot"
    4.59 -    and sup_compl_top: "x \<squnion> - x = top"
    4.60 -  assumes diff_eq: "x - y = x \<sqinter> - y"
    4.61 +class bounded_lattice = lattice + top + bot
    4.62  begin
    4.63  
    4.64 -lemma dual_boolean_algebra:
    4.65 -  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot"
    4.66 -  by (rule boolean_algebra.intro, rule dual_distrib_lattice)
    4.67 -    (unfold_locales,
    4.68 -      auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le)
    4.69 -
    4.70 -lemma compl_inf_bot:
    4.71 -  "- x \<sqinter> x = bot"
    4.72 -  by (simp add: inf_commute inf_compl_bot)
    4.73 -
    4.74 -lemma compl_sup_top:
    4.75 -  "- x \<squnion> x = top"
    4.76 -  by (simp add: sup_commute sup_compl_top)
    4.77 +lemma dual_bounded_lattice:
    4.78 +  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    4.79 +  by (rule bounded_lattice.intro, rule dual_lattice)
    4.80 +    (unfold_locales, auto simp add: less_le_not_le)
    4.81  
    4.82  lemma inf_bot_left [simp]:
    4.83 -  "bot \<sqinter> x = bot"
    4.84 +  "\<bottom> \<sqinter> x = \<bottom>"
    4.85    by (rule inf_absorb1) simp
    4.86  
    4.87  lemma inf_bot_right [simp]:
    4.88 -  "x \<sqinter> bot = bot"
    4.89 +  "x \<sqinter> \<bottom> = \<bottom>"
    4.90    by (rule inf_absorb2) simp
    4.91  
    4.92  lemma sup_top_left [simp]:
    4.93 -  "top \<squnion> x = top"
    4.94 +  "\<top> \<squnion> x = \<top>"
    4.95    by (rule sup_absorb1) simp
    4.96  
    4.97  lemma sup_top_right [simp]:
    4.98 -  "x \<squnion> top = top"
    4.99 +  "x \<squnion> \<top> = \<top>"
   4.100    by (rule sup_absorb2) simp
   4.101  
   4.102  lemma inf_top_left [simp]:
   4.103 -  "top \<sqinter> x = x"
   4.104 +  "\<top> \<sqinter> x = x"
   4.105    by (rule inf_absorb2) simp
   4.106  
   4.107  lemma inf_top_right [simp]:
   4.108 -  "x \<sqinter> top = x"
   4.109 +  "x \<sqinter> \<top> = x"
   4.110    by (rule inf_absorb1) simp
   4.111  
   4.112  lemma sup_bot_left [simp]:
   4.113 -  "bot \<squnion> x = x"
   4.114 +  "\<bottom> \<squnion> x = x"
   4.115    by (rule sup_absorb2) simp
   4.116  
   4.117  lemma sup_bot_right [simp]:
   4.118 -  "x \<squnion> bot = x"
   4.119 +  "x \<squnion> \<bottom> = x"
   4.120    by (rule sup_absorb1) simp
   4.121  
   4.122  lemma inf_eq_top_eq1:
   4.123 @@ -354,8 +342,8 @@
   4.124  proof (cases "B = \<top>")
   4.125    case True with assms show ?thesis by simp
   4.126  next
   4.127 -  case False with top_greatest have "B < \<top>" by (auto intro: neq_le_trans)
   4.128 -  then have "A \<sqinter> B < \<top>" by (rule less_infI2)
   4.129 +  case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans)
   4.130 +  then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2)
   4.131    with assms show ?thesis by simp
   4.132  qed
   4.133  
   4.134 @@ -368,8 +356,8 @@
   4.135    assumes "A \<squnion> B = \<bottom>"
   4.136    shows "A = \<bottom>"
   4.137  proof -
   4.138 -  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
   4.139 -    by (rule dual_boolean_algebra)
   4.140 +  interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   4.141 +    by (rule dual_bounded_lattice)
   4.142    from dual.inf_eq_top_eq1 assms show ?thesis .
   4.143  qed
   4.144  
   4.145 @@ -377,14 +365,35 @@
   4.146    assumes "A \<squnion> B = \<bottom>"
   4.147    shows "B = \<bottom>"
   4.148  proof -
   4.149 -  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
   4.150 -    by (rule dual_boolean_algebra)
   4.151 +  interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   4.152 +    by (rule dual_bounded_lattice)
   4.153    from dual.inf_eq_top_eq2 assms show ?thesis .
   4.154  qed
   4.155  
   4.156 +end
   4.157 +
   4.158 +class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
   4.159 +  assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
   4.160 +    and sup_compl_top: "x \<squnion> - x = \<top>"
   4.161 +  assumes diff_eq: "x - y = x \<sqinter> - y"
   4.162 +begin
   4.163 +
   4.164 +lemma dual_boolean_algebra:
   4.165 +  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   4.166 +  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
   4.167 +    (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
   4.168 +
   4.169 +lemma compl_inf_bot:
   4.170 +  "- x \<sqinter> x = \<bottom>"
   4.171 +  by (simp add: inf_commute inf_compl_bot)
   4.172 +
   4.173 +lemma compl_sup_top:
   4.174 +  "- x \<squnion> x = \<top>"
   4.175 +  by (simp add: sup_commute sup_compl_top)
   4.176 +
   4.177  lemma compl_unique:
   4.178 -  assumes "x \<sqinter> y = bot"
   4.179 -    and "x \<squnion> y = top"
   4.180 +  assumes "x \<sqinter> y = \<bottom>"
   4.181 +    and "x \<squnion> y = \<top>"
   4.182    shows "- x = y"
   4.183  proof -
   4.184    have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
   4.185 @@ -393,7 +402,7 @@
   4.186      by (simp add: inf_commute)
   4.187    then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
   4.188      by (simp add: inf_sup_distrib1)
   4.189 -  then have "- x \<sqinter> top = y \<sqinter> top"
   4.190 +  then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
   4.191      using sup_compl_top assms(2) by simp
   4.192    then show "- x = y" by (simp add: inf_top_right)
   4.193  qed
   4.194 @@ -406,8 +415,8 @@
   4.195    "- x = - y \<longleftrightarrow> x = y"
   4.196  proof
   4.197    assume "- x = - y"
   4.198 -  then have "- x \<sqinter> y = bot"
   4.199 -    and "- x \<squnion> y = top"
   4.200 +  then have "- x \<sqinter> y = \<bottom>"
   4.201 +    and "- x \<squnion> y = \<top>"
   4.202      by (simp_all add: compl_inf_bot compl_sup_top)
   4.203    then have "- (- x) = y" by (rule compl_unique)
   4.204    then show "x = y" by simp
   4.205 @@ -417,16 +426,16 @@
   4.206  qed
   4.207  
   4.208  lemma compl_bot_eq [simp]:
   4.209 -  "- bot = top"
   4.210 +  "- \<bottom> = \<top>"
   4.211  proof -
   4.212 -  from sup_compl_top have "bot \<squnion> - bot = top" .
   4.213 +  from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   4.214    then show ?thesis by simp
   4.215  qed
   4.216  
   4.217  lemma compl_top_eq [simp]:
   4.218 -  "- top = bot"
   4.219 +  "- \<top> = \<bottom>"
   4.220  proof -
   4.221 -  from inf_compl_bot have "top \<sqinter> - top = bot" .
   4.222 +  from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   4.223    then show ?thesis by simp
   4.224  qed
   4.225  
   4.226 @@ -437,21 +446,21 @@
   4.227      by (rule inf_sup_distrib1)
   4.228    also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   4.229      by (simp only: inf_commute inf_assoc inf_left_commute)
   4.230 -  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot"
   4.231 +  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
   4.232      by (simp add: inf_compl_bot)
   4.233  next
   4.234    have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
   4.235      by (rule sup_inf_distrib2)
   4.236    also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   4.237      by (simp only: sup_commute sup_assoc sup_left_commute)
   4.238 -  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top"
   4.239 +  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
   4.240      by (simp add: sup_compl_top)
   4.241  qed
   4.242  
   4.243  lemma compl_sup [simp]:
   4.244    "- (x \<squnion> y) = - x \<sqinter> - y"
   4.245  proof -
   4.246 -  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
   4.247 +  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   4.248      by (rule dual_boolean_algebra)
   4.249    then show ?thesis by simp
   4.250  qed
   4.251 @@ -463,26 +472,26 @@
   4.252  
   4.253  lemma (in lower_semilattice) inf_unique:
   4.254    fixes f (infixl "\<triangle>" 70)
   4.255 -  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
   4.256 -  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   4.257 +  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   4.258 +  and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   4.259    shows "x \<sqinter> y = x \<triangle> y"
   4.260  proof (rule antisym)
   4.261 -  show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   4.262 +  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   4.263  next
   4.264 -  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
   4.265 -  show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all
   4.266 +  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
   4.267 +  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   4.268  qed
   4.269  
   4.270  lemma (in upper_semilattice) sup_unique:
   4.271    fixes f (infixl "\<nabla>" 70)
   4.272 -  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
   4.273 -  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
   4.274 +  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   4.275 +  and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   4.276    shows "x \<squnion> y = x \<nabla> y"
   4.277  proof (rule antisym)
   4.278 -  show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   4.279 +  show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   4.280  next
   4.281 -  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
   4.282 -  show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all
   4.283 +  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   4.284 +  show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   4.285  qed
   4.286    
   4.287  
   4.288 @@ -568,6 +577,8 @@
   4.289  proof
   4.290  qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   4.291  
   4.292 +instance "fun" :: (type, bounded_lattice) bounded_lattice ..
   4.293 +
   4.294  instantiation "fun" :: (type, uminus) uminus
   4.295  begin
   4.296  
     5.1 --- a/src/HOL/Library/List_Set.thy	Sat Dec 05 10:18:23 2009 +0100
     5.2 +++ b/src/HOL/Library/List_Set.thy	Sat Dec 05 20:02:21 2009 +0100
     5.3 @@ -85,50 +85,6 @@
     5.4    "project P (set xs) = set (filter P xs)"
     5.5    by (auto simp add: project_def)
     5.6  
     5.7 -text {* FIXME move the following to @{text Finite_Set.thy} *}
     5.8 -
     5.9 -lemma fun_left_comm_idem_inf:
    5.10 -  "fun_left_comm_idem inf"
    5.11 -proof
    5.12 -qed (auto simp add: inf_left_commute)
    5.13 -
    5.14 -lemma fun_left_comm_idem_sup:
    5.15 -  "fun_left_comm_idem sup"
    5.16 -proof
    5.17 -qed (auto simp add: sup_left_commute)
    5.18 -
    5.19 -lemma inf_Inf_fold_inf:
    5.20 -  fixes A :: "'a::complete_lattice set"
    5.21 -  assumes "finite A"
    5.22 -  shows "inf B (Inf A) = fold inf B A"
    5.23 -proof -
    5.24 -  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
    5.25 -  from `finite A` show ?thesis by (induct A arbitrary: B)
    5.26 -    (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm)
    5.27 -qed
    5.28 -
    5.29 -lemma sup_Sup_fold_sup:
    5.30 -  fixes A :: "'a::complete_lattice set"
    5.31 -  assumes "finite A"
    5.32 -  shows "sup B (Sup A) = fold sup B A"
    5.33 -proof -
    5.34 -  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
    5.35 -  from `finite A` show ?thesis by (induct A arbitrary: B)
    5.36 -    (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm)
    5.37 -qed
    5.38 -
    5.39 -lemma Inf_fold_inf:
    5.40 -  fixes A :: "'a::complete_lattice set"
    5.41 -  assumes "finite A"
    5.42 -  shows "Inf A = fold inf top A"
    5.43 -  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
    5.44 -
    5.45 -lemma Sup_fold_sup:
    5.46 -  fixes A :: "'a::complete_lattice set"
    5.47 -  assumes "finite A"
    5.48 -  shows "Sup A = fold sup bot A"
    5.49 -  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
    5.50 -
    5.51  
    5.52  subsection {* Functorial set operations *}
    5.53  
    5.54 @@ -149,14 +105,6 @@
    5.55      by (simp add: minus_fold_remove [of _ A] fold_set)
    5.56  qed
    5.57  
    5.58 -lemma INFI_set_fold: -- "FIXME move to List.thy"
    5.59 -  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
    5.60 -  unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute)
    5.61 -
    5.62 -lemma SUPR_set_fold: -- "FIXME move to List.thy"
    5.63 -  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
    5.64 -  unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute)
    5.65 -
    5.66  
    5.67  subsection {* Derived set operations *}
    5.68  
     6.1 --- a/src/HOL/List.thy	Sat Dec 05 10:18:23 2009 +0100
     6.2 +++ b/src/HOL/List.thy	Sat Dec 05 20:02:21 2009 +0100
     6.3 @@ -2359,15 +2359,29 @@
     6.4  
     6.5  lemma (in complete_lattice) Inf_set_fold [code_unfold]:
     6.6    "Inf (set xs) = foldl inf top xs"
     6.7 -  by (cases xs)
     6.8 -    (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold
     6.9 -      inf_commute del: set.simps, simp add: top_def)
    6.10 +proof -
    6.11 +  interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.12 +    by (fact fun_left_comm_idem_inf)
    6.13 +  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
    6.14 +qed
    6.15  
    6.16  lemma (in complete_lattice) Sup_set_fold [code_unfold]:
    6.17    "Sup (set xs) = foldl sup bot xs"
    6.18 -  by (cases xs)
    6.19 -    (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold
    6.20 -      sup_commute del: set.simps, simp add: bot_def)
    6.21 +proof -
    6.22 +  interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.23 +    by (fact fun_left_comm_idem_sup)
    6.24 +  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
    6.25 +qed
    6.26 +
    6.27 +lemma (in complete_lattice) INFI_set_fold:
    6.28 +  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
    6.29 +  unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
    6.30 +    by (simp add: inf_commute)
    6.31 +
    6.32 +lemma (in complete_lattice) SUPR_set_fold:
    6.33 +  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
    6.34 +  unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
    6.35 +    by (simp add: sup_commute)
    6.36  
    6.37  
    6.38  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
     7.1 --- a/src/HOL/Predicate.thy	Sat Dec 05 10:18:23 2009 +0100
     7.2 +++ b/src/HOL/Predicate.thy	Sat Dec 05 20:02:21 2009 +0100
     7.3 @@ -726,7 +726,7 @@
     7.4  proof (cases "f ()")
     7.5    case Empty
     7.6    thus ?thesis
     7.7 -    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]  sup_bot)
     7.8 +    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
     7.9  next
    7.10    case Insert
    7.11    thus ?thesis