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