more uniform naming scheme for Inf/INF and Sup/SUP lemmas
authorhaftmann
Tue Aug 09 08:06:15 2011 +0200 (2011-08-09)
changeset 44103cedaca00789f
parent 44086 c0847967a25a
child 44104 50c067b51135
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
NEWS
src/HOL/Complete_Lattice.thy
     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