author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16208  cfe047ad6384 
permissions  rwrr 
16058  1 
(* Title: HOLCF/TypedefPcpo.thy 
2 
ID: $Id$ 

3 
Author: Brian Huffman 

4 
*) 

5 

6 
header {* Subtypes of pcpos *} 

7 

8 
theory TypedefPcpo 

9 
imports Adm 

10 
begin 

11 

12 
subsection {* Proving a subtype is a partial order *} 

13 

14 
text {* 

15 
A subtype of a partial order is itself a partial order, 

16 
if the ordering is defined in the standard way. 

17 
*} 

18 

19 
theorem typedef_po: 

20 
fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord" 

21 
assumes type: "type_definition Rep Abs A" 

22 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

23 
shows "OFCLASS('b, po_class)" 

24 
apply (intro_classes, unfold less) 

25 
apply (rule refl_less) 

26 
apply (subst type_definition.Rep_inject [OF type, symmetric]) 

27 
apply (rule antisym_less, assumption+) 

28 
apply (rule trans_less, assumption+) 

29 
done 

30 

31 

32 
subsection {* Proving a subtype is complete *} 

33 

34 
text {* 

35 
A subtype of a cpo is itself a cpo if the ordering is 

36 
defined in the standard way, and the defining subset 

37 
is closed with respect to limits of chains. A set is 

38 
closed if and only if membership in the set is an 

39 
admissible predicate. 

40 
*} 

41 

42 
lemma chain_Rep: 

43 
assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

44 
shows "chain S \<Longrightarrow> chain (\<lambda>n. Rep (S n))" 

45 
by (rule chainI, drule chainE, unfold less) 

46 

47 
lemma lub_Rep_in_A: 

48 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 

49 
assumes type: "type_definition Rep Abs A" 

50 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

51 
and adm: "adm (\<lambda>x. x \<in> A)" 

52 
shows "chain S \<Longrightarrow> (LUB n. Rep (S n)) \<in> A" 

53 
apply (erule admD [OF adm chain_Rep [OF less], rule_format]) 

54 
apply (rule type_definition.Rep [OF type]) 

55 
done 

56 

57 
theorem typedef_is_lub: 

58 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 

59 
assumes type: "type_definition Rep Abs A" 

60 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

61 
and adm: "adm (\<lambda>x. x \<in> A)" 

62 
shows "chain S \<Longrightarrow> range S << Abs (LUB n. Rep (S n))" 

63 
apply (rule is_lubI) 

64 
apply (rule ub_rangeI) 

65 
apply (subst less) 

66 
apply (subst type_definition.Abs_inverse [OF type]) 

67 
apply (erule lub_Rep_in_A [OF type less adm]) 

68 
apply (rule is_ub_thelub) 

69 
apply (erule chain_Rep [OF less]) 

70 
apply (subst less) 

71 
apply (subst type_definition.Abs_inverse [OF type]) 

72 
apply (erule lub_Rep_in_A [OF type less adm]) 

73 
apply (rule is_lub_thelub) 

74 
apply (erule chain_Rep [OF less]) 

75 
apply (rule ub_rangeI) 

76 
apply (drule ub_rangeD) 

77 
apply (unfold less) 

78 
apply assumption 

79 
done 

80 

81 
theorem typedef_cpo: 

82 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" 

83 
assumes type: "type_definition Rep Abs A" 

84 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

85 
and adm: "adm (\<lambda>x. x \<in> A)" 

86 
shows "OFCLASS('b, cpo_class)" 

87 
apply (intro_classes) 

88 
apply (rule_tac x="Abs (LUB n. Rep (S n))" in exI) 

89 
apply (erule typedef_is_lub [OF type less adm]) 

90 
done 

91 

92 

93 
subsubsection {* Continuity of @{term Rep} and @{term Abs} *} 

94 

95 
text {* For any subcpo, the @{term Rep} function is continuous. *} 

96 

97 
theorem typedef_cont_Rep: 

98 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 

99 
assumes type: "type_definition Rep Abs A" 

100 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

101 
and adm: "adm (\<lambda>x. x \<in> A)" 

102 
shows "cont Rep" 

16208
cfe047ad6384
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents:
16080
diff
changeset

103 
apply (rule contI) 
16058  104 
apply (simp only: typedef_is_lub [OF type less adm, THEN thelubI]) 
105 
apply (subst type_definition.Abs_inverse [OF type]) 

106 
apply (erule lub_Rep_in_A [OF type less adm]) 

107 
apply (rule thelubE [OF _ refl]) 

108 
apply (erule chain_Rep [OF less]) 

109 
done 

110 

111 
text {* 

112 
For a subcpo, we can make the @{term Abs} function continuous 

113 
only if we restrict its domain to the defining subset by 

114 
composing it with another continuous function. 

115 
*} 

116 

117 
theorem typedef_cont_Abs: 

118 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 

119 
fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" 

120 
assumes type: "type_definition Rep Abs A" 

121 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

122 
and adm: "adm (\<lambda>x. x \<in> A)" 

123 
and f_in_A: "\<And>x. f x \<in> A" 

124 
and cont_f: "cont f" 

125 
shows "cont (\<lambda>x. Abs (f x))" 

16208
cfe047ad6384
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents:
16080
diff
changeset

126 
apply (rule contI) 
16058  127 
apply (rule is_lubI) 
128 
apply (rule ub_rangeI) 

129 
apply (simp only: less type_definition.Abs_inverse [OF type f_in_A]) 

130 
apply (rule monofun_fun_arg [OF cont2mono [OF cont_f]]) 

131 
apply (erule is_ub_thelub) 

132 
apply (simp only: less type_definition.Abs_inverse [OF type f_in_A]) 

16208
cfe047ad6384
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents:
16080
diff
changeset

133 
apply (simp only: contlubE [OF cont2contlub [OF cont_f]]) 
16058  134 
apply (rule is_lub_thelub) 
135 
apply (erule ch2ch_monofun [OF cont2mono [OF cont_f]]) 

136 
apply (rule ub_rangeI) 

137 
apply (drule_tac i=i in ub_rangeD) 

138 
apply (simp only: less type_definition.Abs_inverse [OF type f_in_A]) 

139 
done 

140 

141 

142 
subsection {* Proving a typedef is pointed *} 

143 

144 
text {* 

145 
A subtype of a cpo has a least element if and only if 

146 
the defining subset has a least element. 

147 
*} 

148 

149 
theorem typedef_pcpo: 

150 
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" 

151 
assumes type: "type_definition Rep Abs A" 

152 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

153 
and z_in_A: "z \<in> A" 

154 
and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x" 

155 
shows "OFCLASS('b, pcpo_class)" 

156 
apply (intro_classes) 

157 
apply (rule_tac x="Abs z" in exI, rule allI) 

158 
apply (unfold less) 

159 
apply (subst type_definition.Abs_inverse [OF type z_in_A]) 

160 
apply (rule z_least [OF type_definition.Rep [OF type]]) 

161 
done 

162 

163 
text {* 

164 
As a special case, a subtype of a pcpo has a least element 

165 
if the defining subset contains @{term \<bottom>}. 

166 
*} 

167 

168 
theorem typedef_pcpo_UU: 

169 
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" 

170 
assumes type: "type_definition Rep Abs A" 

171 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

172 
and UU_in_A: "\<bottom> \<in> A" 

173 
shows "OFCLASS('b, pcpo_class)" 

174 
by (rule typedef_pcpo [OF type less UU_in_A], rule minimal) 

175 

176 

177 
subsubsection {* Strictness of @{term Rep} and @{term Abs} *} 

178 

179 
text {* 

180 
For a subpcpo where @{term \<bottom>} is a member of the defining 

181 
subset, @{term Rep} and @{term Abs} are both strict. 

182 
*} 

183 

16208
cfe047ad6384
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents:
16080
diff
changeset

184 
theorem typedef_Abs_strict: 
16058  185 
assumes type: "type_definition Rep Abs A" 
186 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

187 
and UU_in_A: "\<bottom> \<in> A" 

188 
shows "Abs \<bottom> = \<bottom>" 

189 
apply (rule UU_I, unfold less) 

190 
apply (simp add: type_definition.Abs_inverse [OF type UU_in_A]) 

191 
done 

192 

16208
cfe047ad6384
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents:
16080
diff
changeset

193 
theorem typedef_Rep_strict: 
16058  194 
assumes type: "type_definition Rep Abs A" 
195 
and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" 

196 
and UU_in_A: "\<bottom> \<in> A" 

197 
shows "Rep \<bottom> = \<bottom>" 

16208
cfe047ad6384
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents:
16080
diff
changeset

198 
apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst]) 
16058  199 
apply (rule type_definition.Abs_inverse [OF type UU_in_A]) 
200 
done 

201 

202 
end 