1.1 --- a/NEWS Mon Jul 18 21:15:51 2011 +0200
1.2 +++ b/NEWS Mon Jul 18 21:34:01 2011 +0200
1.3 @@ -71,6 +71,7 @@
1.4 le_SUPI ~> le_SUP_I
1.5 le_SUPI2 ~> le_SUP_I2
1.6 le_INFI ~> le_INF_I
1.7 + INF_subset ~> INF_superset_mono
1.8 INFI_bool_eq ~> INF_bool_eq
1.9 SUPR_bool_eq ~> SUP_bool_eq
1.10 INFI_apply ~> INF_apply
2.1 --- a/src/HOL/Complete_Lattice.thy Mon Jul 18 21:15:51 2011 +0200
2.2 +++ b/src/HOL/Complete_Lattice.thy Mon Jul 18 21:34:01 2011 +0200
2.3 @@ -88,6 +88,12 @@
2.4 lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
2.5 by (auto intro: Sup_least dest: Sup_upper)
2.6
2.7 +lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
2.8 + by (auto intro: Inf_greatest Inf_lower)
2.9 +
2.10 +lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
2.11 + by (auto intro: Sup_least Sup_upper)
2.12 +
2.13 lemma Inf_mono:
2.14 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
2.15 shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
2.16 @@ -134,10 +140,10 @@
2.17 ultimately show ?thesis by (rule Sup_upper2)
2.18 qed
2.19
2.20 -lemma Inf_inter_less_eq: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
2.21 +lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
2.22 by (auto intro: Inf_greatest Inf_lower)
2.23
2.24 -lemma Sup_inter_greater_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
2.25 +lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
2.26 by (auto intro: Sup_least Sup_upper)
2.27
2.28 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
2.29 @@ -177,12 +183,6 @@
2.30 from dual.Inf_top_conv show ?P and ?Q by simp_all
2.31 qed
2.32
2.33 -lemma Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
2.34 - by (auto intro: Inf_greatest Inf_lower)
2.35 -
2.36 -lemma Sup_anti_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
2.37 - by (auto intro: Sup_least Sup_upper)
2.38 -
2.39 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
2.40 INF_def: "INFI A f = \<Sqinter> (f ` A)"
2.41
2.42 @@ -285,13 +285,13 @@
2.43 "(\<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.44 by (force intro!: Sup_mono simp: SUP_def)
2.45
2.46 -lemma INF_subset:
2.47 - "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
2.48 - by (intro INF_mono) auto
2.49 +lemma INF_superset_mono:
2.50 + "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
2.51 + by (rule INF_mono) auto
2.52
2.53 -lemma SUP_subset:
2.54 +lemma SUPO_subset_mono:
2.55 "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
2.56 - by (intro SUP_mono) auto
2.57 + by (rule SUP_mono) auto
2.58
2.59 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.60 by (iprover intro: INF_leI le_INF_I order_trans antisym)
2.61 @@ -365,13 +365,13 @@
2.62 "(\<Squnion>b. A b) = A True \<squnion> A False"
2.63 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
2.64
2.65 -lemma INF_anti_mono:
2.66 +lemma INF_mono':
2.67 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
2.68 -- {* The last inclusion is POSITIVE! *}
2.69 - by (blast intro: INF_mono dest: subsetD)
2.70 + by (rule INF_mono) auto
2.71
2.72 -lemma SUP_anti_mono:
2.73 - "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<sqsubseteq> f x) \<Longrightarrow> (\<Squnion>x\<in>B. g x) \<sqsubseteq> (\<Squnion>x\<in>B. f x)"
2.74 +lemma SUP_mono':
2.75 + "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>B. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
2.76 -- {* The last inclusion is POSITIVE! *}
2.77 by (blast intro: SUP_mono dest: subsetD)
2.78
2.79 @@ -554,7 +554,7 @@
2.80 by (fact Inf_insert)
2.81
2.82 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
2.83 - by (fact Inf_inter_less_eq)
2.84 + by (fact less_eq_Inf_inter)
2.85
2.86 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
2.87 by (fact Inf_union_distrib)
2.88 @@ -565,7 +565,7 @@
2.89 by (fact Inf_top_conv)+
2.90
2.91 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
2.92 - by (fact Inf_anti_mono)
2.93 + by (fact Inf_superset_mono)
2.94
2.95
2.96 subsection {* Intersections of families *}
2.97 @@ -682,7 +682,7 @@
2.98 lemma INT_anti_mono:
2.99 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)"
2.100 -- {* The last inclusion is POSITIVE! *}
2.101 - by (fact INF_anti_mono)
2.102 + by (fact INF_mono')
2.103
2.104 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
2.105 by blast
2.106 @@ -1077,6 +1077,7 @@
2.107 lemmas (in complete_lattice) le_SUPI = le_SUP_I
2.108 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
2.109 lemmas (in complete_lattice) le_INFI = le_INF_I
2.110 +lemmas (in complete_lattice) INF_subset = INF_superset_mono
2.111 lemmas INFI_apply = INF_apply
2.112 lemmas SUPR_apply = SUP_apply
2.113