merged
authorhaftmann
Mon Jul 11 07:04:30 2011 +0200 (2011-07-11)
changeset 4375717c36f05b40d
parent 43743 8786e36b8142
parent 43756 15ea1a07a8cf
child 43758 52310132063b
merged
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 21:46:41 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 11 07:04:30 2011 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4    "\<Squnion>{a, b} = a \<squnion> b"
     1.5    by (simp add: Sup_empty Sup_insert)
     1.6  
     1.7 -lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     1.8 +lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     1.9    by (auto intro: Inf_greatest dest: Inf_lower)
    1.10  
    1.11  lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    1.12 @@ -190,58 +190,58 @@
    1.13  lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
    1.14    by (auto simp add: INFI_def intro: Inf_greatest)
    1.15  
    1.16 -lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
    1.17 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
    1.18    unfolding SUPR_def by (auto simp add: Sup_le_iff)
    1.19  
    1.20 -lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
    1.21 +lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
    1.22    unfolding INFI_def by (auto simp add: le_Inf_iff)
    1.23  
    1.24 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
    1.25 +lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. M) = M"
    1.26    by (auto intro: antisym INF_leI le_INFI)
    1.27  
    1.28 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
    1.29 +lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. M) = M"
    1.30    by (auto intro: antisym SUP_leI le_SUPI)
    1.31  
    1.32  lemma INF_mono:
    1.33 -  "(\<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.34 +  "(\<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.35    by (force intro!: Inf_mono simp: INFI_def)
    1.36  
    1.37  lemma SUP_mono:
    1.38 -  "(\<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.39 +  "(\<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.40    by (force intro!: Sup_mono simp: SUPR_def)
    1.41  
    1.42 -lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f"
    1.43 +lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    1.44    by (intro INF_mono) auto
    1.45  
    1.46 -lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
    1.47 +lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
    1.48    by (intro SUP_mono) auto
    1.49  
    1.50 -lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
    1.51 +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.52    by (iprover intro: INF_leI le_INFI order_trans antisym)
    1.53  
    1.54 -lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
    1.55 +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.56    by (iprover intro: SUP_leI le_SUPI order_trans antisym)
    1.57  
    1.58  end
    1.59  
    1.60  lemma Inf_less_iff:
    1.61    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.62 -  shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
    1.63 -  unfolding not_le[symmetric] le_Inf_iff by auto
    1.64 +  shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    1.65 +  unfolding not_le [symmetric] le_Inf_iff by auto
    1.66  
    1.67  lemma less_Sup_iff:
    1.68    fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.69 -  shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
    1.70 -  unfolding not_le[symmetric] Sup_le_iff by auto
    1.71 +  shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
    1.72 +  unfolding not_le [symmetric] Sup_le_iff by auto
    1.73  
    1.74  lemma INF_less_iff:
    1.75    fixes a :: "'a::{complete_lattice,linorder}"
    1.76 -  shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
    1.77 +  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
    1.78    unfolding INFI_def Inf_less_iff by auto
    1.79  
    1.80  lemma less_SUP_iff:
    1.81    fixes a :: "'a::{complete_lattice,linorder}"
    1.82 -  shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
    1.83 +  shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    1.84    unfolding SUPR_def less_Sup_iff by auto
    1.85  
    1.86  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    1.87 @@ -265,7 +265,7 @@
    1.88  proof (rule ext)+
    1.89    fix A :: "'a set"
    1.90    fix P :: "'a \<Rightarrow> bool"
    1.91 -  show "(INF x:A. P x) \<longleftrightarrow> (\<forall>x \<in> A. P x)"
    1.92 +  show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
    1.93      by (auto simp add: Ball_def INFI_def Inf_bool_def)
    1.94  qed
    1.95  
    1.96 @@ -274,7 +274,7 @@
    1.97  proof (rule ext)+
    1.98    fix A :: "'a set"
    1.99    fix P :: "'a \<Rightarrow> bool"
   1.100 -  show "(SUP x:A. P x) \<longleftrightarrow> (\<exists>x \<in> A. P x)"
   1.101 +  show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)"
   1.102      by (auto simp add: Bex_def SUPR_def Sup_bool_def)
   1.103  qed
   1.104  
   1.105 @@ -354,7 +354,7 @@
   1.106  lemma (in complete_lattice) Inf_less_eq:
   1.107    assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
   1.108      and "A \<noteq> {}"
   1.109 -  shows "\<Sqinter>A \<le> u"
   1.110 +  shows "\<Sqinter>A \<sqsubseteq> u"
   1.111  proof -
   1.112    from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   1.113    moreover with assms have "v \<sqsubseteq> u" by blast
   1.114 @@ -362,10 +362,10 @@
   1.115  qed
   1.116  
   1.117  lemma Inter_subset:
   1.118 -  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
   1.119 +  "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.120    by (fact Inf_less_eq)
   1.121  
   1.122 -lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
   1.123 +lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
   1.124    by (fact Inf_greatest)
   1.125  
   1.126  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   1.127 @@ -386,18 +386,25 @@
   1.128  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   1.129    by (fact Inf_inter_less)
   1.130  
   1.131 -(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
   1.132 +lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   1.133 +  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
   1.134  
   1.135  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   1.136 -  by blast
   1.137 +  by (fact Inf_union_distrib)
   1.138 +
   1.139 +(*lemma (in complete_lattice) Inf_top_conv [no_atp]:
   1.140 +  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"*)
   1.141  
   1.142  lemma Inter_UNIV_conv [simp,no_atp]:
   1.143    "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   1.144    "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   1.145    by blast+
   1.146  
   1.147 +lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   1.148 +  by (auto intro: Inf_greatest Inf_lower)
   1.149 +
   1.150  lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
   1.151 -  by blast
   1.152 +  by (fact Inf_anti_mono)
   1.153  
   1.154  
   1.155  subsection {* Intersections of families *}
     2.1 --- a/src/HOL/Lattices.thy	Sun Jul 10 21:46:41 2011 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Mon Jul 11 07:04:30 2011 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4  text {* Dual lattice *}
     2.5  
     2.6  lemma dual_semilattice:
     2.7 -  "class.semilattice_inf (op \<ge>) (op >) sup"
     2.8 +  "class.semilattice_inf greater_eq greater sup"
     2.9  by (rule class.semilattice_inf.intro, rule dual_order)
    2.10    (unfold_locales, simp_all add: sup_least)
    2.11  
    2.12 @@ -104,7 +104,7 @@
    2.13    "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    2.14    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    2.15  
    2.16 -lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    2.17 +lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    2.18    by (fast intro: inf_greatest le_infI1 le_infI2)
    2.19  
    2.20  lemma mono_inf:
    2.21 @@ -141,7 +141,7 @@
    2.22    "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    2.23    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    2.24  
    2.25 -lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    2.26 +lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    2.27    by (fast intro: sup_least le_supI1 le_supI2)
    2.28  
    2.29  lemma mono_sup:
    2.30 @@ -420,7 +420,7 @@
    2.31  begin
    2.32  
    2.33  lemma dual_bounded_lattice:
    2.34 -  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    2.35 +  "class.bounded_lattice greater_eq greater sup inf \<top> \<bottom>"
    2.36    by unfold_locales (auto simp add: less_le_not_le)
    2.37  
    2.38  end
    2.39 @@ -432,7 +432,7 @@
    2.40  begin
    2.41  
    2.42  lemma dual_boolean_algebra:
    2.43 -  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    2.44 +  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus greater_eq greater sup inf \<top> \<bottom>"
    2.45    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    2.46      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    2.47  
    2.48 @@ -506,7 +506,7 @@
    2.49  lemma compl_sup [simp]:
    2.50    "- (x \<squnion> y) = - x \<sqinter> - y"
    2.51  proof -
    2.52 -  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
    2.53 +  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus greater_eq greater sup inf \<top> \<bottom>
    2.54      by (rule dual_boolean_algebra)
    2.55    then show ?thesis by simp
    2.56  qed
    2.57 @@ -523,7 +523,7 @@
    2.58  qed
    2.59  
    2.60  lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
    2.61 -  "- x \<le> - y \<longleftrightarrow> y \<le> x"
    2.62 +  "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
    2.63  by (auto dest: compl_mono)
    2.64  
    2.65  end