author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 51459  bc3651180a09 
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 

46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46041
diff
changeset

9 
keywords "partial_function" :: thy_decl 
40107  10 
begin 
11 

48891  12 
ML_file "Tools/Function/function_lib.ML" 
13 
ML_file "Tools/Function/partial_function.ML" 

40107  14 
setup Partial_Function.setup 
15 

16 
subsection {* Axiomatic setup *} 

17 

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

42949
618adb3584e5
separate initializations for different modes of partial_function  generation of induction rules will be nonuniform
krauss
parents:
40288
diff
changeset

19 
definitions with ccpo fixed points. *} 
40107  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 

43081  26 
lemma chain_fun: 
27 
assumes A: "chain (fun_ord ord) A" 

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

29 
proof (rule chainI) 

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

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

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

33 
from chainD[OF A fg] 

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

35 
qed 

36 

40107  37 
lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)" 
38 
by (rule monotoneI) (auto simp: fun_ord_def) 

39 

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

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

43 
by (simp add: Let_def) 

44 

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

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

48 
unfolding monotone_def by simp 

49 

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

51 

52 
locale partial_function_definitions = 

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

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

55 
assumes leq_refl: "leq x x" 

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

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

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

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

60 

61 
lemma partial_function_lift: 

62 
assumes "partial_function_definitions ord lb" 

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

64 
proof  

65 
interpret partial_function_definitions ord lb by fact 

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 

43081  78 
by (force intro!: dest: leq_antisym) 
40107  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" 

46041
1e3ff542e83e
remove constant 'ccpo.lub', reuse constant 'Sup' instead
huffman
parents:
45297
diff
changeset

93 
shows "class.ccpo lb ord (mk_less ord)" 
40107  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" 

46041
1e3ff542e83e
remove constant 'ccpo.lub', reuse constant 'Sup' instead
huffman
parents:
45297
diff
changeset

130 
abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun" 
40107  131 
abbreviation "mono_body \<equiv> monotone le_fun leq" 
46041
1e3ff542e83e
remove constant 'ccpo.lub', reuse constant 'Sup' instead
huffman
parents:
45297
diff
changeset

132 
abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun" 
40107  133 

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

135 
orders *} 

136 

46041
1e3ff542e83e
remove constant 'ccpo.lub', reuse constant 'Sup' instead
huffman
parents:
45297
diff
changeset

137 
lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)" 
40107  138 
apply (rule ccpo) 
139 
apply (rule partial_function_lift) 

140 
apply (rule partial_function_definitions_axioms) 

141 
done 

142 

143 
text {* The crucial fixedpoint theorem *} 

144 

145 
lemma mono_body_fixp: 

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

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

148 

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

150 

151 
lemma fixp_rule_uc: 

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

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

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

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

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

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

158 
shows "f = F f" 

159 
proof  

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

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

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

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

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

165 
finally show "f = F f" . 

166 
qed 

167 

43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

168 
text {* Fixpoint induction rule *} 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

169 

8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

170 
lemma fixp_induct_uc: 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

171 
fixes F :: "'c \<Rightarrow> 'c" and 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

172 
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

173 
C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

174 
P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

175 
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

176 
assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

177 
assumes inverse: "\<And>f. U (C f) = f" 
46041
1e3ff542e83e
remove constant 'ccpo.lub', reuse constant 'Sup' instead
huffman
parents:
45297
diff
changeset

178 
assumes adm: "ccpo.admissible lub_fun le_fun P" 
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

179 
assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

180 
shows "P (U f)" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

181 
unfolding eq inverse 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

182 
apply (rule ccpo.fixp_induct[OF ccpo adm]) 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

183 
apply (insert mono, auto simp: monotone_def fun_ord_def)[1] 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

184 
by (rule_tac f="C x" in step, simp add: inverse) 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

185 

8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

186 

40107  187 
text {* Rules for @{term mono_body}: *} 
188 

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

190 
by (rule monotoneI) (rule leq_refl) 

191 

192 
end 

193 

194 

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

196 

197 
definition 

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

199 

200 
definition 

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

202 

203 
lemma flat_interpretation: 

204 
"partial_function_definitions (flat_ord b) (flat_lub b)" 

205 
proof 

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

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

208 
proof cases 

209 
assume "x = b" 

210 
thus ?thesis by (simp add: flat_ord_def) 

211 
next 

212 
assume "x \<noteq> b" 

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

214 
by (auto elim: chainE simp: flat_ord_def) 

215 
then have "flat_lub b A = x" 

216 
by (auto simp: flat_lub_def) 

217 
thus ?thesis by (auto simp: flat_ord_def) 

218 
qed 

219 
next 

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

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

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

223 
proof cases 

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

225 
thus ?thesis 

226 
by (auto simp: flat_lub_def flat_ord_def) 

227 
next 

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

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

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

231 
by (auto elim: chainE simp: flat_ord_def) 

232 
with nb have "flat_lub b A = y" 

233 
by (auto simp: flat_lub_def) 

234 
with z y show ?thesis by auto 

235 
qed 

236 
qed (auto simp: flat_ord_def) 

237 

238 
interpretation tailrec!: 

239 
partial_function_definitions "flat_ord undefined" "flat_lub undefined" 

240 
by (rule flat_interpretation) 

241 

242 
interpretation option!: 

243 
partial_function_definitions "flat_ord None" "flat_lub None" 

244 
by (rule flat_interpretation) 

245 

42949
618adb3584e5
separate initializations for different modes of partial_function  generation of induction rules will be nonuniform
krauss
parents:
40288
diff
changeset

246 

40107  247 
abbreviation "option_ord \<equiv> flat_ord None" 
248 
abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" 

249 

250 
lemma bind_mono[partial_function_mono]: 

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

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

253 
proof (rule monotoneI) 

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

255 
with mf 

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

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

258 
unfolding flat_ord_def by auto 

259 
also from mg 

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

261 
by (rule monotoneD) (rule fg) 

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

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

264 
finally (option.leq_trans) 

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

266 
qed 

267 

43081  268 
lemma flat_lub_in_chain: 
269 
assumes ch: "chain (flat_ord b) A " 

270 
assumes lub: "flat_lub b A = a" 

271 
shows "a = b \<or> a \<in> A" 

272 
proof (cases "A \<subseteq> {b}") 

273 
case True 

274 
then have "flat_lub b A = b" unfolding flat_lub_def by simp 

275 
with lub show ?thesis by simp 

276 
next 

277 
case False 

278 
then obtain c where "c \<in> A" and "c \<noteq> b" by auto 

279 
{ fix z assume "z \<in> A" 

280 
from chainD[OF ch `c \<in> A` this] have "z = c \<or> z = b" 

281 
unfolding flat_ord_def using `c \<noteq> b` by auto } 

282 
with False have "A  {b} = {c}" by auto 

283 
with False have "flat_lub b A = c" by (auto simp: flat_lub_def) 

284 
with `c \<in> A` lub show ?thesis by simp 

285 
qed 

286 

287 
lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option). 

288 
(\<forall>x y. f x = Some y \<longrightarrow> P x y))" 

289 
proof (rule ccpo.admissibleI[OF option.ccpo]) 

290 
fix A :: "('a \<Rightarrow> 'b option) set" 

291 
assume ch: "chain option.le_fun A" 

292 
and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y" 

293 
from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun) 

294 
show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y" 

295 
proof (intro allI impI) 

296 
fix x y assume "option.lub_fun A x = Some y" 

297 
from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]] 

298 
have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp 

299 
then have "\<exists>f\<in>A. f x = Some y" by auto 

300 
with IH show "P x y" by auto 

301 
qed 

302 
qed 

303 

43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

304 
lemma fixp_induct_option: 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

305 
fixes F :: "'c \<Rightarrow> 'c" and 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

306 
U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

307 
C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

308 
P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

309 
assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)" 
46041
1e3ff542e83e
remove constant 'ccpo.lub', reuse constant 'Sup' instead
huffman
parents:
45297
diff
changeset

310 
assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))" 
43082
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

311 
assumes inverse2: "\<And>f. U (C f) = f" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

312 
assumes step: "\<And>f x y. (\<And>x y. U f x = Some y \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = Some y \<Longrightarrow> P x y" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

313 
assumes defined: "U f x = Some y" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

314 
shows "P x y" 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

315 
using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible] 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

316 
by blast 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

317 

8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

318 
declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

319 
@{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

320 

8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

321 
declaration {* Partial_Function.init "option" @{term option.fixp_fun} 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

322 
@{term option.mono_body} @{thm option.fixp_rule_uc} 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

323 
(SOME @{thm fixp_induct_option}) *} 
8d0c44de9773
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
krauss
parents:
43081
diff
changeset

324 

43081  325 

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

326 
hide_const (open) chain 
40107  327 

328 
end 