# HG changeset patch
# User haftmann
# Date 1310925317 -7200
# Node ID 771014555553d94e5d47af05811f923523154f41
# Parent  8a50dc70cbff81818387d8b20cb972bf2ab88768
generalized INT_anti_mono

diff -r 8a50dc70cbff -r 771014555553 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:48:02 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:55:17 2011 +0200
@@ -533,8 +533,6 @@
   "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   by blast
 
--- {* continue generalization from here *}
-
 lemma (in complete_lattice) INF_constant:
   "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   by (simp add: INF_empty)
@@ -572,14 +570,14 @@
   by (fact INF_bool_eq)
 
 lemma (in complete_lattice) INF_anti_mono:
-  "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)"
+  "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)"
   -- {* The last inclusion is POSITIVE! *}
-  by (blast dest: subsetD)
+  by (blast intro: INF_mono dest: subsetD)
 
 lemma INT_anti_mono:
-  "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)"
+  "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)"
   -- {* The last inclusion is POSITIVE! *}
-  by (blast dest: subsetD)
+  by (fact INF_anti_mono)
 
 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
   by blast