generalized INT_anti_mono
authorhaftmann
Sun Jul 17 19:55:17 2011 +0200 (2011-07-17)
changeset 43867771014555553
parent 43866 8a50dc70cbff
child 43868 9684251c7ec1
generalized INT_anti_mono
src/HOL/Complete_Lattice.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:48:02 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:55:17 2011 +0200
     1.3 @@ -533,8 +533,6 @@
     1.4    "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
     1.5    by blast
     1.6  
     1.7 --- {* continue generalization from here *}
     1.8 -
     1.9  lemma (in complete_lattice) INF_constant:
    1.10    "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
    1.11    by (simp add: INF_empty)
    1.12 @@ -572,14 +570,14 @@
    1.13    by (fact INF_bool_eq)
    1.14  
    1.15  lemma (in complete_lattice) INF_anti_mono:
    1.16 -  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
    1.17 +  "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)"
    1.18    -- {* The last inclusion is POSITIVE! *}
    1.19 -  by (blast dest: subsetD)
    1.20 +  by (blast intro: INF_mono dest: subsetD)
    1.21  
    1.22  lemma INT_anti_mono:
    1.23 -  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
    1.24 +  "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)"
    1.25    -- {* The last inclusion is POSITIVE! *}
    1.26 -  by (blast dest: subsetD)
    1.27 +  by (fact INF_anti_mono)
    1.28  
    1.29  lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
    1.30    by blast