# HG changeset patch
# User haftmann
# Date 1312577897 -7200
# Node ID 32881ab55eac60e63a2ab4a8c8cd2b6845e6720b
# Parent  c3d0dac940fcf59e9f504a2dcc151a1497975daf
tuned order: pushing INF and SUP to Inf and Sup

diff -r c3d0dac940fc -r 32881ab55eac src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Aug 05 22:45:57 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Aug 05 22:58:17 2011 +0200
@@ -38,34 +38,146 @@
     (unfold_locales, (fact bot_least top_greatest
         Sup_upper Sup_least Inf_lower Inf_greatest)+)
 
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
-  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  INF_def: "INFI A f = \<Sqinter>(f ` A)"
+
+definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  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
+
+syntax
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+translations
+  "INF x y. B"   == "INF x. INF y. B"
+  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
+  "INF x. B"     == "INF x:CONST UNIV. B"
+  "INF x:A. B"   == "CONST INFI A (%x. B)"
+  "SUP x y. B"   == "SUP x. SUP y. B"
+  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
+  "SUP x. B"     == "SUP x:CONST UNIV. B"
+  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
+
+print_translation {*
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
+    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+*} -- {* to avoid eta-contraction of body *}
+
+context complete_lattice
+begin
 
-lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
-  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+lemma INF_foundation_dual [no_atp]:
+  "complete_lattice.SUPR Inf = INFI"
+proof (rule ext)+
+  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+    by (fact dual_complete_lattice)
+  fix f :: "'b \<Rightarrow> 'a" and A
+  show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
+    by (simp only: dual.SUP_def INF_def)
+qed
+
+lemma SUP_foundation_dual [no_atp]:
+  "complete_lattice.INFI Sup = SUPR"
+proof (rule ext)+
+  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+    by (fact dual_complete_lattice)
+  fix f :: "'b \<Rightarrow> 'a" and A
+  show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
+    by (simp only: dual.INF_def SUP_def)
+qed
+
+lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
+  by (auto simp add: INF_def intro: Inf_lower)
+
+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 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: SUP_def intro: Sup_least)
+
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
+  using Inf_lower [of u A] by auto
+
+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 Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
+  using Sup_upper [of u A] 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_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+  by (auto intro: Inf_greatest dest: Inf_lower)
+
+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: INF_def le_Inf_iff)
+
+lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+  by (auto intro: Sup_least dest: Sup_upper)
+
+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: SUP_def Sup_le_iff)
 
 lemma Inf_empty [simp]:
   "\<Sqinter>{} = \<top>"
   by (auto intro: antisym Inf_greatest)
 
+lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
+  by (simp add: INF_def)
+
 lemma Sup_empty [simp]:
   "\<Squnion>{} = \<bottom>"
   by (auto intro: antisym Sup_least)
 
+lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
+  by (simp add: SUP_def)
+
 lemma Inf_UNIV [simp]:
   "\<Sqinter>UNIV = \<bottom>"
-  by (simp add: Sup_Inf Sup_empty [symmetric])
+  by (auto intro!: antisym Inf_lower)
 
 lemma Sup_UNIV [simp]:
   "\<Squnion>UNIV = \<top>"
-  by (simp add: Inf_Sup Inf_empty [symmetric])
+  by (auto intro!: antisym Sup_upper)
 
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
+lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+  by (simp add: INF_def Inf_insert)
+
 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
+lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+  by (simp add: SUP_def Sup_insert)
+
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
+  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+
+lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
+  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+
 lemma Inf_singleton [simp]:
   "\<Sqinter>{a} = a"
   by (auto intro: antisym Inf_lower Inf_greatest)
@@ -82,12 +194,6 @@
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_insert)
 
-lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
-  by (auto intro: Inf_greatest dest: Inf_lower)
-
-lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
-  by (auto intro: Sup_least dest: Sup_upper)
-
 lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   by (auto intro: Inf_greatest Inf_lower)
 
@@ -114,12 +220,6 @@
   with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
 qed
 
-lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
-  using Sup_upper [of u A] by auto
-
-lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
-  using Inf_lower [of u A] by auto
-
 lemma Inf_less_eq:
   assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
     and "A \<noteq> {}"
@@ -183,86 +283,6 @@
   from dual.Inf_top_conv show ?P and ?Q by simp_all
 qed
 
-definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  INF_def: "INFI A f = \<Sqinter>(f ` A)"
-
-definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  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
-
-syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
-
-syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-translations
-  "INF x y. B"   == "INF x. INF y. B"
-  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
-  "INF x. B"     == "INF x:CONST UNIV. B"
-  "INF x:A. B"   == "CONST INFI A (%x. B)"
-  "SUP x y. B"   == "SUP x. SUP y. B"
-  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
-  "SUP x. B"     == "SUP x:CONST UNIV. B"
-  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
-
-print_translation {*
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
-    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
-*} -- {* to avoid eta-contraction of body *}
-
-context complete_lattice
-begin
-
-lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
-  by (simp add: INF_def)
-
-lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
-  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: INF_def Inf_insert)
-
-lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
-  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: INF_def intro: Inf_lower)
-
-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_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_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: 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: 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: 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_INF_I)
 
@@ -397,26 +417,6 @@
   "(\<Squnion>b. A b) = A True \<squnion> A False"
   by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
 
-lemma INF_foundation_dual [no_atp]:
-  "complete_lattice.SUPR Inf = INFI"
-proof (rule ext)+
-  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
-    by (fact dual_complete_lattice)
-  fix f :: "'b \<Rightarrow> 'a" and A
-  show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
-    by (simp only: dual.SUP_def INF_def)
-qed
-
-lemma SUP_foundation_dual [no_atp]:
-  "complete_lattice.INFI Sup = SUPR"
-proof (rule ext)+
-  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
-    by (fact dual_complete_lattice)
-  fix f :: "'b \<Rightarrow> 'a" and A
-  show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
-    by (simp only: dual.INF_def SUP_def)
-qed
-
 end
 
 class complete_distrib_lattice = complete_lattice +