src/HOLCF/Completion.thy
changeset 28133 218252dfd81e
parent 28053 a2106c0d8c45
child 29138 661a8db7e647
child 29237 e90d9d51106b
     1.1 --- a/src/HOLCF/Completion.thy	Thu Sep 04 17:21:49 2008 +0200
     1.2 +++ b/src/HOLCF/Completion.thy	Thu Sep 04 17:24:18 2008 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4  apply (erule (1) trans_less)
     1.5  done
     1.6  
     1.7 -subsection {* Defining functions in terms of basis elements *}
     1.8 +subsection {* Lemmas about least upper bounds *}
     1.9  
    1.10  lemma finite_directed_contains_lub:
    1.11    "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
    1.12 @@ -191,6 +191,8 @@
    1.13  lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
    1.14  by (erule exE, drule lubI, erule is_lub_lub)
    1.15  
    1.16 +subsection {* Locale for ideal completion *}
    1.17 +
    1.18  locale basis_take = preorder +
    1.19    fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
    1.20    assumes take_less: "take n a \<preceq> a"
    1.21 @@ -221,6 +223,61 @@
    1.22  lemma finite_take_rep: "finite (take n ` rep x)"
    1.23  by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take])
    1.24  
    1.25 +lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
    1.26 +apply (frule bin_chain)
    1.27 +apply (drule rep_contlub)
    1.28 +apply (simp only: thelubI [OF lub_bin_chain])
    1.29 +apply (rule subsetI, rule UN_I [where a=0], simp_all)
    1.30 +done
    1.31 +
    1.32 +lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
    1.33 +by (rule iffI [OF rep_mono subset_repD])
    1.34 +
    1.35 +lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
    1.36 +unfolding less_def rep_principal
    1.37 +apply safe
    1.38 +apply (erule (1) idealD3 [OF ideal_rep])
    1.39 +apply (erule subsetD, simp add: r_refl)
    1.40 +done
    1.41 +
    1.42 +lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
    1.43 +by (simp add: rep_eq)
    1.44 +
    1.45 +lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
    1.46 +by (simp add: rep_eq)
    1.47 +
    1.48 +lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
    1.49 +by (simp add: principal_less_iff_mem_rep rep_principal)
    1.50 +
    1.51 +lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
    1.52 +unfolding po_eq_conv [where 'a='b] principal_less_iff ..
    1.53 +
    1.54 +lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
    1.55 +by (simp add: rep_eq)
    1.56 +
    1.57 +lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
    1.58 +by (simp only: principal_less_iff)
    1.59 +
    1.60 +lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
    1.61 +unfolding principal_less_iff_mem_rep
    1.62 +by (simp add: less_def subset_eq)
    1.63 +
    1.64 +lemma lub_principal_rep: "principal ` rep x <<| x"
    1.65 +apply (rule is_lubI)
    1.66 +apply (rule ub_imageI)
    1.67 +apply (erule repD)
    1.68 +apply (subst less_def)
    1.69 +apply (rule subsetI)
    1.70 +apply (drule (1) ub_imageD)
    1.71 +apply (simp add: rep_eq)
    1.72 +done
    1.73 +
    1.74 +subsection {* Defining functions in terms of basis elements *}
    1.75 +
    1.76 +definition
    1.77 +  basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
    1.78 +  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
    1.79 +
    1.80  lemma basis_fun_lemma0:
    1.81    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
    1.82    assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
    1.83 @@ -278,59 +335,6 @@
    1.84    shows "\<exists>u. f ` rep x <<| u"
    1.85  by (rule exI, rule basis_fun_lemma2, erule f_mono)
    1.86  
    1.87 -lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
    1.88 -apply (frule bin_chain)
    1.89 -apply (drule rep_contlub)
    1.90 -apply (simp only: thelubI [OF lub_bin_chain])
    1.91 -apply (rule subsetI, rule UN_I [where a=0], simp_all)
    1.92 -done
    1.93 -
    1.94 -lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
    1.95 -by (rule iffI [OF rep_mono subset_repD])
    1.96 -
    1.97 -lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
    1.98 -unfolding less_def rep_principal
    1.99 -apply safe
   1.100 -apply (erule (1) idealD3 [OF ideal_rep])
   1.101 -apply (erule subsetD, simp add: r_refl)
   1.102 -done
   1.103 -
   1.104 -lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
   1.105 -by (simp add: rep_eq)
   1.106 -
   1.107 -lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
   1.108 -by (simp add: rep_eq)
   1.109 -
   1.110 -lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
   1.111 -by (simp add: principal_less_iff_mem_rep rep_principal)
   1.112 -
   1.113 -lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
   1.114 -unfolding po_eq_conv [where 'a='b] principal_less_iff ..
   1.115 -
   1.116 -lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
   1.117 -by (simp add: rep_eq)
   1.118 -
   1.119 -lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
   1.120 -by (simp only: principal_less_iff)
   1.121 -
   1.122 -lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
   1.123 -unfolding principal_less_iff_mem_rep
   1.124 -by (simp add: less_def subset_eq)
   1.125 -
   1.126 -lemma lub_principal_rep: "principal ` rep x <<| x"
   1.127 -apply (rule is_lubI)
   1.128 -apply (rule ub_imageI)
   1.129 -apply (erule repD)
   1.130 -apply (subst less_def)
   1.131 -apply (rule subsetI)
   1.132 -apply (drule (1) ub_imageD)
   1.133 -apply (simp add: rep_eq)
   1.134 -done
   1.135 -
   1.136 -definition
   1.137 -  basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
   1.138 -  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
   1.139 -
   1.140  lemma basis_fun_beta:
   1.141    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.142    assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.143 @@ -380,6 +384,8 @@
   1.144  lemma compact_principal [simp]: "compact (principal a)"
   1.145  by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
   1.146  
   1.147 +subsection {* Bifiniteness of ideal completions *}
   1.148 +
   1.149  definition
   1.150    completion_approx :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where
   1.151    "completion_approx = (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"