1.1 --- a/NEWS Tue Aug 09 07:44:17 2011 +0200
1.2 +++ b/NEWS Tue Aug 09 08:06:15 2011 +0200
1.3 @@ -67,19 +67,27 @@
1.4 generalized theorems INF_cong and SUP_cong. New type classes for complete
1.5 boolean algebras and complete linear orders. Lemmas Inf_less_iff,
1.6 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
1.7 -Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
1.8 -Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have
1.9 -been discarded.
1.10 +Changed proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
1.11 +Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
1.12 +INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
1.13 +INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,
1.14 +Union_def, UN_singleton, UN_eq have been discarded.
1.15 More consistent and less misunderstandable names:
1.16 INFI_def ~> INF_def
1.17 SUPR_def ~> SUP_def
1.18 - le_SUPI ~> le_SUP_I
1.19 - le_SUPI2 ~> le_SUP_I2
1.20 - le_INFI ~> le_INF_I
1.21 + INF_leI ~> INF_lower
1.22 + INF_leI2 ~> INF_lower2
1.23 + le_INFI ~> INF_greatest
1.24 + le_SUPI ~> SUP_upper
1.25 + le_SUPI2 ~> SUP_upper2
1.26 + SUP_leI ~> SUP_least
1.27 INFI_bool_eq ~> INF_bool_eq
1.28 SUPR_bool_eq ~> SUP_bool_eq
1.29 INFI_apply ~> INF_apply
1.30 SUPR_apply ~> SUP_apply
1.31 + INTER_def ~> INTER_eq
1.32 + UNION_def ~> UNION_eq
1.33 +
1.34 INCOMPATIBILITY.
1.35
1.36 * Theorem collections ball_simps and bex_simps do not contain theorems referring
2.1 --- a/src/HOL/Complete_Lattice.thy Tue Aug 09 07:44:17 2011 +0200
2.2 +++ b/src/HOL/Complete_Lattice.thy Tue Aug 09 08:06:15 2011 +0200
2.3 @@ -1,4 +1,4 @@
2.4 -(* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
2.5 + (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
2.6
2.7 header {* Complete lattices, with special focus on sets *}
2.8
2.9 @@ -102,29 +102,29 @@
2.10 by (simp only: dual.INF_def SUP_def)
2.11 qed
2.12
2.13 -lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
2.14 +lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
2.15 by (auto simp add: INF_def intro: Inf_lower)
2.16
2.17 -lemma le_SUP_I: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
2.18 +lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
2.19 + by (auto simp add: INF_def intro: Inf_greatest)
2.20 +
2.21 +lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
2.22 by (auto simp add: SUP_def intro: Sup_upper)
2.23
2.24 -lemma le_INF_I: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
2.25 - by (auto simp add: INF_def intro: Inf_greatest)
2.26 -
2.27 -lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
2.28 +lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
2.29 by (auto simp add: SUP_def intro: Sup_least)
2.30
2.31 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
2.32 using Inf_lower [of u A] by auto
2.33
2.34 -lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
2.35 - using INF_leI [of i A f] by auto
2.36 +lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
2.37 + using INF_lower [of i A f] by auto
2.38
2.39 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
2.40 using Sup_upper [of u A] by auto
2.41
2.42 -lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
2.43 - using le_SUP_I [of i A f] by auto
2.44 +lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
2.45 + using SUP_upper [of i A f] by auto
2.46
2.47 lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
2.48 by (auto intro: Inf_greatest dest: Inf_lower)
2.49 @@ -266,21 +266,21 @@
2.50
2.51 lemma INF_union:
2.52 "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
2.53 - by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
2.54 + by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
2.55
2.56 lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
2.57 by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
2.58
2.59 lemma SUP_union:
2.60 "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
2.61 - by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
2.62 + by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
2.63
2.64 lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
2.65 - by (rule antisym) (rule le_INF_I, auto intro: le_infI1 le_infI2 INF_leI INF_mono)
2.66 + by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
2.67
2.68 lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
2.69 - by (rule antisym) (auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono,
2.70 - rule SUP_leI, auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono)
2.71 + by (rule antisym) (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono,
2.72 + rule SUP_least, auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
2.73
2.74 lemma Inf_top_conv (*[simp]*) [no_atp]:
2.75 "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
2.76 @@ -324,10 +324,10 @@
2.77 by (auto simp add: SUP_def Sup_bot_conv)
2.78
2.79 lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
2.80 - by (auto intro: antisym INF_leI le_INF_I)
2.81 + by (auto intro: antisym INF_lower INF_greatest)
2.82
2.83 lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
2.84 - by (auto intro: antisym SUP_leI le_SUP_I)
2.85 + by (auto intro: antisym SUP_upper SUP_least)
2.86
2.87 lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
2.88 by (cases "A = {}") (simp_all add: INF_empty)
2.89 @@ -336,10 +336,10 @@
2.90 by (cases "A = {}") (simp_all add: SUP_empty)
2.91
2.92 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
2.93 - by (iprover intro: INF_leI le_INF_I order_trans antisym)
2.94 + by (iprover intro: INF_lower INF_greatest order_trans antisym)
2.95
2.96 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
2.97 - by (iprover intro: SUP_leI le_SUP_I order_trans antisym)
2.98 + by (iprover intro: SUP_upper SUP_least order_trans antisym)
2.99
2.100 lemma INF_absorb:
2.101 assumes "k \<in> I"
2.102 @@ -370,7 +370,7 @@
2.103 proof -
2.104 note `y < (\<Sqinter>i\<in>A. f i)`
2.105 also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
2.106 - by (rule INF_leI)
2.107 + by (rule INF_lower)
2.108 finally show "y < f i" .
2.109 qed
2.110
2.111 @@ -378,7 +378,7 @@
2.112 assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
2.113 proof -
2.114 have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
2.115 - by (rule le_SUP_I)
2.116 + by (rule SUP_upper)
2.117 also note `(\<Squnion>i\<in>A. f i) < y`
2.118 finally show "f i < y" .
2.119 qed
2.120 @@ -605,7 +605,7 @@
2.121 by (simp add: Sup_fun_def)
2.122
2.123 instance proof
2.124 -qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_leI le_SUP_I le_INF_I SUP_leI)
2.125 +qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
2.126
2.127 end
2.128
2.129 @@ -759,10 +759,10 @@
2.130 by blast
2.131
2.132 lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a"
2.133 - by (fact INF_leI)
2.134 + by (fact INF_lower)
2.135
2.136 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
2.137 - by (fact le_INF_I)
2.138 + by (fact INF_greatest)
2.139
2.140 lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
2.141 by (fact INF_empty)
2.142 @@ -947,10 +947,10 @@
2.143 by blast
2.144
2.145 lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
2.146 - by (fact le_SUP_I)
2.147 + by (fact SUP_upper)
2.148
2.149 lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
2.150 - by (fact SUP_leI)
2.151 + by (fact SUP_least)
2.152
2.153 lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
2.154 by blast
2.155 @@ -1166,9 +1166,12 @@
2.156
2.157 lemmas (in complete_lattice) INFI_def = INF_def
2.158 lemmas (in complete_lattice) SUPR_def = SUP_def
2.159 -lemmas (in complete_lattice) le_SUPI = le_SUP_I
2.160 -lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
2.161 -lemmas (in complete_lattice) le_INFI = le_INF_I
2.162 +lemmas (in complete_lattice) INF_leI = INF_lower
2.163 +lemmas (in complete_lattice) INF_leI2 = INF_lower2
2.164 +lemmas (in complete_lattice) le_INFI = INF_greatest
2.165 +lemmas (in complete_lattice) le_SUPI = SUP_upper
2.166 +lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
2.167 +lemmas (in complete_lattice) SUP_leI = SUP_least
2.168 lemmas (in complete_lattice) less_INFD = less_INF_D
2.169
2.170 lemmas INFI_apply = INF_apply