author  krauss 
Fri, 29 Oct 2010 21:41:14 +0200  
changeset 40288  520199d8b66e 
parent 40252  029400b6c893 
child 42949  618adb3584e5 
permissions  rwrr 
40107  1 
(* Title: HOL/Partial_Function.thy 
2 
Author: Alexander Krauss, TU Muenchen 

3 
*) 

4 

5 
header {* Partial Function Definitions *} 

6 

7 
theory Partial_Function 

8 
imports Complete_Partial_Order Option 

9 
uses 

10 
"Tools/Function/function_lib.ML" 

11 
"Tools/Function/partial_function.ML" 

12 
begin 

13 

14 
setup Partial_Function.setup 

15 

16 
subsection {* Axiomatic setup *} 

17 

18 
text {* This techical locale constains the requirements for function 

19 
definitions with ccpo fixed points. *} 

20 

21 
definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))" 

22 
definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})" 

23 
definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))" 

24 
definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))" 

25 

26 
lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)" 

27 
by (rule monotoneI) (auto simp: fun_ord_def) 

28 

40288  29 
lemma let_mono[partial_function_mono]: 
30 
"(\<And>x. monotone orda ordb (\<lambda>f. b f x)) 

31 
\<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))" 

32 
by (simp add: Let_def) 

33 

40107  34 
lemma if_mono[partial_function_mono]: "monotone orda ordb F 
35 
\<Longrightarrow> monotone orda ordb G 

36 
\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)" 

37 
unfolding monotone_def by simp 

38 

39 
definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)" 

40 

41 
locale partial_function_definitions = 

42 
fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

43 
fixes lub :: "'a set \<Rightarrow> 'a" 

44 
assumes leq_refl: "leq x x" 

45 
assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z" 

46 
assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y" 

47 
assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)" 

48 
assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z" 

49 

50 
lemma partial_function_lift: 

51 
assumes "partial_function_definitions ord lb" 

52 
shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf") 

53 
proof  

54 
interpret partial_function_definitions ord lb by fact 

55 

56 
{ fix A a assume A: "chain ?ordf A" 

57 
have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C") 

58 
proof (rule chainI) 

59 
fix x y assume "x \<in> ?C" "y \<in> ?C" 

60 
then obtain f g where fg: "f \<in> A" "g \<in> A" 

61 
and [simp]: "x = f a" "y = g a" by blast 

62 
from chainD[OF A fg] 

63 
show "ord x y \<or> ord y x" unfolding fun_ord_def by auto 

64 
qed } 

65 
note chain_fun = this 

66 

67 
show ?thesis 

68 
proof 

69 
fix x show "?ordf x x" 

70 
unfolding fun_ord_def by (auto simp: leq_refl) 

71 
next 

72 
fix x y z assume "?ordf x y" "?ordf y z" 

73 
thus "?ordf x z" unfolding fun_ord_def 

74 
by (force dest: leq_trans) 

75 
next 

76 
fix x y assume "?ordf x y" "?ordf y x" 

77 
thus "x = y" unfolding fun_ord_def 

78 
by (force intro!: ext dest: leq_antisym) 

79 
next 

80 
fix A f assume f: "f \<in> A" and A: "chain ?ordf A" 

81 
thus "?ordf f (?lubf A)" 

82 
unfolding fun_lub_def fun_ord_def 

83 
by (blast intro: lub_upper chain_fun[OF A] f) 

84 
next 

85 
fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a" 

86 
assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g" 

87 
show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def 

88 
by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def]) 

89 
qed 

90 
qed 

91 

92 
lemma ccpo: assumes "partial_function_definitions ord lb" 

93 
shows "class.ccpo ord (mk_less ord) lb" 

94 
using assms unfolding partial_function_definitions_def mk_less_def 

95 
by unfold_locales blast+ 

96 

97 
lemma partial_function_image: 

98 
assumes "partial_function_definitions ord Lub" 

99 
assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" 

100 
assumes inv: "\<And>x. f (g x) = x" 

101 
shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)" 

102 
proof  

103 
let ?iord = "img_ord f ord" 

104 
let ?ilub = "img_lub f g Lub" 

105 

106 
interpret partial_function_definitions ord Lub by fact 

107 
show ?thesis 

108 
proof 

109 
fix A x assume "chain ?iord A" "x \<in> A" 

110 
then have "chain ord (f ` A)" "f x \<in> f ` A" 

111 
by (auto simp: img_ord_def intro: chainI dest: chainD) 

112 
thus "?iord x (?ilub A)" 

113 
unfolding inv img_lub_def img_ord_def by (rule lub_upper) 

114 
next 

115 
fix A x assume "chain ?iord A" 

116 
and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x" 

117 
then have "chain ord (f ` A)" 

118 
by (auto simp: img_ord_def intro: chainI dest: chainD) 

119 
thus "?iord (?ilub A) x" 

120 
unfolding inv img_lub_def img_ord_def 

121 
by (rule lub_least) (auto dest: 1[unfolded img_ord_def]) 

122 
qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj) 

123 
qed 

124 

125 
context partial_function_definitions 

126 
begin 

127 

128 
abbreviation "le_fun \<equiv> fun_ord leq" 

129 
abbreviation "lub_fun \<equiv> fun_lub lub" 

130 
abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun" 

131 
abbreviation "mono_body \<equiv> monotone le_fun leq" 

132 

133 
text {* Interpret manually, to avoid flooding everything with facts about 

134 
orders *} 

135 

136 
lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun" 

137 
apply (rule ccpo) 

138 
apply (rule partial_function_lift) 

139 
apply (rule partial_function_definitions_axioms) 

140 
done 

141 

142 
text {* The crucial fixedpoint theorem *} 

143 

144 
lemma mono_body_fixp: 

145 
"(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)" 

146 
by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def) 

147 

148 
text {* Version with curry/uncurry combinators, to be used by package *} 

149 

150 
lemma fixp_rule_uc: 

151 
fixes F :: "'c \<Rightarrow> 'c" and 

152 
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and 

153 
C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" 

154 
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" 

155 
assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" 

156 
assumes inverse: "\<And>f. C (U f) = f" 

157 
shows "f = F f" 

158 
proof  

159 
have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq) 

160 
also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))" 

161 
by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl) 

162 
also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse) 

163 
also have "... = F f" by (simp add: eq) 

164 
finally show "f = F f" . 

165 
qed 

166 

167 
text {* Rules for @{term mono_body}: *} 

168 

169 
lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)" 

170 
by (rule monotoneI) (rule leq_refl) 

171 

172 
declaration {* Partial_Function.init @{term fixp_fun} 

173 
@{term mono_body} @{thm fixp_rule_uc} *} 

174 

175 
end 

176 

177 

178 
subsection {* Flat interpretation: tailrec and option *} 

179 

180 
definition 

181 
"flat_ord b x y \<longleftrightarrow> x = b \<or> x = y" 

182 

183 
definition 

184 
"flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A  {b}))" 

185 

186 
lemma flat_interpretation: 

187 
"partial_function_definitions (flat_ord b) (flat_lub b)" 

188 
proof 

189 
fix A x assume 1: "chain (flat_ord b) A" "x \<in> A" 

190 
show "flat_ord b x (flat_lub b A)" 

191 
proof cases 

192 
assume "x = b" 

193 
thus ?thesis by (simp add: flat_ord_def) 

194 
next 

195 
assume "x \<noteq> b" 

196 
with 1 have "A  {b} = {x}" 

197 
by (auto elim: chainE simp: flat_ord_def) 

198 
then have "flat_lub b A = x" 

199 
by (auto simp: flat_lub_def) 

200 
thus ?thesis by (auto simp: flat_ord_def) 

201 
qed 

202 
next 

203 
fix A z assume A: "chain (flat_ord b) A" 

204 
and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z" 

205 
show "flat_ord b (flat_lub b A) z" 

206 
proof cases 

207 
assume "A \<subseteq> {b}" 

208 
thus ?thesis 

209 
by (auto simp: flat_lub_def flat_ord_def) 

210 
next 

211 
assume nb: "\<not> A \<subseteq> {b}" 

212 
then obtain y where y: "y \<in> A" "y \<noteq> b" by auto 

213 
with A have "A  {b} = {y}" 

214 
by (auto elim: chainE simp: flat_ord_def) 

215 
with nb have "flat_lub b A = y" 

216 
by (auto simp: flat_lub_def) 

217 
with z y show ?thesis by auto 

218 
qed 

219 
qed (auto simp: flat_ord_def) 

220 

221 
interpretation tailrec!: 

222 
partial_function_definitions "flat_ord undefined" "flat_lub undefined" 

223 
by (rule flat_interpretation) 

224 

225 
interpretation option!: 

226 
partial_function_definitions "flat_ord None" "flat_lub None" 

227 
by (rule flat_interpretation) 

228 

229 
abbreviation "option_ord \<equiv> flat_ord None" 

230 
abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" 

231 

232 
lemma bind_mono[partial_function_mono]: 

233 
assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)" 

234 
shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))" 

235 
proof (rule monotoneI) 

236 
fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g" 

237 
with mf 

238 
have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g]) 

239 
then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))" 

240 
unfolding flat_ord_def by auto 

241 
also from mg 

242 
have "\<And>y'. option_ord (C y' f) (C y' g)" 

243 
by (rule monotoneD) (rule fg) 

244 
then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))" 

245 
unfolding flat_ord_def by (cases "B g") auto 

246 
finally (option.leq_trans) 

247 
show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" . 

248 
qed 

249 

40252
029400b6c893
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
krauss
parents:
40107
diff
changeset

250 
hide_const (open) chain 
40107  251 

252 
end 

253 