src/HOLCF/Representable.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 40002 c5b5f7a3a3b1
child 40037 81e6b89d8f58
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
huffman@33589
     1
(*  Title:      HOLCF/Representable.thy
huffman@33589
     2
    Author:     Brian Huffman
huffman@33589
     3
*)
huffman@33589
     4
huffman@33588
     5
header {* Representable Types *}
huffman@33588
     6
huffman@33588
     7
theory Representable
huffman@39987
     8
imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
huffman@33794
     9
uses
huffman@33794
    10
  ("Tools/repdef.ML")
huffman@33794
    11
  ("Tools/Domain/domain_isomorphism.ML")
huffman@33588
    12
begin
huffman@33588
    13
huffman@39986
    14
default_sort bifinite
huffman@33588
    15
huffman@33588
    16
subsection {* Representations of types *}
huffman@33588
    17
huffman@39989
    18
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
huffman@39989
    19
by (simp add: cast_DEFL)
huffman@33588
    20
huffman@39989
    21
lemma in_DEFL_iff:
huffman@39989
    22
  "x ::: DEFL('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
huffman@39989
    23
by (simp add: in_defl_def cast_DEFL)
huffman@33588
    24
huffman@33588
    25
lemma prj_inverse:
huffman@39989
    26
  "x ::: DEFL('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
huffman@39989
    27
by (simp only: in_DEFL_iff)
huffman@33588
    28
huffman@39989
    29
lemma emb_in_DEFL [simp]:
huffman@39989
    30
  "emb\<cdot>(x::'a) ::: DEFL('a)"
huffman@39989
    31
by (simp add: in_DEFL_iff)
huffman@33588
    32
huffman@33588
    33
subsection {* Coerce operator *}
huffman@33588
    34
huffman@33588
    35
definition coerce :: "'a \<rightarrow> 'b"
huffman@33588
    36
where "coerce = prj oo emb"
huffman@33588
    37
huffman@33588
    38
lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)"
huffman@33588
    39
by (simp add: coerce_def)
huffman@33588
    40
huffman@33588
    41
lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x"
huffman@33588
    42
by (simp add: coerce_def)
huffman@33588
    43
huffman@33588
    44
lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>"
huffman@33588
    45
by (simp add: coerce_def)
huffman@33588
    46
huffman@33588
    47
lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
huffman@40002
    48
by (rule cfun_eqI, simp add: beta_coerce)
huffman@33588
    49
huffman@33588
    50
lemma emb_coerce:
huffman@39989
    51
  "DEFL('a) \<sqsubseteq> DEFL('b)
huffman@33588
    52
   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
huffman@33588
    53
 apply (simp add: beta_coerce)
huffman@33588
    54
 apply (rule prj_inverse)
huffman@39989
    55
 apply (erule defl_belowD)
huffman@39989
    56
 apply (rule emb_in_DEFL)
huffman@33588
    57
done
huffman@33588
    58
huffman@33588
    59
lemma coerce_prj:
huffman@39989
    60
  "DEFL('a) \<sqsubseteq> DEFL('b)
huffman@33588
    61
   \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
huffman@33588
    62
 apply (simp add: coerce_def)
huffman@33588
    63
 apply (rule emb_eq_iff [THEN iffD1])
huffman@33588
    64
 apply (simp only: emb_prj)
huffman@33588
    65
 apply (rule deflation_below_comp1)
huffman@33588
    66
   apply (rule deflation_cast)
huffman@33588
    67
  apply (rule deflation_cast)
huffman@33588
    68
 apply (erule monofun_cfun_arg)
huffman@33588
    69
done
huffman@33588
    70
huffman@33588
    71
lemma coerce_coerce [simp]:
huffman@39989
    72
  "DEFL('a) \<sqsubseteq> DEFL('b)
huffman@33588
    73
   \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
huffman@39989
    74
by (simp add: beta_coerce prj_inverse defl_belowD)
huffman@33588
    75
huffman@33588
    76
lemma coerce_inverse:
huffman@39989
    77
  "emb\<cdot>(x::'a) ::: DEFL('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
huffman@33588
    78
by (simp only: beta_coerce prj_inverse emb_inverse)
huffman@33588
    79
huffman@33588
    80
lemma coerce_type:
huffman@39989
    81
  "DEFL('a) \<sqsubseteq> DEFL('b)
huffman@39989
    82
   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: DEFL('a)"
huffman@39989
    83
by (simp add: beta_coerce prj_inverse defl_belowD)
huffman@33588
    84
huffman@33588
    85
lemma ep_pair_coerce:
huffman@39989
    86
  "DEFL('a) \<sqsubseteq> DEFL('b)
huffman@33588
    87
   \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
huffman@33588
    88
 apply (rule ep_pair.intro)
huffman@33588
    89
  apply simp
huffman@33588
    90
 apply (simp only: beta_coerce)
huffman@33588
    91
 apply (rule below_trans)
huffman@33588
    92
  apply (rule monofun_cfun_arg)
huffman@33588
    93
  apply (rule emb_prj_below)
huffman@33588
    94
 apply simp
huffman@33588
    95
done
huffman@33588
    96
huffman@33779
    97
text {* Isomorphism lemmas used internally by the domain package: *}
huffman@33779
    98
huffman@33779
    99
lemma domain_abs_iso:
huffman@33779
   100
  fixes abs and rep
huffman@39989
   101
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@33779
   102
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
huffman@33779
   103
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
huffman@33779
   104
  shows "rep\<cdot>(abs\<cdot>x) = x"
huffman@39989
   105
unfolding abs_def rep_def by (simp add: DEFL)
huffman@33779
   106
huffman@33779
   107
lemma domain_rep_iso:
huffman@33779
   108
  fixes abs and rep
huffman@39989
   109
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@33779
   110
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
huffman@33779
   111
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
huffman@33779
   112
  shows "abs\<cdot>(rep\<cdot>x) = x"
huffman@39989
   113
unfolding abs_def rep_def by (simp add: DEFL [symmetric])
huffman@33779
   114
huffman@33779
   115
huffman@33588
   116
subsection {* Proving a subtype is representable *}
huffman@33588
   117
huffman@33588
   118
text {*
huffman@39974
   119
  Temporarily relax type constraints for @{term emb}, and @{term prj}.
huffman@33588
   120
*}
huffman@33588
   121
huffman@33588
   122
setup {* Sign.add_const_constraint
huffman@39989
   123
  (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) *}
huffman@33588
   124
huffman@33588
   125
setup {* Sign.add_const_constraint
huffman@33588
   126
  (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
huffman@33588
   127
huffman@33588
   128
setup {* Sign.add_const_constraint
huffman@33588
   129
  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *}
huffman@33588
   130
huffman@33588
   131
lemma typedef_rep_class:
huffman@33588
   132
  fixes Rep :: "'a::pcpo \<Rightarrow> udom"
huffman@33588
   133
  fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
huffman@39989
   134
  fixes t :: defl
huffman@33588
   135
  assumes type: "type_definition Rep Abs {x. x ::: t}"
huffman@33588
   136
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@33679
   137
  assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
huffman@33679
   138
  assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
huffman@39989
   139
  assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
huffman@39986
   140
  shows "OFCLASS('a, bifinite_class)"
huffman@33588
   141
proof
huffman@33588
   142
  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
huffman@39989
   143
    by (simp add: adm_in_defl)
huffman@33588
   144
  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
huffman@33588
   145
    unfolding emb
huffman@33588
   146
    apply (rule beta_cfun)
huffman@33588
   147
    apply (rule typedef_cont_Rep [OF type below adm])
huffman@33588
   148
    done
huffman@33588
   149
  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
huffman@33588
   150
    unfolding prj
huffman@33588
   151
    apply (rule beta_cfun)
huffman@33588
   152
    apply (rule typedef_cont_Abs [OF type below adm])
huffman@33588
   153
    apply simp_all
huffman@33588
   154
    done
huffman@39989
   155
  have emb_in_defl: "\<And>x::'a. emb\<cdot>x ::: t"
huffman@33588
   156
    using type_definition.Rep [OF type]
huffman@33588
   157
    by (simp add: emb_beta)
huffman@33588
   158
  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
huffman@33588
   159
    unfolding prj_beta
huffman@39989
   160
    apply (simp add: cast_fixed [OF emb_in_defl])
huffman@33588
   161
    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
huffman@33588
   162
    done
huffman@33588
   163
  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
huffman@33588
   164
    unfolding prj_beta emb_beta
huffman@33588
   165
    by (simp add: type_definition.Abs_inverse [OF type])
huffman@39974
   166
  show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
huffman@39974
   167
    apply default
huffman@39974
   168
    apply (simp add: prj_emb)
huffman@39974
   169
    apply (simp add: emb_prj cast.below)
huffman@33588
   170
    done
huffman@39989
   171
  show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
huffman@40002
   172
    by (rule cfun_eqI, simp add: defl emb_prj)
huffman@33588
   173
qed
huffman@33588
   174
huffman@39989
   175
lemma typedef_DEFL:
huffman@39989
   176
  assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
huffman@39989
   177
  shows "DEFL('a::pcpo) = t"
huffman@39974
   178
unfolding assms ..
huffman@39974
   179
huffman@39974
   180
text {* Restore original typing constraints *}
huffman@39974
   181
huffman@39974
   182
setup {* Sign.add_const_constraint
huffman@39989
   183
  (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) *}
huffman@39974
   184
huffman@39974
   185
setup {* Sign.add_const_constraint
huffman@39986
   186
  (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
huffman@39974
   187
huffman@39974
   188
setup {* Sign.add_const_constraint
huffman@39986
   189
  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
huffman@39974
   190
huffman@39989
   191
lemma adm_mem_Collect_in_defl: "adm (\<lambda>x. x \<in> {x. x ::: A})"
huffman@39989
   192
unfolding mem_Collect_eq by (rule adm_in_defl)
huffman@33679
   193
huffman@33679
   194
use "Tools/repdef.ML"
huffman@33679
   195
huffman@33588
   196
subsection {* Isomorphic deflations *}
huffman@33588
   197
huffman@33588
   198
definition
huffman@39989
   199
  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
huffman@33588
   200
where
huffman@33588
   201
  "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
huffman@33588
   202
huffman@33588
   203
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
huffman@40002
   204
unfolding isodefl_def by (simp add: cfun_eqI)
huffman@33588
   205
huffman@33588
   206
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
huffman@40002
   207
unfolding isodefl_def by (simp add: cfun_eqI)
huffman@33588
   208
huffman@33588
   209
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
huffman@33588
   210
unfolding isodefl_def
huffman@33588
   211
by (drule cfun_fun_cong [where x="\<bottom>"], simp)
huffman@33588
   212
huffman@33588
   213
lemma isodefl_imp_deflation:
huffman@39986
   214
  fixes d :: "'a \<rightarrow> 'a"
huffman@33588
   215
  assumes "isodefl d t" shows "deflation d"
huffman@33588
   216
proof
huffman@39974
   217
  note assms [unfolded isodefl_def, simp]
huffman@33588
   218
  fix x :: 'a
huffman@33588
   219
  show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@33588
   220
    using cast.idem [of t "emb\<cdot>x"] by simp
huffman@33588
   221
  show "d\<cdot>x \<sqsubseteq> x"
huffman@33588
   222
    using cast.below [of t "emb\<cdot>x"] by simp
huffman@33588
   223
qed
huffman@33588
   224
huffman@39989
   225
lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
huffman@39989
   226
unfolding isodefl_def by (simp add: cast_DEFL)
huffman@33588
   227
huffman@39989
   228
lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
huffman@33588
   229
unfolding isodefl_def
huffman@39989
   230
apply (simp add: cast_DEFL)
huffman@40002
   231
apply (simp add: cfun_eq_iff)
huffman@33588
   232
apply (rule allI)
huffman@33588
   233
apply (drule_tac x="emb\<cdot>x" in spec)
huffman@33588
   234
apply simp
huffman@33588
   235
done
huffman@33588
   236
huffman@33588
   237
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
huffman@40002
   238
unfolding isodefl_def by (simp add: cfun_eq_iff)
huffman@33588
   239
huffman@33588
   240
lemma adm_isodefl:
huffman@33588
   241
  "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
huffman@33588
   242
unfolding isodefl_def by simp
huffman@33588
   243
huffman@33588
   244
lemma isodefl_lub:
huffman@33588
   245
  assumes "chain d" and "chain t"
huffman@33588
   246
  assumes "\<And>i. isodefl (d i) (t i)"
huffman@33588
   247
  shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
huffman@33588
   248
using prems unfolding isodefl_def
huffman@33588
   249
by (simp add: contlub_cfun_arg contlub_cfun_fun)
huffman@33588
   250
huffman@33588
   251
lemma isodefl_fix:
huffman@33588
   252
  assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
huffman@33588
   253
  shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
huffman@33588
   254
unfolding fix_def2
huffman@33588
   255
apply (rule isodefl_lub, simp, simp)
huffman@33588
   256
apply (induct_tac i)
huffman@33588
   257
apply (simp add: isodefl_bottom)
huffman@39974
   258
apply (simp add: assms)
huffman@33588
   259
done
huffman@33588
   260
huffman@33588
   261
lemma isodefl_coerce:
huffman@33588
   262
  fixes d :: "'a \<rightarrow> 'a"
huffman@39989
   263
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@33588
   264
  shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
huffman@33588
   265
unfolding isodefl_def
huffman@40002
   266
apply (simp add: cfun_eq_iff)
huffman@39989
   267
apply (simp add: emb_coerce coerce_prj DEFL)
huffman@33588
   268
done
huffman@33588
   269
huffman@33779
   270
lemma isodefl_abs_rep:
huffman@33779
   271
  fixes abs and rep and d
huffman@39989
   272
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@33779
   273
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
huffman@33779
   274
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
huffman@33779
   275
  shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
huffman@39989
   276
unfolding abs_def rep_def using DEFL by (rule isodefl_coerce)
huffman@33779
   277
huffman@33588
   278
lemma isodefl_cfun:
huffman@33588
   279
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   280
    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   281
apply (rule isodeflI)
huffman@39989
   282
apply (simp add: cast_cfun_defl cast_isodefl)
huffman@33588
   283
apply (simp add: emb_cfun_def prj_cfun_def)
huffman@33588
   284
apply (simp add: cfun_map_map cfcomp1)
huffman@33588
   285
done
huffman@33588
   286
huffman@33588
   287
lemma isodefl_ssum:
huffman@33588
   288
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   289
    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   290
apply (rule isodeflI)
huffman@39989
   291
apply (simp add: cast_ssum_defl cast_isodefl)
huffman@33588
   292
apply (simp add: emb_ssum_def prj_ssum_def)
huffman@33588
   293
apply (simp add: ssum_map_map isodefl_strict)
huffman@33588
   294
done
huffman@33588
   295
huffman@33588
   296
lemma isodefl_sprod:
huffman@33588
   297
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   298
    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   299
apply (rule isodeflI)
huffman@39989
   300
apply (simp add: cast_sprod_defl cast_isodefl)
huffman@33588
   301
apply (simp add: emb_sprod_def prj_sprod_def)
huffman@33588
   302
apply (simp add: sprod_map_map isodefl_strict)
huffman@33588
   303
done
huffman@33588
   304
huffman@33786
   305
lemma isodefl_cprod:
huffman@33786
   306
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   307
    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
huffman@33786
   308
apply (rule isodeflI)
huffman@39989
   309
apply (simp add: cast_prod_defl cast_isodefl)
huffman@39974
   310
apply (simp add: emb_prod_def prj_prod_def)
huffman@33786
   311
apply (simp add: cprod_map_map cfcomp1)
huffman@33786
   312
done
huffman@33786
   313
huffman@33588
   314
lemma isodefl_u:
huffman@39989
   315
  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
huffman@33588
   316
apply (rule isodeflI)
huffman@39989
   317
apply (simp add: cast_u_defl cast_isodefl)
huffman@33588
   318
apply (simp add: emb_u_def prj_u_def)
huffman@33588
   319
apply (simp add: u_map_map)
huffman@33588
   320
done
huffman@33588
   321
huffman@33794
   322
subsection {* Constructing Domain Isomorphisms *}
huffman@33794
   323
huffman@33794
   324
use "Tools/Domain/domain_isomorphism.ML"
huffman@33794
   325
huffman@33794
   326
setup {*
huffman@33794
   327
  fold Domain_Isomorphism.add_type_constructor
huffman@39989
   328
    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
huffman@35479
   329
        @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
huffman@33794
   330
huffman@39989
   331
     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
huffman@35479
   332
        @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
huffman@33794
   333
huffman@39989
   334
     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
huffman@35479
   335
        @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
huffman@33794
   336
huffman@39989
   337
     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
huffman@35479
   338
        @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
huffman@33794
   339
huffman@39989
   340
     (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
huffman@35479
   341
        @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
huffman@33794
   342
*}
huffman@33794
   343
huffman@33588
   344
end