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>{})"
    1.74    by (simp add: Inf_fun_def)