1(* Title: HOL/HOLCF/Algebraic.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Algebraic deflations\<close> 6 7theory Algebraic 8imports Universal Map_Functions 9begin 10 11default_sort bifinite 12 13subsection \<open>Type constructor for finite deflations\<close> 14 15typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}" 16by (fast intro: finite_deflation_bottom) 17 18instantiation fin_defl :: (bifinite) below 19begin 20 21definition below_fin_defl_def: 22 "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y" 23 24instance .. 25end 26 27instance fin_defl :: (bifinite) po 28using type_definition_fin_defl below_fin_defl_def 29by (rule typedef_po) 30 31lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)" 32using Rep_fin_defl by simp 33 34lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)" 35using finite_deflation_Rep_fin_defl 36by (rule finite_deflation_imp_deflation) 37 38interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d" 39by (rule finite_deflation_Rep_fin_defl) 40 41lemma fin_defl_belowI: 42 "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b" 43unfolding below_fin_defl_def 44by (rule Rep_fin_defl.belowI) 45 46lemma fin_defl_belowD: 47 "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x" 48unfolding below_fin_defl_def 49by (rule Rep_fin_defl.belowD) 50 51lemma fin_defl_eqI: 52 "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b" 53apply (rule below_antisym) 54apply (rule fin_defl_belowI, simp) 55apply (rule fin_defl_belowI, simp) 56done 57 58lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b" 59unfolding below_fin_defl_def . 60 61lemma Abs_fin_defl_mono: 62 "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk> 63 \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b" 64unfolding below_fin_defl_def 65by (simp add: Abs_fin_defl_inverse) 66 67lemma (in finite_deflation) compact_belowI: 68 assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f" 69by (rule belowI, rule assms, erule subst, rule compact) 70 71lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)" 72using finite_deflation_Rep_fin_defl 73by (rule finite_deflation_imp_compact) 74 75subsection \<open>Defining algebraic deflations by ideal completion\<close> 76 77typedef 'a defl = "{S::'a fin_defl set. below.ideal S}" 78by (rule below.ex_ideal) 79 80instantiation defl :: (bifinite) below 81begin 82 83definition 84 "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y" 85 86instance .. 87end 88 89instance defl :: (bifinite) po 90using type_definition_defl below_defl_def 91by (rule below.typedef_ideal_po) 92 93instance defl :: (bifinite) cpo 94using type_definition_defl below_defl_def 95by (rule below.typedef_ideal_cpo) 96 97definition 98 defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where 99 "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}" 100 101lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f" 102proof - 103 obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f" 104 using compact_basis.countable .. 105 have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})" 106 apply (rule finite_imageI) 107 apply (rule finite_vimageI) 108 apply (rule Rep_fin_defl.finite_fixes) 109 apply (simp add: inj_on_def Rep_compact_basis_inject) 110 done 111 have range_eq: "range Rep_compact_basis = {x. compact x}" 112 using type_definition_compact_basis by (rule type_definition.Rep_range) 113 have "inj (\<lambda>d. set_encode 114 (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))" 115 apply (rule inj_onI) 116 apply (simp only: set_encode_eq *) 117 apply (simp only: inj_image_eq_iff inj_f) 118 apply (drule_tac f="image Rep_compact_basis" in arg_cong) 119 apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff) 120 apply (rule Rep_fin_defl_inject [THEN iffD1]) 121 apply (rule below_antisym) 122 apply (rule Rep_fin_defl.compact_belowI, rename_tac z) 123 apply (drule_tac x=z in spec, simp) 124 apply (rule Rep_fin_defl.compact_belowI, rename_tac z) 125 apply (drule_tac x=z in spec, simp) 126 done 127 thus ?thesis by - (rule exI) 128qed 129 130interpretation defl: ideal_completion below defl_principal Rep_defl 131using type_definition_defl below_defl_def 132using defl_principal_def fin_defl_countable 133by (rule below.typedef_ideal_completion) 134 135text \<open>Algebraic deflations are pointed\<close> 136 137lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x" 138apply (induct x rule: defl.principal_induct, simp) 139apply (rule defl.principal_mono) 140apply (simp add: below_fin_defl_def) 141apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom) 142done 143 144instance defl :: (bifinite) pcpo 145by intro_classes (fast intro: defl_minimal) 146 147lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)" 148by (rule defl_minimal [THEN bottomI, symmetric]) 149 150subsection \<open>Applying algebraic deflations\<close> 151 152definition 153 cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a" 154where 155 "cast = defl.extension Rep_fin_defl" 156 157lemma cast_defl_principal: 158 "cast\<cdot>(defl_principal a) = Rep_fin_defl a" 159unfolding cast_def 160apply (rule defl.extension_principal) 161apply (simp only: below_fin_defl_def) 162done 163 164lemma deflation_cast: "deflation (cast\<cdot>d)" 165apply (induct d rule: defl.principal_induct) 166apply (rule adm_subst [OF _ adm_deflation], simp) 167apply (simp add: cast_defl_principal) 168apply (rule finite_deflation_imp_deflation) 169apply (rule finite_deflation_Rep_fin_defl) 170done 171 172lemma finite_deflation_cast: 173 "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)" 174apply (drule defl.compact_imp_principal, clarify) 175apply (simp add: cast_defl_principal) 176apply (rule finite_deflation_Rep_fin_defl) 177done 178 179interpretation cast: deflation "cast\<cdot>d" 180by (rule deflation_cast) 181 182declare cast.idem [simp] 183 184lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)" 185apply (rule finite_deflation_imp_compact) 186apply (erule finite_deflation_cast) 187done 188 189lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B" 190apply (induct A rule: defl.principal_induct, simp) 191apply (induct B rule: defl.principal_induct, simp) 192apply (simp add: cast_defl_principal below_fin_defl_def) 193done 194 195lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d" 196apply (rule iffI) 197apply (simp only: compact_def cast_below_cast [symmetric]) 198apply (erule adm_subst [OF cont_Rep_cfun2]) 199apply (erule compact_cast) 200done 201 202lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B" 203by (simp only: cast_below_cast) 204 205lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B" 206by (simp add: below_antisym cast_below_imp_below) 207 208lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>" 209apply (subst inst_defl_pcpo) 210apply (subst cast_defl_principal) 211apply (rule Abs_fin_defl_inverse) 212apply (simp add: finite_deflation_bottom) 213done 214 215lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>" 216by (rule cast.below [THEN bottomI]) 217 218subsection \<open>Deflation combinators\<close> 219 220definition 221 "defl_fun1 e p f = 222 defl.extension (\<lambda>a. 223 defl_principal (Abs_fin_defl 224 (e oo f\<cdot>(Rep_fin_defl a) oo p)))" 225 226definition 227 "defl_fun2 e p f = 228 defl.extension (\<lambda>a. 229 defl.extension (\<lambda>b. 230 defl_principal (Abs_fin_defl 231 (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))" 232 233lemma cast_defl_fun1: 234 assumes ep: "ep_pair e p" 235 assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)" 236 shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p" 237proof - 238 have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)" 239 apply (rule ep_pair.finite_deflation_e_d_p [OF ep]) 240 apply (rule f, rule finite_deflation_Rep_fin_defl) 241 done 242 show ?thesis 243 by (induct A rule: defl.principal_induct, simp) 244 (simp only: defl_fun1_def 245 defl.extension_principal 246 defl.extension_mono 247 defl.principal_mono 248 Abs_fin_defl_mono [OF 1 1] 249 monofun_cfun below_refl 250 Rep_fin_defl_mono 251 cast_defl_principal 252 Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) 253qed 254 255lemma cast_defl_fun2: 256 assumes ep: "ep_pair e p" 257 assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow> 258 finite_deflation (f\<cdot>a\<cdot>b)" 259 shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p" 260proof - 261 have 1: "\<And>a b. finite_deflation 262 (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)" 263 apply (rule ep_pair.finite_deflation_e_d_p [OF ep]) 264 apply (rule f, (rule finite_deflation_Rep_fin_defl)+) 265 done 266 show ?thesis 267 apply (induct A rule: defl.principal_induct, simp) 268 apply (induct B rule: defl.principal_induct, simp) 269 by (simp only: defl_fun2_def 270 defl.extension_principal 271 defl.extension_mono 272 defl.principal_mono 273 Abs_fin_defl_mono [OF 1 1] 274 monofun_cfun below_refl 275 Rep_fin_defl_mono 276 cast_defl_principal 277 Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) 278qed 279 280end 281