src/HOL/HOLCF/Library/List_Predomain.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61169 4de9ff3ea29a
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Library/List_Predomain.thy
huffman@41112
     2
    Author:     Brian Huffman
huffman@41112
     3
*)
huffman@41112
     4
wenzelm@58880
     5
section {* Predomain class instance for HOL list type *}
huffman@41112
     6
huffman@41112
     7
theory List_Predomain
huffman@41292
     8
imports List_Cpo Sum_Cpo
huffman@41112
     9
begin
huffman@41112
    10
huffman@41112
    11
subsection {* Strict list type *}
huffman@41112
    12
huffman@41112
    13
domain 'a slist = SNil | SCons "'a" "'a slist"
huffman@41112
    14
huffman@41292
    15
text {* Polymorphic map function for strict lists. *}
huffman@41292
    16
huffman@41292
    17
text {* FIXME: The domain package should generate this! *}
huffman@41292
    18
huffman@41292
    19
fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
huffman@41292
    20
  where "slist_map'\<cdot>f\<cdot>SNil = SNil"
huffman@41292
    21
  | "\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow>
huffman@41292
    22
      slist_map'\<cdot>f\<cdot>(SCons\<cdot>x\<cdot>xs) = SCons\<cdot>(f\<cdot>x)\<cdot>(slist_map'\<cdot>f\<cdot>xs)"
huffman@41292
    23
huffman@41292
    24
lemma slist_map'_strict [simp]: "slist_map'\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@41292
    25
by fixrec_simp
huffman@41292
    26
huffman@41292
    27
lemma slist_map_conv [simp]: "slist_map = slist_map'"
huffman@41292
    28
apply (rule cfun_eqI, rule cfun_eqI, rename_tac f xs)
huffman@41292
    29
apply (induct_tac xs, simp_all)
huffman@41292
    30
apply (subst slist_map_unfold, simp)
huffman@41292
    31
apply (subst slist_map_unfold, simp add: SNil_def)
huffman@41292
    32
apply (subst slist_map_unfold, simp add: SCons_def)
huffman@41292
    33
done
huffman@41292
    34
huffman@41292
    35
lemma slist_map'_slist_map':
huffman@41292
    36
  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>f\<cdot>(slist_map'\<cdot>g\<cdot>xs) = slist_map'\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
huffman@41292
    37
apply (induct xs, simp, simp)
huffman@41292
    38
apply (case_tac "g\<cdot>a = \<bottom>", simp, simp)
huffman@41292
    39
apply (case_tac "slist_map'\<cdot>g\<cdot>xs = \<bottom>", simp, simp)
huffman@41292
    40
done
huffman@41292
    41
huffman@41292
    42
lemma slist_map'_oo:
huffman@41292
    43
  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_map'\<cdot>(f oo g) = slist_map'\<cdot>f oo slist_map'\<cdot>g"
huffman@41292
    44
by (simp add: cfcomp1 slist_map'_slist_map' eta_cfun)
huffman@41292
    45
huffman@41292
    46
lemma slist_map'_ID: "slist_map'\<cdot>ID = ID"
huffman@41292
    47
by (rule cfun_eqI, induct_tac x, simp_all)
huffman@41292
    48
huffman@41292
    49
lemma ep_pair_slist_map':
huffman@41292
    50
  "ep_pair e p \<Longrightarrow> ep_pair (slist_map'\<cdot>e) (slist_map'\<cdot>p)"
huffman@41292
    51
apply (rule ep_pair.intro)
huffman@41292
    52
apply (subst slist_map'_slist_map')
huffman@41292
    53
apply (erule pcpo_ep_pair.p_strict [unfolded pcpo_ep_pair_def])
huffman@41292
    54
apply (simp add: ep_pair.e_inverse ID_def [symmetric] slist_map'_ID)
huffman@41292
    55
apply (subst slist_map'_slist_map')
huffman@41292
    56
apply (erule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def])
huffman@41292
    57
apply (rule below_eq_trans [OF _ ID1])
huffman@41292
    58
apply (subst slist_map'_ID [symmetric])
huffman@41292
    59
apply (intro monofun_cfun below_refl)
huffman@41292
    60
apply (simp add: cfun_below_iff ep_pair.e_p_below)
huffman@41292
    61
done
huffman@41292
    62
huffman@41112
    63
text {*
huffman@41112
    64
  Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
huffman@41112
    65
*}
huffman@41112
    66
huffman@41112
    67
fixrec encode_list_u where
huffman@41112
    68
  "encode_list_u\<cdot>(up\<cdot>[]) = SNil" |
huffman@41112
    69
  "encode_list_u\<cdot>(up\<cdot>(x # xs)) = SCons\<cdot>(up\<cdot>x)\<cdot>(encode_list_u\<cdot>(up\<cdot>xs))"
huffman@41112
    70
huffman@41112
    71
lemma encode_list_u_strict [simp]: "encode_list_u\<cdot>\<bottom> = \<bottom>"
huffman@41112
    72
by fixrec_simp
huffman@41112
    73
huffman@41112
    74
lemma encode_list_u_bottom_iff [simp]:
huffman@41112
    75
  "encode_list_u\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
huffman@41112
    76
apply (induct x, simp_all)
huffman@41112
    77
apply (rename_tac xs, induct_tac xs, simp_all)
huffman@41112
    78
done
huffman@41112
    79
huffman@41112
    80
fixrec decode_list_u where
huffman@41112
    81
  "decode_list_u\<cdot>SNil = up\<cdot>[]" |
huffman@41112
    82
  "ys \<noteq> \<bottom> \<Longrightarrow> decode_list_u\<cdot>(SCons\<cdot>(up\<cdot>x)\<cdot>ys) =
huffman@41112
    83
    (case decode_list_u\<cdot>ys of up\<cdot>xs \<Rightarrow> up\<cdot>(x # xs))"
huffman@41112
    84
huffman@41112
    85
lemma decode_list_u_strict [simp]: "decode_list_u\<cdot>\<bottom> = \<bottom>"
huffman@41112
    86
by fixrec_simp
huffman@41112
    87
huffman@41112
    88
lemma decode_encode_list_u [simp]: "decode_list_u\<cdot>(encode_list_u\<cdot>x) = x"
huffman@41112
    89
by (induct x, simp, rename_tac xs, induct_tac xs, simp_all)
huffman@41112
    90
huffman@41112
    91
lemma encode_decode_list_u [simp]: "encode_list_u\<cdot>(decode_list_u\<cdot>y) = y"
huffman@41112
    92
apply (induct y, simp, simp)
huffman@41112
    93
apply (case_tac a, simp)
huffman@41112
    94
apply (case_tac "decode_list_u\<cdot>y", simp, simp)
huffman@41112
    95
done
huffman@41112
    96
huffman@41112
    97
subsection {* Lists are a predomain *}
huffman@41112
    98
huffman@41292
    99
definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
huffman@41437
   100
  where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))"
huffman@41292
   101
huffman@41292
   102
lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"
huffman@41292
   103
using isodefl_slist [where fa="cast\<cdot>a" and da="a"]
huffman@41292
   104
unfolding isodefl_def by simp
huffman@41292
   105
huffman@41112
   106
instantiation list :: (predomain) predomain
huffman@41112
   107
begin
huffman@41112
   108
huffman@41112
   109
definition
huffman@41292
   110
  "liftemb = (strictify\<cdot>up oo emb oo slist_map'\<cdot>u_emb) oo slist_map'\<cdot>liftemb oo encode_list_u"
huffman@41112
   111
huffman@41112
   112
definition
huffman@41292
   113
  "liftprj = (decode_list_u oo slist_map'\<cdot>liftprj) oo (slist_map'\<cdot>u_prj oo prj) oo fup\<cdot>ID"
huffman@41112
   114
huffman@41112
   115
definition
huffman@41292
   116
  "liftdefl (t::('a list) itself) = list_liftdefl\<cdot>LIFTDEFL('a)"
huffman@41112
   117
huffman@41112
   118
instance proof
huffman@41292
   119
  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a list) u)"
huffman@41112
   120
    unfolding liftemb_list_def liftprj_list_def
huffman@41292
   121
    by (intro ep_pair_comp ep_pair_slist_map' ep_pair_strictify_up
huffman@41292
   122
      ep_pair_emb_prj predomain_ep ep_pair_u, simp add: ep_pair.intro)
huffman@41292
   123
  show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom u \<rightarrow> ('a list) u)"
huffman@41112
   124
    unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
huffman@41437
   125
    apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl cast_liftdefl)
huffman@41292
   126
    apply (simp add: slist_map'_oo u_emb_bottom cfun_eq_iff)
huffman@41292
   127
    done
huffman@41112
   128
qed
huffman@41112
   129
huffman@41112
   130
end
huffman@41112
   131
huffman@41321
   132
subsection {* Configuring domain package to work with list type *}
huffman@41321
   133
huffman@41112
   134
lemma liftdefl_list [domain_defl_simps]:
huffman@41292
   135
  "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
huffman@41292
   136
by (rule liftdefl_list_def)
huffman@41112
   137
huffman@41320
   138
abbreviation list_map :: "('a::cpo \<rightarrow> 'b::cpo) \<Rightarrow> 'a list \<rightarrow> 'b list"
huffman@41320
   139
  where "list_map f \<equiv> Abs_cfun (map (Rep_cfun f))"
huffman@41112
   140
huffman@41320
   141
lemma list_map_ID [domain_map_ID]: "list_map ID = ID"
huffman@41323
   142
by (simp add: ID_def)
huffman@41112
   143
huffman@41112
   144
lemma deflation_list_map [domain_deflation]:
huffman@41320
   145
  "deflation d \<Longrightarrow> deflation (list_map d)"
huffman@41112
   146
apply default
huffman@41112
   147
apply (induct_tac x, simp_all add: deflation.idem)
huffman@41112
   148
apply (induct_tac x, simp_all add: deflation.below)
huffman@41112
   149
done
huffman@41112
   150
huffman@41112
   151
lemma encode_list_u_map:
huffman@41320
   152
  "encode_list_u\<cdot>(u_map\<cdot>(list_map f)\<cdot>(decode_list_u\<cdot>xs))
huffman@41112
   153
    = slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
huffman@41292
   154
apply (induct xs, simp, simp)
huffman@41112
   155
apply (case_tac a, simp, rename_tac b)
huffman@41112
   156
apply (case_tac "decode_list_u\<cdot>xs")
huffman@41292
   157
apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp, simp)
huffman@41292
   158
done
huffman@41112
   159
huffman@41112
   160
lemma isodefl_list_u [domain_isodefl]:
huffman@41112
   161
  fixes d :: "'a::predomain \<rightarrow> 'a"
huffman@41292
   162
  assumes "isodefl' d t"
huffman@41320
   163
  shows "isodefl' (list_map d) (list_liftdefl\<cdot>t)"
huffman@41292
   164
using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
huffman@41437
   165
apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl)
huffman@41292
   166
apply (simp add: cfcomp1 encode_list_u_map)
huffman@41292
   167
apply (simp add: slist_map'_slist_map' u_emb_bottom)
huffman@41292
   168
done
huffman@41112
   169
huffman@41112
   170
setup {*
huffman@41112
   171
  Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
huffman@41112
   172
*}
huffman@41112
   173
huffman@41112
   174
end