src/HOLCF/ex/Strict_Fun.thy
changeset 35167 eba22d68a0a7
child 35427 ad039d29e01c
child 35479 dffffe36344a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/ex/Strict_Fun.thy	Wed Feb 17 08:05:16 2010 -0800
     1.3 @@ -0,0 +1,239 @@
     1.4 +(*  Title:      HOLCF/ex/Strict_Fun.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* The Strict Function Type *}
     1.9 +
    1.10 +theory Strict_Fun
    1.11 +imports HOLCF
    1.12 +begin
    1.13 +
    1.14 +pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
    1.15 +  = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    1.16 +by simp_all
    1.17 +
    1.18 +syntax (xsymbols)
    1.19 +  sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0)
    1.20 +
    1.21 +text {* TODO: Define nice syntax for abstraction, application. *}
    1.22 +
    1.23 +definition
    1.24 +  sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
    1.25 +where
    1.26 +  "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
    1.27 +
    1.28 +definition
    1.29 +  sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
    1.30 +where
    1.31 +  "sfun_rep = (\<Lambda> f. Rep_sfun f)"
    1.32 +
    1.33 +lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
    1.34 +  unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
    1.35 +
    1.36 +lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
    1.37 +  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
    1.38 +
    1.39 +lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
    1.40 +  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
    1.41 +
    1.42 +lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
    1.43 +  by (simp add: expand_cfun_eq strictify_conv_if)
    1.44 +
    1.45 +lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
    1.46 +  unfolding sfun_abs_def sfun_rep_def
    1.47 +  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    1.48 +  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
    1.49 +  apply (simp add: expand_cfun_eq strictify_conv_if)
    1.50 +  apply (simp add: Rep_sfun [simplified])
    1.51 +  done
    1.52 +
    1.53 +lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
    1.54 +  unfolding sfun_abs_def sfun_rep_def
    1.55 +  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    1.56 +  apply (simp add: Abs_sfun_inverse)
    1.57 +  done
    1.58 +
    1.59 +lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
    1.60 +apply default
    1.61 +apply (rule sfun_abs_sfun_rep)
    1.62 +apply (simp add: expand_cfun_below strictify_conv_if)
    1.63 +done
    1.64 +
    1.65 +interpretation sfun: ep_pair sfun_rep sfun_abs
    1.66 +  by (rule ep_pair_sfun)
    1.67 +
    1.68 +subsection {* Map functional for strict function space *}
    1.69 +
    1.70 +definition
    1.71 +  sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
    1.72 +where
    1.73 +  "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
    1.74 +
    1.75 +lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
    1.76 +  unfolding sfun_map_def
    1.77 +  by (simp add: cfun_map_ID expand_cfun_eq)
    1.78 +
    1.79 +lemma sfun_map_map:
    1.80 +  assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
    1.81 +  "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.82 +    sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.83 +unfolding sfun_map_def
    1.84 +by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map)
    1.85 +
    1.86 +lemma ep_pair_sfun_map:
    1.87 +  assumes 1: "ep_pair e1 p1"
    1.88 +  assumes 2: "ep_pair e2 p2"
    1.89 +  shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)"
    1.90 +proof
    1.91 +  interpret e1p1: pcpo_ep_pair e1 p1
    1.92 +    unfolding pcpo_ep_pair_def by fact
    1.93 +  interpret e2p2: pcpo_ep_pair e2 p2
    1.94 +    unfolding pcpo_ep_pair_def by fact
    1.95 +  fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    1.96 +    unfolding sfun_map_def
    1.97 +    apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel)
    1.98 +    apply (rule ep_pair.e_inverse)
    1.99 +    apply (rule ep_pair_cfun_map [OF 1 2])
   1.100 +    done
   1.101 +  fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
   1.102 +    unfolding sfun_map_def
   1.103 +    apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel)
   1.104 +    apply (rule ep_pair.e_p_below)
   1.105 +    apply (rule ep_pair_cfun_map [OF 1 2])
   1.106 +    done
   1.107 +qed
   1.108 +
   1.109 +lemma deflation_sfun_map:
   1.110 +  assumes 1: "deflation d1"
   1.111 +  assumes 2: "deflation d2"
   1.112 +  shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
   1.113 +apply (simp add: sfun_map_def)
   1.114 +apply (rule deflation.intro)
   1.115 +apply simp
   1.116 +apply (subst strictify_cancel)
   1.117 +apply (simp add: cfun_map_def deflation_strict 1 2)
   1.118 +apply (simp add: cfun_map_def deflation.idem 1 2)
   1.119 +apply (simp add: sfun.e_below_iff [symmetric])
   1.120 +apply (subst strictify_cancel)
   1.121 +apply (simp add: cfun_map_def deflation_strict 1 2)
   1.122 +apply (rule deflation.below)
   1.123 +apply (rule deflation_cfun_map [OF 1 2])
   1.124 +done
   1.125 +
   1.126 +lemma finite_deflation_sfun_map:
   1.127 +  assumes 1: "finite_deflation d1"
   1.128 +  assumes 2: "finite_deflation d2"
   1.129 +  shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
   1.130 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
   1.131 +  interpret d1: finite_deflation d1 by fact
   1.132 +  interpret d2: finite_deflation d2 by fact
   1.133 +  have "deflation d1" and "deflation d2" by fact+
   1.134 +  thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
   1.135 +  from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   1.136 +    by (rule finite_deflation_cfun_map)
   1.137 +  then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   1.138 +    by (rule finite_deflation.finite_fixes)
   1.139 +  moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
   1.140 +    by (rule inj_onI, simp)
   1.141 +  ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
   1.142 +    by (rule finite_vimageI)
   1.143 +  then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   1.144 +    unfolding sfun_map_def sfun.e_eq_iff [symmetric]
   1.145 +    by (simp add: strictify_cancel
   1.146 +         deflation_strict `deflation d1` `deflation d2`)
   1.147 +qed
   1.148 +
   1.149 +subsection {* Strict function space is bifinite *}
   1.150 +
   1.151 +instantiation sfun :: (bifinite, bifinite) bifinite
   1.152 +begin
   1.153 +
   1.154 +definition
   1.155 +  "approx = (\<lambda>i. sfun_map\<cdot>(approx i)\<cdot>(approx i))"
   1.156 +
   1.157 +instance proof
   1.158 +  show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b))"
   1.159 +    unfolding approx_sfun_def by simp
   1.160 +next
   1.161 +  fix x :: "'a \<rightarrow>! 'b"
   1.162 +  show "(\<Squnion>i. approx i\<cdot>x) = x"
   1.163 +    unfolding approx_sfun_def
   1.164 +    by (simp add: lub_distribs sfun_map_ID [unfolded ID_def])
   1.165 +next
   1.166 +  fix i :: nat and x :: "'a \<rightarrow>! 'b"
   1.167 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   1.168 +    unfolding approx_sfun_def
   1.169 +    by (intro deflation.idem deflation_sfun_map deflation_approx)
   1.170 +next
   1.171 +  fix i :: nat
   1.172 +  show "finite {x::'a \<rightarrow>! 'b. approx i\<cdot>x = x}"
   1.173 +    unfolding approx_sfun_def
   1.174 +    by (intro finite_deflation.finite_fixes
   1.175 +              finite_deflation_sfun_map
   1.176 +              finite_deflation_approx)
   1.177 +qed
   1.178 +
   1.179 +end
   1.180 +
   1.181 +subsection {* Strict function space is representable *}
   1.182 +
   1.183 +instantiation sfun :: (rep, rep) rep
   1.184 +begin
   1.185 +
   1.186 +definition
   1.187 +  "emb = udom_emb oo sfun_map\<cdot>prj\<cdot>emb"
   1.188 +
   1.189 +definition
   1.190 +  "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj"
   1.191 +
   1.192 +instance
   1.193 +apply (default, unfold emb_sfun_def prj_sfun_def)
   1.194 +apply (rule ep_pair_comp)
   1.195 +apply (rule ep_pair_sfun_map)
   1.196 +apply (rule ep_pair_emb_prj)
   1.197 +apply (rule ep_pair_emb_prj)
   1.198 +apply (rule ep_pair_udom)
   1.199 +done
   1.200 +
   1.201 +end
   1.202 +
   1.203 +text {*
   1.204 +  A deflation constructor lets us configure the domain package to work
   1.205 +  with the strict function space type constructor.
   1.206 +*}
   1.207 +
   1.208 +definition
   1.209 +  sfun_defl :: "TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep"
   1.210 +where
   1.211 +  "sfun_defl = TypeRep_fun2 sfun_map"
   1.212 +
   1.213 +lemma cast_sfun_defl:
   1.214 +  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) = udom_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
   1.215 +unfolding sfun_defl_def
   1.216 +apply (rule cast_TypeRep_fun2)
   1.217 +apply (erule (1) finite_deflation_sfun_map)
   1.218 +done
   1.219 +
   1.220 +lemma REP_sfun: "REP('a::rep \<rightarrow>! 'b::rep) = sfun_defl\<cdot>REP('a)\<cdot>REP('b)"
   1.221 +apply (rule cast_eq_imp_eq, rule ext_cfun)
   1.222 +apply (simp add: cast_REP cast_sfun_defl)
   1.223 +apply (simp only: prj_sfun_def emb_sfun_def)
   1.224 +apply (simp add: sfun_map_def cfun_map_def strictify_cancel)
   1.225 +done
   1.226 +
   1.227 +lemma isodefl_sfun:
   1.228 +  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   1.229 +    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
   1.230 +apply (rule isodeflI)
   1.231 +apply (simp add: cast_sfun_defl cast_isodefl)
   1.232 +apply (simp add: emb_sfun_def prj_sfun_def)
   1.233 +apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
   1.234 +done
   1.235 +
   1.236 +setup {*
   1.237 +  Domain_Isomorphism.add_type_constructor
   1.238 +    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map},
   1.239 +        @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID})
   1.240 +*}
   1.241 +
   1.242 +end