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