src/HOL/Complete_Lattice.thy
 changeset 38705 aaee86c0e237 parent 37767 a2b7a20d6ea3 child 39302 d7728f65b353
```     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Aug 23 19:35:57 2010 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy	Tue Aug 24 14:41:37 2010 +0200
1.3 @@ -88,6 +88,26 @@
1.4  lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
1.5    by (auto intro: Inf_greatest dest: Inf_lower)
1.6
1.7 +lemma Sup_mono:
1.8 +  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
1.9 +  shows "Sup A \<le> Sup B"
1.10 +proof (rule Sup_least)
1.11 +  fix a assume "a \<in> A"
1.12 +  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
1.13 +  from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
1.14 +  with `a \<le> b` show "a \<le> Sup B" by auto
1.15 +qed
1.16 +
1.17 +lemma Inf_mono:
1.18 +  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
1.19 +  shows "Inf A \<le> Inf B"
1.20 +proof (rule Inf_greatest)
1.21 +  fix b assume "b \<in> B"
1.22 +  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
1.23 +  from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
1.24 +  with `a \<le> b` show "Inf A \<le> b" by auto
1.25 +qed
1.26 +
1.27  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.28    "SUPR A f = \<Squnion> (f ` A)"
1.29
1.30 @@ -144,8 +164,25 @@
1.31  lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
1.32    by (auto intro: antisym INF_leI le_INFI)
1.33
1.34 +lemma SUP_mono:
1.35 +  "(\<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.36 +  by (force intro!: Sup_mono simp: SUPR_def)
1.37 +
1.38 +lemma INF_mono:
1.39 +  "(\<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.40 +  by (force intro!: Inf_mono simp: INFI_def)
1.41 +
1.42  end
1.43
1.44 +lemma less_Sup_iff:
1.45 +  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
1.46 +  shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
1.47 +  unfolding not_le[symmetric] Sup_le_iff by auto
1.48 +
1.49 +lemma Inf_less_iff:
1.50 +  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
1.51 +  shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
1.52 +  unfolding not_le[symmetric] le_Inf_iff by auto
1.53
1.54  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
1.55
1.56 @@ -204,6 +241,18 @@
1.57
1.58  end
1.59
1.60 +lemma SUPR_fun_expand:
1.61 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
1.62 +  shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
1.63 +  by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
1.64 +           simp: SUPR_def Sup_fun_def)
1.65 +
1.66 +lemma INFI_fun_expand:
1.67 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
1.68 +  shows "(INF y:A. f y) x = (INF y:A. f y x)"
1.69 +  by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
1.70 +           simp: INFI_def Inf_fun_def)
1.71 +
1.72  lemma Inf_empty_fun:
1.73    "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"