src/HOL/Complete_Lattice.thy
changeset 43753 fe5e846c0839
parent 43741 fac11b64713c
child 43754 09d455c93bf8
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 21:39:03 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 21:56:39 2011 +0200
     1.3 @@ -190,58 +190,58 @@
     1.4  lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
     1.5    by (auto simp add: INFI_def intro: Inf_greatest)
     1.6  
     1.7 -lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
     1.8 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
     1.9    unfolding SUPR_def by (auto simp add: Sup_le_iff)
    1.10  
    1.11 -lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
    1.12 +lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
    1.13    unfolding INFI_def by (auto simp add: le_Inf_iff)
    1.14  
    1.15 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
    1.16 +lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. M) = M"
    1.17    by (auto intro: antisym INF_leI le_INFI)
    1.18  
    1.19 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
    1.20 +lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. M) = M"
    1.21    by (auto intro: antisym SUP_leI le_SUPI)
    1.22  
    1.23  lemma INF_mono:
    1.24 -  "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
    1.25 +  "(\<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)"
    1.26    by (force intro!: Inf_mono simp: INFI_def)
    1.27  
    1.28  lemma SUP_mono:
    1.29 -  "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
    1.30 +  "(\<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)"
    1.31    by (force intro!: Sup_mono simp: SUPR_def)
    1.32  
    1.33 -lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f"
    1.34 +lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    1.35    by (intro INF_mono) auto
    1.36  
    1.37 -lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
    1.38 +lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
    1.39    by (intro SUP_mono) auto
    1.40  
    1.41 -lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
    1.42 +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)"
    1.43    by (iprover intro: INF_leI le_INFI order_trans antisym)
    1.44  
    1.45 -lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
    1.46 +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)"
    1.47    by (iprover intro: SUP_leI le_SUPI order_trans antisym)
    1.48  
    1.49  end
    1.50  
    1.51  lemma Inf_less_iff:
    1.52    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.53 -  shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
    1.54 +  shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    1.55    unfolding not_le[symmetric] le_Inf_iff by auto
    1.56  
    1.57  lemma less_Sup_iff:
    1.58    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.59 -  shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
    1.60 +  shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
    1.61    unfolding not_le[symmetric] Sup_le_iff by auto
    1.62  
    1.63  lemma INF_less_iff:
    1.64    fixes a :: "'a::{complete_lattice,linorder}"
    1.65 -  shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
    1.66 +  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
    1.67    unfolding INFI_def Inf_less_iff by auto
    1.68  
    1.69  lemma less_SUP_iff:
    1.70    fixes a :: "'a::{complete_lattice,linorder}"
    1.71 -  shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
    1.72 +  shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    1.73    unfolding SUPR_def less_Sup_iff by auto
    1.74  
    1.75  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    1.76 @@ -265,7 +265,7 @@
    1.77  proof (rule ext)+
    1.78    fix A :: "'a set"
    1.79    fix P :: "'a \<Rightarrow> bool"
    1.80 -  show "(INF x:A. P x) \<longleftrightarrow> (\<forall>x \<in> A. P x)"
    1.81 +  show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
    1.82      by (auto simp add: Ball_def INFI_def Inf_bool_def)
    1.83  qed
    1.84  
    1.85 @@ -274,7 +274,7 @@
    1.86  proof (rule ext)+
    1.87    fix A :: "'a set"
    1.88    fix P :: "'a \<Rightarrow> bool"
    1.89 -  show "(SUP x:A. P x) \<longleftrightarrow> (\<exists>x \<in> A. P x)"
    1.90 +  show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
    1.91      by (auto simp add: Bex_def SUPR_def Sup_bool_def)
    1.92  qed
    1.93  
    1.94 @@ -354,7 +354,7 @@
    1.95  lemma (in complete_lattice) Inf_less_eq:
    1.96    assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
    1.97      and "A \<noteq> {}"
    1.98 -  shows "\<Sqinter>A \<le> u"
    1.99 +  shows "\<Sqinter>A \<sqsubseteq> u"
   1.100  proof -
   1.101    from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   1.102    moreover with assms have "v \<sqsubseteq> u" by blast