author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 41437 | 5bc117c382ec |
child 58880 | 0baae4311a9f |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Library/List_Predomain.thy |
41112
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" |
41437 | 100 |
where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))" |
41292
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 |
41437 | 125 |
apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl cast_liftdefl) |
41292
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 | 138 |
abbreviation list_map :: "('a::cpo \<rightarrow> 'b::cpo) \<Rightarrow> 'a list \<rightarrow> 'b list" |
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 | 141 |
lemma list_map_ID [domain_map_ID]: "list_map ID = ID" |
41323 | 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 | 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 | 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 | 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 |
41437 | 165 |
apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl) |
41292
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 |