author  huffman 
Mon, 20 Dec 2010 09:48:16 0800  
changeset 41323  ae1c227534f5 
parent 41321  4e72b6fc9dd4 
child 41437  5bc117c382ec 
permissions  rwrr 
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  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 
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 