# HG changeset patch
# User haftmann
# Date 1310929076 -7200
# Node ID 6b917e5877d285b8ea346960bcd493cbbe1fb1e0
# Parent  79c3231e0593635639e56e8e5ac684b05f1d6dcf
more consistent theorem names

diff -r 79c3231e0593 -r 6b917e5877d2 NEWS
--- a/NEWS	Sun Jul 17 20:46:51 2011 +0200
+++ b/NEWS	Sun Jul 17 20:57:56 2011 +0200
@@ -64,8 +64,13 @@
 uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
 * Class 'complete_lattice': generalized a couple of lemmas from sets;
-generalized theorems INF_cong and SUP_cong.  More consistent names: TBD.
-
+generalized theorems INF_cong and SUP_cong.  More consistent and less
+misunderstandable names:
+  INFI_def ~> INF_def
+  SUPR_def ~> SUP_def
+  le_SUPI ~> le_SUP_I
+  le_SUPI2 ~> le_SUP_I2
+  le_INFI ~> le_INF_I
 INCOMPATIBILITY.
 
 * Archimedian_Field.thy:
diff -r 79c3231e0593 -r 6b917e5877d2 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:46:51 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:57:56 2011 +0200
@@ -184,10 +184,16 @@
   by (auto intro: Sup_least Sup_upper)
 
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "INFI A f = \<Sqinter> (f ` A)"
+  INF_def: "INFI A f = \<Sqinter> (f ` A)"
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "SUPR A f = \<Squnion> (f ` A)"
+  SUP_def: "SUPR A f = \<Squnion> (f ` A)"
+
+text {*
+  Note: must use names @{const INFI} and @{const SUPR} here instead of
+  @{text INF} and @{text SUP} to allow the following syntax coexist
+  with the plain constant names.
+*}
 
 end
 
@@ -222,62 +228,62 @@
 begin
 
 lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
-  by (simp add: INFI_def)
+  by (simp add: INF_def)
 
 lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
-  by (simp add: SUPR_def)
+  by (simp add: SUP_def)
 
 lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
-  by (simp add: INFI_def Inf_insert)
+  by (simp add: INF_def Inf_insert)
 
 lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
-  by (simp add: SUPR_def Sup_insert)
+  by (simp add: SUP_def Sup_insert)
 
 lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
-  by (auto simp add: INFI_def intro: Inf_lower)
+  by (auto simp add: INF_def intro: Inf_lower)
 
-lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
-  by (auto simp add: SUPR_def intro: Sup_upper)
+lemma le_SUP_I: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+  by (auto simp add: SUP_def intro: Sup_upper)
 
 lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
   using INF_leI [of i A f] by auto
 
-lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
-  using le_SUPI [of i A f] by auto
+lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+  using le_SUP_I [of i A f] by auto
 
-lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
-  by (auto simp add: INFI_def intro: Inf_greatest)
+lemma le_INF_I: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
+  by (auto simp add: INF_def intro: Inf_greatest)
 
 lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
-  by (auto simp add: SUPR_def intro: Sup_least)
+  by (auto simp add: SUP_def intro: Sup_least)
 
 lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
-  by (auto simp add: INFI_def le_Inf_iff)
+  by (auto simp add: INF_def le_Inf_iff)
 
 lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
-  by (auto simp add: SUPR_def Sup_le_iff)
+  by (auto simp add: SUP_def Sup_le_iff)
 
 lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
-  by (auto intro: antisym INF_leI le_INFI)
+  by (auto intro: antisym INF_leI le_INF_I)
 
 lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
-  by (auto intro: antisym SUP_leI le_SUPI)
+  by (auto intro: antisym SUP_leI le_SUP_I)
 
 lemma INF_cong:
   "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)"
-  by (simp add: INFI_def image_def)
+  by (simp add: INF_def image_def)
 
 lemma SUP_cong:
   "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)"
-  by (simp add: SUPR_def image_def)
+  by (simp add: SUP_def image_def)
 
 lemma INF_mono:
   "(\<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)"
-  by (force intro!: Inf_mono simp: INFI_def)
+  by (force intro!: Inf_mono simp: INF_def)
 
 lemma SUP_mono:
   "(\<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)"
-  by (force intro!: Sup_mono simp: SUPR_def)
+  by (force intro!: Sup_mono simp: SUP_def)
 
 lemma INF_subset:
   "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
@@ -288,10 +294,10 @@
   by (intro SUP_mono) auto
 
 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)"
-  by (iprover intro: INF_leI le_INFI order_trans antisym)
+  by (iprover intro: INF_leI le_INF_I order_trans antisym)
 
 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)"
-  by (iprover intro: SUP_leI le_SUPI order_trans antisym)
+  by (iprover intro: SUP_leI le_SUP_I order_trans antisym)
 
 lemma INF_absorb:
   assumes "k \<in> I"
@@ -311,11 +317,11 @@
 
 lemma INF_union:
   "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
-  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)
+  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
 
 lemma SUP_union:
   "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
-  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUPI)
+  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
 
 lemma INF_constant:
   "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
@@ -327,29 +333,29 @@
 
 lemma INF_eq:
   "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
-  by (simp add: INFI_def image_def)
+  by (simp add: INF_def image_def)
 
 lemma SUP_eq:
   "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
-  by (simp add: SUPR_def image_def)
+  by (simp add: SUP_def image_def)
 
 lemma INF_top_conv:
  "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
  "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
-  by (auto simp add: INFI_def Inf_top_conv)
+  by (auto simp add: INF_def Inf_top_conv)
 
 lemma SUP_bot_conv:
  "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
-  by (auto simp add: SUPR_def Sup_bot_conv)
+  by (auto simp add: SUP_def Sup_bot_conv)
 
 lemma (in complete_lattice) INF_UNIV_range:
   "(\<Sqinter>x. f x) = \<Sqinter>range f"
-  by (fact INFI_def)
+  by (fact INF_def)
 
 lemma (in complete_lattice) SUP_UNIV_range:
   "(\<Squnion>x. f x) = \<Squnion>range f"
-  by (fact SUPR_def)
+  by (fact SUP_def)
 
 lemma INF_bool_eq:
   "(\<Sqinter>b. A b) = A True \<sqinter> A False"
@@ -384,12 +390,12 @@
 lemma INF_less_iff:
   fixes a :: "'a::{complete_lattice,linorder}"
   shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
-  unfolding INFI_def Inf_less_iff by auto
+  unfolding INF_def Inf_less_iff by auto
 
 lemma less_SUP_iff:
   fixes a :: "'a::{complete_lattice,linorder}"
   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
-  unfolding SUPR_def less_Sup_iff by auto
+  unfolding SUP_def less_Sup_iff by auto
 
 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
@@ -413,7 +419,7 @@
   fix A :: "'a set"
   fix P :: "'a \<Rightarrow> bool"
   show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
-    by (auto simp add: Ball_def INFI_def Inf_bool_def)
+    by (auto simp add: Ball_def INF_def Inf_bool_def)
 qed
 
 lemma SUPR_bool_eq [simp]:
@@ -422,7 +428,7 @@
   fix A :: "'a set"
   fix P :: "'a \<Rightarrow> bool"
   show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
-    by (auto simp add: Bex_def SUPR_def Sup_bool_def)
+    by (auto simp add: Bex_def SUP_def Sup_bool_def)
 qed
 
 instantiation "fun" :: (type, complete_lattice) complete_lattice
@@ -450,11 +456,11 @@
 
 lemma INFI_apply:
   "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
-  by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply)
+  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
 
 lemma SUPR_apply:
   "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
-  by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply)
+  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
 
 
 subsection {* Inter *}
@@ -537,6 +543,11 @@
 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   "INTER \<equiv> INFI"
 
+text {*
+  Note: must use name @{const INTER} here instead of @{text INT}
+  to allow the following syntax coexist with the plain constant name.
+*}
+
 syntax
   "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
   "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
@@ -561,7 +572,7 @@
 
 lemma INTER_eq_Inter_image:
   "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
-  by (fact INFI_def)
+  by (fact INF_def)
   
 lemma Inter_def:
   "\<Inter>S = (\<Inter>x\<in>S. x)"
@@ -573,7 +584,7 @@
 
 lemma Inter_image_eq [simp]:
   "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
-  by (rule sym) (fact INFI_def)
+  by (rule sym) (fact INF_def)
 
 lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
   by (unfold INTER_def) blast
@@ -602,13 +613,13 @@
   by (fact INF_leI)
 
 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
-  by (fact le_INFI)
+  by (fact le_INF_I)
 
 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
-  by (fact INFI_empty)
+  by (fact INF_empty)
 
 lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
-  by (fact INFI_absorb)
+  by (fact INF_absorb)
 
 lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
   by (fact le_INF_iff)
@@ -730,6 +741,11 @@
 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   "UNION \<equiv> SUPR"
 
+text {*
+  Note: must use name @{const UNION} here instead of @{text UN}
+  to allow the following syntax coexist with the plain constant name.
+*}
+
 syntax
   "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
@@ -763,7 +779,7 @@
 
 lemma UNION_eq_Union_image:
   "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
-  by (fact SUPR_def)
+  by (fact SUP_def)
 
 lemma Union_def:
   "\<Union>S = (\<Union>x\<in>S. x)"
@@ -800,7 +816,7 @@
   by blast
 
 lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
-  by (fact le_SUPI)
+  by (fact le_SUP_I)
 
 lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
   by (iprover intro: subsetI elim: UN_E dest: subsetD)
@@ -1024,6 +1040,17 @@
   by auto
 
 
+text {* Legacy names *}
+
+lemmas (in complete_lattice) INFI_def = INF_def
+lemmas (in complete_lattice) SUPR_def = SUP_def
+lemmas (in complete_lattice) le_SUPI = le_SUP_I
+lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
+lemmas (in complete_lattice) le_INFI = le_INF_I
+
+
+text {* Finally *}
+
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and