add theory HOLCF/ex/Strict_Fun.thy
authorhuffman
Wed Feb 17 08:05:16 2010 -0800 (2010-02-17)
changeset 35167eba22d68a0a7
parent 35166 a57ef2cd2236
child 35168 07b3112e464b
add theory HOLCF/ex/Strict_Fun.thy
src/HOLCF/IsaMakefile
src/HOLCF/ex/ROOT.ML
src/HOLCF/ex/Strict_Fun.thy
     1.1 --- a/src/HOLCF/IsaMakefile	Wed Feb 17 13:48:13 2010 +0100
     1.2 +++ b/src/HOLCF/IsaMakefile	Wed Feb 17 08:05:16 2010 -0800
     1.3 @@ -95,6 +95,7 @@
     1.4    ex/Dagstuhl.thy \
     1.5    ex/Dnat.thy \
     1.6    ex/Domain_ex.thy \
     1.7 +  ex/Domain_Proofs.thy \
     1.8    ex/Fix2.thy \
     1.9    ex/Fixrec_ex.thy \
    1.10    ex/Focus_ex.thy \
    1.11 @@ -103,6 +104,7 @@
    1.12    ex/New_Domain.thy \
    1.13    ex/Powerdomain_ex.thy \
    1.14    ex/Stream.thy \
    1.15 +  ex/Strict_Fun.thy \
    1.16    ex/ROOT.ML
    1.17  	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
    1.18  
     2.1 --- a/src/HOLCF/ex/ROOT.ML	Wed Feb 17 13:48:13 2010 +0100
     2.2 +++ b/src/HOLCF/ex/ROOT.ML	Wed Feb 17 08:05:16 2010 -0800
     2.3 @@ -5,4 +5,5 @@
     2.4  
     2.5  use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
     2.6    "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
     2.7 +  "Strict_Fun",
     2.8    "New_Domain"];
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/ex/Strict_Fun.thy	Wed Feb 17 08:05:16 2010 -0800
     3.3 @@ -0,0 +1,239 @@
     3.4 +(*  Title:      HOLCF/ex/Strict_Fun.thy
     3.5 +    Author:     Brian Huffman
     3.6 +*)
     3.7 +
     3.8 +header {* The Strict Function Type *}
     3.9 +
    3.10 +theory Strict_Fun
    3.11 +imports HOLCF
    3.12 +begin
    3.13 +
    3.14 +pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
    3.15 +  = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    3.16 +by simp_all
    3.17 +
    3.18 +syntax (xsymbols)
    3.19 +  sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0)
    3.20 +
    3.21 +text {* TODO: Define nice syntax for abstraction, application. *}
    3.22 +
    3.23 +definition
    3.24 +  sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
    3.25 +where
    3.26 +  "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
    3.27 +
    3.28 +definition
    3.29 +  sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
    3.30 +where
    3.31 +  "sfun_rep = (\<Lambda> f. Rep_sfun f)"
    3.32 +
    3.33 +lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
    3.34 +  unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
    3.35 +
    3.36 +lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
    3.37 +  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
    3.38 +
    3.39 +lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
    3.40 +  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
    3.41 +
    3.42 +lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
    3.43 +  by (simp add: expand_cfun_eq strictify_conv_if)
    3.44 +
    3.45 +lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
    3.46 +  unfolding sfun_abs_def sfun_rep_def
    3.47 +  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    3.48 +  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
    3.49 +  apply (simp add: expand_cfun_eq strictify_conv_if)
    3.50 +  apply (simp add: Rep_sfun [simplified])
    3.51 +  done
    3.52 +
    3.53 +lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
    3.54 +  unfolding sfun_abs_def sfun_rep_def
    3.55 +  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    3.56 +  apply (simp add: Abs_sfun_inverse)
    3.57 +  done
    3.58 +
    3.59 +lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
    3.60 +apply default
    3.61 +apply (rule sfun_abs_sfun_rep)
    3.62 +apply (simp add: expand_cfun_below strictify_conv_if)
    3.63 +done
    3.64 +
    3.65 +interpretation sfun: ep_pair sfun_rep sfun_abs
    3.66 +  by (rule ep_pair_sfun)
    3.67 +
    3.68 +subsection {* Map functional for strict function space *}
    3.69 +
    3.70 +definition
    3.71 +  sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
    3.72 +where
    3.73 +  "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
    3.74 +
    3.75 +lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
    3.76 +  unfolding sfun_map_def
    3.77 +  by (simp add: cfun_map_ID expand_cfun_eq)
    3.78 +
    3.79 +lemma sfun_map_map:
    3.80 +  assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
    3.81 +  "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    3.82 +    sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    3.83 +unfolding sfun_map_def
    3.84 +by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map)
    3.85 +
    3.86 +lemma ep_pair_sfun_map:
    3.87 +  assumes 1: "ep_pair e1 p1"
    3.88 +  assumes 2: "ep_pair e2 p2"
    3.89 +  shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)"
    3.90 +proof
    3.91 +  interpret e1p1: pcpo_ep_pair e1 p1
    3.92 +    unfolding pcpo_ep_pair_def by fact
    3.93 +  interpret e2p2: pcpo_ep_pair e2 p2
    3.94 +    unfolding pcpo_ep_pair_def by fact
    3.95 +  fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    3.96 +    unfolding sfun_map_def
    3.97 +    apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel)
    3.98 +    apply (rule ep_pair.e_inverse)
    3.99 +    apply (rule ep_pair_cfun_map [OF 1 2])
   3.100 +    done
   3.101 +  fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
   3.102 +    unfolding sfun_map_def
   3.103 +    apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel)
   3.104 +    apply (rule ep_pair.e_p_below)
   3.105 +    apply (rule ep_pair_cfun_map [OF 1 2])
   3.106 +    done
   3.107 +qed
   3.108 +
   3.109 +lemma deflation_sfun_map:
   3.110 +  assumes 1: "deflation d1"
   3.111 +  assumes 2: "deflation d2"
   3.112 +  shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
   3.113 +apply (simp add: sfun_map_def)
   3.114 +apply (rule deflation.intro)
   3.115 +apply simp
   3.116 +apply (subst strictify_cancel)
   3.117 +apply (simp add: cfun_map_def deflation_strict 1 2)
   3.118 +apply (simp add: cfun_map_def deflation.idem 1 2)
   3.119 +apply (simp add: sfun.e_below_iff [symmetric])
   3.120 +apply (subst strictify_cancel)
   3.121 +apply (simp add: cfun_map_def deflation_strict 1 2)
   3.122 +apply (rule deflation.below)
   3.123 +apply (rule deflation_cfun_map [OF 1 2])
   3.124 +done
   3.125 +
   3.126 +lemma finite_deflation_sfun_map:
   3.127 +  assumes 1: "finite_deflation d1"
   3.128 +  assumes 2: "finite_deflation d2"
   3.129 +  shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
   3.130 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
   3.131 +  interpret d1: finite_deflation d1 by fact
   3.132 +  interpret d2: finite_deflation d2 by fact
   3.133 +  have "deflation d1" and "deflation d2" by fact+
   3.134 +  thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
   3.135 +  from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   3.136 +    by (rule finite_deflation_cfun_map)
   3.137 +  then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   3.138 +    by (rule finite_deflation.finite_fixes)
   3.139 +  moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
   3.140 +    by (rule inj_onI, simp)
   3.141 +  ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
   3.142 +    by (rule finite_vimageI)
   3.143 +  then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   3.144 +    unfolding sfun_map_def sfun.e_eq_iff [symmetric]
   3.145 +    by (simp add: strictify_cancel
   3.146 +         deflation_strict `deflation d1` `deflation d2`)
   3.147 +qed
   3.148 +
   3.149 +subsection {* Strict function space is bifinite *}
   3.150 +
   3.151 +instantiation sfun :: (bifinite, bifinite) bifinite
   3.152 +begin
   3.153 +
   3.154 +definition
   3.155 +  "approx = (\<lambda>i. sfun_map\<cdot>(approx i)\<cdot>(approx i))"
   3.156 +
   3.157 +instance proof
   3.158 +  show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b))"
   3.159 +    unfolding approx_sfun_def by simp
   3.160 +next
   3.161 +  fix x :: "'a \<rightarrow>! 'b"
   3.162 +  show "(\<Squnion>i. approx i\<cdot>x) = x"
   3.163 +    unfolding approx_sfun_def
   3.164 +    by (simp add: lub_distribs sfun_map_ID [unfolded ID_def])
   3.165 +next
   3.166 +  fix i :: nat and x :: "'a \<rightarrow>! 'b"
   3.167 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   3.168 +    unfolding approx_sfun_def
   3.169 +    by (intro deflation.idem deflation_sfun_map deflation_approx)
   3.170 +next
   3.171 +  fix i :: nat
   3.172 +  show "finite {x::'a \<rightarrow>! 'b. approx i\<cdot>x = x}"
   3.173 +    unfolding approx_sfun_def
   3.174 +    by (intro finite_deflation.finite_fixes
   3.175 +              finite_deflation_sfun_map
   3.176 +              finite_deflation_approx)
   3.177 +qed
   3.178 +
   3.179 +end
   3.180 +
   3.181 +subsection {* Strict function space is representable *}
   3.182 +
   3.183 +instantiation sfun :: (rep, rep) rep
   3.184 +begin
   3.185 +
   3.186 +definition
   3.187 +  "emb = udom_emb oo sfun_map\<cdot>prj\<cdot>emb"
   3.188 +
   3.189 +definition
   3.190 +  "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj"
   3.191 +
   3.192 +instance
   3.193 +apply (default, unfold emb_sfun_def prj_sfun_def)
   3.194 +apply (rule ep_pair_comp)
   3.195 +apply (rule ep_pair_sfun_map)
   3.196 +apply (rule ep_pair_emb_prj)
   3.197 +apply (rule ep_pair_emb_prj)
   3.198 +apply (rule ep_pair_udom)
   3.199 +done
   3.200 +
   3.201 +end
   3.202 +
   3.203 +text {*
   3.204 +  A deflation constructor lets us configure the domain package to work
   3.205 +  with the strict function space type constructor.
   3.206 +*}
   3.207 +
   3.208 +definition
   3.209 +  sfun_defl :: "TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep"
   3.210 +where
   3.211 +  "sfun_defl = TypeRep_fun2 sfun_map"
   3.212 +
   3.213 +lemma cast_sfun_defl:
   3.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"
   3.215 +unfolding sfun_defl_def
   3.216 +apply (rule cast_TypeRep_fun2)
   3.217 +apply (erule (1) finite_deflation_sfun_map)
   3.218 +done
   3.219 +
   3.220 +lemma REP_sfun: "REP('a::rep \<rightarrow>! 'b::rep) = sfun_defl\<cdot>REP('a)\<cdot>REP('b)"
   3.221 +apply (rule cast_eq_imp_eq, rule ext_cfun)
   3.222 +apply (simp add: cast_REP cast_sfun_defl)
   3.223 +apply (simp only: prj_sfun_def emb_sfun_def)
   3.224 +apply (simp add: sfun_map_def cfun_map_def strictify_cancel)
   3.225 +done
   3.226 +
   3.227 +lemma isodefl_sfun:
   3.228 +  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   3.229 +    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
   3.230 +apply (rule isodeflI)
   3.231 +apply (simp add: cast_sfun_defl cast_isodefl)
   3.232 +apply (simp add: emb_sfun_def prj_sfun_def)
   3.233 +apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
   3.234 +done
   3.235 +
   3.236 +setup {*
   3.237 +  Domain_Isomorphism.add_type_constructor
   3.238 +    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map},
   3.239 +        @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID})
   3.240 +*}
   3.241 +
   3.242 +end