more consistent theorem names
authorhaftmann
Sun Jul 17 20:57:56 2011 +0200 (2011-07-17)
changeset 438726b917e5877d2
parent 43871 79c3231e0593
child 43873 8a2f339641c1
more consistent theorem names
NEWS
src/HOL/Complete_Lattice.thy
     1.1 --- a/NEWS	Sun Jul 17 20:46:51 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 17 20:57:56 2011 +0200
     1.3 @@ -64,8 +64,13 @@
     1.4  uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
     1.5  
     1.6  * Class 'complete_lattice': generalized a couple of lemmas from sets;
     1.7 -generalized theorems INF_cong and SUP_cong.  More consistent names: TBD.
     1.8 -
     1.9 +generalized theorems INF_cong and SUP_cong.  More consistent and less
    1.10 +misunderstandable names:
    1.11 +  INFI_def ~> INF_def
    1.12 +  SUPR_def ~> SUP_def
    1.13 +  le_SUPI ~> le_SUP_I
    1.14 +  le_SUPI2 ~> le_SUP_I2
    1.15 +  le_INFI ~> le_INF_I
    1.16  INCOMPATIBILITY.
    1.17  
    1.18  * Archimedian_Field.thy:
     2.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:46:51 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:57:56 2011 +0200
     2.3 @@ -184,10 +184,16 @@
     2.4    by (auto intro: Sup_least Sup_upper)
     2.5  
     2.6  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
     2.7 -  "INFI A f = \<Sqinter> (f ` A)"
     2.8 +  INF_def: "INFI A f = \<Sqinter> (f ` A)"
     2.9  
    2.10  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.11 -  "SUPR A f = \<Squnion> (f ` A)"
    2.12 +  SUP_def: "SUPR A f = \<Squnion> (f ` A)"
    2.13 +
    2.14 +text {*
    2.15 +  Note: must use names @{const INFI} and @{const SUPR} here instead of
    2.16 +  @{text INF} and @{text SUP} to allow the following syntax coexist
    2.17 +  with the plain constant names.
    2.18 +*}
    2.19  
    2.20  end
    2.21  
    2.22 @@ -222,62 +228,62 @@
    2.23  begin
    2.24  
    2.25  lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
    2.26 -  by (simp add: INFI_def)
    2.27 +  by (simp add: INF_def)
    2.28  
    2.29  lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
    2.30 -  by (simp add: SUPR_def)
    2.31 +  by (simp add: SUP_def)
    2.32  
    2.33  lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
    2.34 -  by (simp add: INFI_def Inf_insert)
    2.35 +  by (simp add: INF_def Inf_insert)
    2.36  
    2.37  lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
    2.38 -  by (simp add: SUPR_def Sup_insert)
    2.39 +  by (simp add: SUP_def Sup_insert)
    2.40  
    2.41  lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    2.42 -  by (auto simp add: INFI_def intro: Inf_lower)
    2.43 +  by (auto simp add: INF_def intro: Inf_lower)
    2.44  
    2.45 -lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    2.46 -  by (auto simp add: SUPR_def intro: Sup_upper)
    2.47 +lemma le_SUP_I: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    2.48 +  by (auto simp add: SUP_def intro: Sup_upper)
    2.49  
    2.50  lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
    2.51    using INF_leI [of i A f] by auto
    2.52  
    2.53 -lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    2.54 -  using le_SUPI [of i A f] by auto
    2.55 +lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    2.56 +  using le_SUP_I [of i A f] by auto
    2.57  
    2.58 -lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    2.59 -  by (auto simp add: INFI_def intro: Inf_greatest)
    2.60 +lemma le_INF_I: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    2.61 +  by (auto simp add: INF_def intro: Inf_greatest)
    2.62  
    2.63  lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
    2.64 -  by (auto simp add: SUPR_def intro: Sup_least)
    2.65 +  by (auto simp add: SUP_def intro: Sup_least)
    2.66  
    2.67  lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
    2.68 -  by (auto simp add: INFI_def le_Inf_iff)
    2.69 +  by (auto simp add: INF_def le_Inf_iff)
    2.70  
    2.71  lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
    2.72 -  by (auto simp add: SUPR_def Sup_le_iff)
    2.73 +  by (auto simp add: SUP_def Sup_le_iff)
    2.74  
    2.75  lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
    2.76 -  by (auto intro: antisym INF_leI le_INFI)
    2.77 +  by (auto intro: antisym INF_leI le_INF_I)
    2.78  
    2.79  lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
    2.80 -  by (auto intro: antisym SUP_leI le_SUPI)
    2.81 +  by (auto intro: antisym SUP_leI le_SUP_I)
    2.82  
    2.83  lemma INF_cong:
    2.84    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
    2.85 -  by (simp add: INFI_def image_def)
    2.86 +  by (simp add: INF_def image_def)
    2.87  
    2.88  lemma SUP_cong:
    2.89    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Squnion>x\<in>A. C x) = (\<Squnion>x\<in>B. D x)"
    2.90 -  by (simp add: SUPR_def image_def)
    2.91 +  by (simp add: SUP_def image_def)
    2.92  
    2.93  lemma INF_mono:
    2.94    "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
    2.95 -  by (force intro!: Inf_mono simp: INFI_def)
    2.96 +  by (force intro!: Inf_mono simp: INF_def)
    2.97  
    2.98  lemma SUP_mono:
    2.99    "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
   2.100 -  by (force intro!: Sup_mono simp: SUPR_def)
   2.101 +  by (force intro!: Sup_mono simp: SUP_def)
   2.102  
   2.103  lemma INF_subset:
   2.104    "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
   2.105 @@ -288,10 +294,10 @@
   2.106    by (intro SUP_mono) auto
   2.107  
   2.108  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.109 -  by (iprover intro: INF_leI le_INFI order_trans antisym)
   2.110 +  by (iprover intro: INF_leI le_INF_I order_trans antisym)
   2.111  
   2.112  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.113 -  by (iprover intro: SUP_leI le_SUPI order_trans antisym)
   2.114 +  by (iprover intro: SUP_leI le_SUP_I order_trans antisym)
   2.115  
   2.116  lemma INF_absorb:
   2.117    assumes "k \<in> I"
   2.118 @@ -311,11 +317,11 @@
   2.119  
   2.120  lemma INF_union:
   2.121    "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
   2.122 -  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)
   2.123 +  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
   2.124  
   2.125  lemma SUP_union:
   2.126    "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
   2.127 -  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUPI)
   2.128 +  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
   2.129  
   2.130  lemma INF_constant:
   2.131    "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   2.132 @@ -327,29 +333,29 @@
   2.133  
   2.134  lemma INF_eq:
   2.135    "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
   2.136 -  by (simp add: INFI_def image_def)
   2.137 +  by (simp add: INF_def image_def)
   2.138  
   2.139  lemma SUP_eq:
   2.140    "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
   2.141 -  by (simp add: SUPR_def image_def)
   2.142 +  by (simp add: SUP_def image_def)
   2.143  
   2.144  lemma INF_top_conv:
   2.145   "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.146   "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   2.147 -  by (auto simp add: INFI_def Inf_top_conv)
   2.148 +  by (auto simp add: INF_def Inf_top_conv)
   2.149  
   2.150  lemma SUP_bot_conv:
   2.151   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.152   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.153 -  by (auto simp add: SUPR_def Sup_bot_conv)
   2.154 +  by (auto simp add: SUP_def Sup_bot_conv)
   2.155  
   2.156  lemma (in complete_lattice) INF_UNIV_range:
   2.157    "(\<Sqinter>x. f x) = \<Sqinter>range f"
   2.158 -  by (fact INFI_def)
   2.159 +  by (fact INF_def)
   2.160  
   2.161  lemma (in complete_lattice) SUP_UNIV_range:
   2.162    "(\<Squnion>x. f x) = \<Squnion>range f"
   2.163 -  by (fact SUPR_def)
   2.164 +  by (fact SUP_def)
   2.165  
   2.166  lemma INF_bool_eq:
   2.167    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   2.168 @@ -384,12 +390,12 @@
   2.169  lemma INF_less_iff:
   2.170    fixes a :: "'a::{complete_lattice,linorder}"
   2.171    shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   2.172 -  unfolding INFI_def Inf_less_iff by auto
   2.173 +  unfolding INF_def Inf_less_iff by auto
   2.174  
   2.175  lemma less_SUP_iff:
   2.176    fixes a :: "'a::{complete_lattice,linorder}"
   2.177    shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   2.178 -  unfolding SUPR_def less_Sup_iff by auto
   2.179 +  unfolding SUP_def less_Sup_iff by auto
   2.180  
   2.181  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
   2.182  
   2.183 @@ -413,7 +419,7 @@
   2.184    fix A :: "'a set"
   2.185    fix P :: "'a \<Rightarrow> bool"
   2.186    show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
   2.187 -    by (auto simp add: Ball_def INFI_def Inf_bool_def)
   2.188 +    by (auto simp add: Ball_def INF_def Inf_bool_def)
   2.189  qed
   2.190  
   2.191  lemma SUPR_bool_eq [simp]:
   2.192 @@ -422,7 +428,7 @@
   2.193    fix A :: "'a set"
   2.194    fix P :: "'a \<Rightarrow> bool"
   2.195    show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
   2.196 -    by (auto simp add: Bex_def SUPR_def Sup_bool_def)
   2.197 +    by (auto simp add: Bex_def SUP_def Sup_bool_def)
   2.198  qed
   2.199  
   2.200  instantiation "fun" :: (type, complete_lattice) complete_lattice
   2.201 @@ -450,11 +456,11 @@
   2.202  
   2.203  lemma INFI_apply:
   2.204    "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   2.205 -  by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply)
   2.206 +  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
   2.207  
   2.208  lemma SUPR_apply:
   2.209    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   2.210 -  by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply)
   2.211 +  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
   2.212  
   2.213  
   2.214  subsection {* Inter *}
   2.215 @@ -537,6 +543,11 @@
   2.216  abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.217    "INTER \<equiv> INFI"
   2.218  
   2.219 +text {*
   2.220 +  Note: must use name @{const INTER} here instead of @{text INT}
   2.221 +  to allow the following syntax coexist with the plain constant name.
   2.222 +*}
   2.223 +
   2.224  syntax
   2.225    "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
   2.226    "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
   2.227 @@ -561,7 +572,7 @@
   2.228  
   2.229  lemma INTER_eq_Inter_image:
   2.230    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
   2.231 -  by (fact INFI_def)
   2.232 +  by (fact INF_def)
   2.233    
   2.234  lemma Inter_def:
   2.235    "\<Inter>S = (\<Inter>x\<in>S. x)"
   2.236 @@ -573,7 +584,7 @@
   2.237  
   2.238  lemma Inter_image_eq [simp]:
   2.239    "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   2.240 -  by (rule sym) (fact INFI_def)
   2.241 +  by (rule sym) (fact INF_def)
   2.242  
   2.243  lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   2.244    by (unfold INTER_def) blast
   2.245 @@ -602,13 +613,13 @@
   2.246    by (fact INF_leI)
   2.247  
   2.248  lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
   2.249 -  by (fact le_INFI)
   2.250 +  by (fact le_INF_I)
   2.251  
   2.252  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
   2.253 -  by (fact INFI_empty)
   2.254 +  by (fact INF_empty)
   2.255  
   2.256  lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   2.257 -  by (fact INFI_absorb)
   2.258 +  by (fact INF_absorb)
   2.259  
   2.260  lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
   2.261    by (fact le_INF_iff)
   2.262 @@ -730,6 +741,11 @@
   2.263  abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.264    "UNION \<equiv> SUPR"
   2.265  
   2.266 +text {*
   2.267 +  Note: must use name @{const UNION} here instead of @{text UN}
   2.268 +  to allow the following syntax coexist with the plain constant name.
   2.269 +*}
   2.270 +
   2.271  syntax
   2.272    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   2.273    "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
   2.274 @@ -763,7 +779,7 @@
   2.275  
   2.276  lemma UNION_eq_Union_image:
   2.277    "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
   2.278 -  by (fact SUPR_def)
   2.279 +  by (fact SUP_def)
   2.280  
   2.281  lemma Union_def:
   2.282    "\<Union>S = (\<Union>x\<in>S. x)"
   2.283 @@ -800,7 +816,7 @@
   2.284    by blast
   2.285  
   2.286  lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
   2.287 -  by (fact le_SUPI)
   2.288 +  by (fact le_SUP_I)
   2.289  
   2.290  lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
   2.291    by (iprover intro: subsetI elim: UN_E dest: subsetD)
   2.292 @@ -1024,6 +1040,17 @@
   2.293    by auto
   2.294  
   2.295  
   2.296 +text {* Legacy names *}
   2.297 +
   2.298 +lemmas (in complete_lattice) INFI_def = INF_def
   2.299 +lemmas (in complete_lattice) SUPR_def = SUP_def
   2.300 +lemmas (in complete_lattice) le_SUPI = le_SUP_I
   2.301 +lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
   2.302 +lemmas (in complete_lattice) le_INFI = le_INF_I
   2.303 +
   2.304 +
   2.305 +text {* Finally *}
   2.306 +
   2.307  no_notation
   2.308    less_eq  (infix "\<sqsubseteq>" 50) and
   2.309    less (infix "\<sqsubset>" 50) and