src/HOLCF/ex/Strict_Fun.thy
author wenzelm
Tue Mar 02 23:59:54 2010 +0100 (2010-03-02)
changeset 35427 ad039d29e01c
parent 35167 eba22d68a0a7
child 35547 991a6af75978
permissions -rw-r--r--
proper (type_)notation;
     1 (*  Title:      HOLCF/ex/Strict_Fun.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* The Strict Function Type *}
     6 
     7 theory Strict_Fun
     8 imports HOLCF
     9 begin
    10 
    11 pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
    12   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    13 by simp_all
    14 
    15 type_notation (xsymbols)
    16   sfun  (infixr "\<rightarrow>!" 0)
    17 
    18 text {* TODO: Define nice syntax for abstraction, application. *}
    19 
    20 definition
    21   sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
    22 where
    23   "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
    24 
    25 definition
    26   sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
    27 where
    28   "sfun_rep = (\<Lambda> f. Rep_sfun f)"
    29 
    30 lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
    31   unfolding sfun_rep_def by (simp add: cont_Rep_sfun)
    32 
    33 lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
    34   unfolding sfun_rep_beta by (rule Rep_sfun_strict)
    35 
    36 lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
    37   unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
    38 
    39 lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
    40   by (simp add: expand_cfun_eq strictify_conv_if)
    41 
    42 lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
    43   unfolding sfun_abs_def sfun_rep_def
    44   apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    45   apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
    46   apply (simp add: expand_cfun_eq strictify_conv_if)
    47   apply (simp add: Rep_sfun [simplified])
    48   done
    49 
    50 lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
    51   unfolding sfun_abs_def sfun_rep_def
    52   apply (simp add: cont_Abs_sfun cont_Rep_sfun)
    53   apply (simp add: Abs_sfun_inverse)
    54   done
    55 
    56 lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
    57 apply default
    58 apply (rule sfun_abs_sfun_rep)
    59 apply (simp add: expand_cfun_below strictify_conv_if)
    60 done
    61 
    62 interpretation sfun: ep_pair sfun_rep sfun_abs
    63   by (rule ep_pair_sfun)
    64 
    65 subsection {* Map functional for strict function space *}
    66 
    67 definition
    68   sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
    69 where
    70   "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
    71 
    72 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
    73   unfolding sfun_map_def
    74   by (simp add: cfun_map_ID expand_cfun_eq)
    75 
    76 lemma sfun_map_map:
    77   assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
    78   "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    79     sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    80 unfolding sfun_map_def
    81 by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map)
    82 
    83 lemma ep_pair_sfun_map:
    84   assumes 1: "ep_pair e1 p1"
    85   assumes 2: "ep_pair e2 p2"
    86   shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)"
    87 proof
    88   interpret e1p1: pcpo_ep_pair e1 p1
    89     unfolding pcpo_ep_pair_def by fact
    90   interpret e2p2: pcpo_ep_pair e2 p2
    91     unfolding pcpo_ep_pair_def by fact
    92   fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    93     unfolding sfun_map_def
    94     apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel)
    95     apply (rule ep_pair.e_inverse)
    96     apply (rule ep_pair_cfun_map [OF 1 2])
    97     done
    98   fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
    99     unfolding sfun_map_def
   100     apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel)
   101     apply (rule ep_pair.e_p_below)
   102     apply (rule ep_pair_cfun_map [OF 1 2])
   103     done
   104 qed
   105 
   106 lemma deflation_sfun_map:
   107   assumes 1: "deflation d1"
   108   assumes 2: "deflation d2"
   109   shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
   110 apply (simp add: sfun_map_def)
   111 apply (rule deflation.intro)
   112 apply simp
   113 apply (subst strictify_cancel)
   114 apply (simp add: cfun_map_def deflation_strict 1 2)
   115 apply (simp add: cfun_map_def deflation.idem 1 2)
   116 apply (simp add: sfun.e_below_iff [symmetric])
   117 apply (subst strictify_cancel)
   118 apply (simp add: cfun_map_def deflation_strict 1 2)
   119 apply (rule deflation.below)
   120 apply (rule deflation_cfun_map [OF 1 2])
   121 done
   122 
   123 lemma finite_deflation_sfun_map:
   124   assumes 1: "finite_deflation d1"
   125   assumes 2: "finite_deflation d2"
   126   shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
   127 proof (intro finite_deflation.intro finite_deflation_axioms.intro)
   128   interpret d1: finite_deflation d1 by fact
   129   interpret d2: finite_deflation d2 by fact
   130   have "deflation d1" and "deflation d2" by fact+
   131   thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
   132   from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   133     by (rule finite_deflation_cfun_map)
   134   then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   135     by (rule finite_deflation.finite_fixes)
   136   moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
   137     by (rule inj_onI, simp)
   138   ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
   139     by (rule finite_vimageI)
   140   then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   141     unfolding sfun_map_def sfun.e_eq_iff [symmetric]
   142     by (simp add: strictify_cancel
   143          deflation_strict `deflation d1` `deflation d2`)
   144 qed
   145 
   146 subsection {* Strict function space is bifinite *}
   147 
   148 instantiation sfun :: (bifinite, bifinite) bifinite
   149 begin
   150 
   151 definition
   152   "approx = (\<lambda>i. sfun_map\<cdot>(approx i)\<cdot>(approx i))"
   153 
   154 instance proof
   155   show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b))"
   156     unfolding approx_sfun_def by simp
   157 next
   158   fix x :: "'a \<rightarrow>! 'b"
   159   show "(\<Squnion>i. approx i\<cdot>x) = x"
   160     unfolding approx_sfun_def
   161     by (simp add: lub_distribs sfun_map_ID [unfolded ID_def])
   162 next
   163   fix i :: nat and x :: "'a \<rightarrow>! 'b"
   164   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   165     unfolding approx_sfun_def
   166     by (intro deflation.idem deflation_sfun_map deflation_approx)
   167 next
   168   fix i :: nat
   169   show "finite {x::'a \<rightarrow>! 'b. approx i\<cdot>x = x}"
   170     unfolding approx_sfun_def
   171     by (intro finite_deflation.finite_fixes
   172               finite_deflation_sfun_map
   173               finite_deflation_approx)
   174 qed
   175 
   176 end
   177 
   178 subsection {* Strict function space is representable *}
   179 
   180 instantiation sfun :: (rep, rep) rep
   181 begin
   182 
   183 definition
   184   "emb = udom_emb oo sfun_map\<cdot>prj\<cdot>emb"
   185 
   186 definition
   187   "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj"
   188 
   189 instance
   190 apply (default, unfold emb_sfun_def prj_sfun_def)
   191 apply (rule ep_pair_comp)
   192 apply (rule ep_pair_sfun_map)
   193 apply (rule ep_pair_emb_prj)
   194 apply (rule ep_pair_emb_prj)
   195 apply (rule ep_pair_udom)
   196 done
   197 
   198 end
   199 
   200 text {*
   201   A deflation constructor lets us configure the domain package to work
   202   with the strict function space type constructor.
   203 *}
   204 
   205 definition
   206   sfun_defl :: "TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep"
   207 where
   208   "sfun_defl = TypeRep_fun2 sfun_map"
   209 
   210 lemma cast_sfun_defl:
   211   "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) = udom_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
   212 unfolding sfun_defl_def
   213 apply (rule cast_TypeRep_fun2)
   214 apply (erule (1) finite_deflation_sfun_map)
   215 done
   216 
   217 lemma REP_sfun: "REP('a::rep \<rightarrow>! 'b::rep) = sfun_defl\<cdot>REP('a)\<cdot>REP('b)"
   218 apply (rule cast_eq_imp_eq, rule ext_cfun)
   219 apply (simp add: cast_REP cast_sfun_defl)
   220 apply (simp only: prj_sfun_def emb_sfun_def)
   221 apply (simp add: sfun_map_def cfun_map_def strictify_cancel)
   222 done
   223 
   224 lemma isodefl_sfun:
   225   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   226     isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
   227 apply (rule isodeflI)
   228 apply (simp add: cast_sfun_defl cast_isodefl)
   229 apply (simp add: emb_sfun_def prj_sfun_def)
   230 apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
   231 done
   232 
   233 setup {*
   234   Domain_Isomorphism.add_type_constructor
   235     (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map},
   236         @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID})
   237 *}
   238 
   239 end