author  haftmann 
Thu, 09 Aug 2007 15:52:42 +0200  
changeset 24194  96013f81faef 
parent 24162  8dfd5dd65d82 
child 24286  7619080e49f0 
permissions  rwrr 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Datatype.thy 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
20819  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
11954  4 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
20819  5 

6 
Could <*> be generalized to a general summation (Sigma)? 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

7 
*) 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

8 

21669  9 
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} 
11954  10 

15131  11 
theory Datatype 
21243  12 
imports Nat Sum_Type 
15131  13 
begin 
11954  14 

20819  15 
typedef (Node) 
16 
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" 

17 
{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} 

18 
by auto 

19 

20 
text{*Datatypes will be represented by sets of type @{text node}*} 

21 

22 
types 'a item = "('a, unit) node set" 

23 
('a, 'b) dtree = "('a, 'b) node set" 

24 

25 
consts 

26 
apfst :: "['a=>'c, 'a*'b] => 'c*'b" 

27 
Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" 

28 

29 
Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" 

30 
ndepth :: "('a, 'b) node => nat" 

31 

32 
Atom :: "('a + nat) => ('a, 'b) dtree" 

33 
Leaf :: "'a => ('a, 'b) dtree" 

34 
Numb :: "nat => ('a, 'b) dtree" 

35 
Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree" 

36 
In0 :: "('a, 'b) dtree => ('a, 'b) dtree" 

37 
In1 :: "('a, 'b) dtree => ('a, 'b) dtree" 

38 
Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree" 

39 

40 
ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree" 

41 

42 
uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" 

43 
usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" 

44 

45 
Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" 

46 
Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" 

47 

48 
dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 

49 
=> (('a, 'b) dtree * ('a, 'b) dtree)set" 

50 
dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 

51 
=> (('a, 'b) dtree * ('a, 'b) dtree)set" 

52 

53 

54 
defs 

55 

56 
Push_Node_def: "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" 

57 

58 
(*crude "lists" of nats  needed for the constructions*) 

59 
apfst_def: "apfst == (%f (x,y). (f(x),y))" 

60 
Push_def: "Push == (%b h. nat_case b h)" 

61 

62 
(** operations on Sexpressions  sets of nodes **) 

63 

64 
(*Sexpression constructors*) 

65 
Atom_def: "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" 

66 
Scons_def: "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)" 

67 

68 
(*Leaf nodes, with arbitrary or nat labels*) 

69 
Leaf_def: "Leaf == Atom o Inl" 

70 
Numb_def: "Numb == Atom o Inr" 

71 

72 
(*Injections of the "disjoint sum"*) 

73 
In0_def: "In0(M) == Scons (Numb 0) M" 

74 
In1_def: "In1(M) == Scons (Numb 1) M" 

75 

76 
(*Function spaces*) 

77 
Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}" 

78 

79 
(*the set of nodes with depth less than k*) 

80 
ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" 

81 
ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}" 

82 

83 
(*products and sums for the "universe"*) 

84 
uprod_def: "uprod A B == UN x:A. UN y:B. { Scons x y }" 

85 
usum_def: "usum A B == In0`A Un In1`B" 

86 

87 
(*the corresponding eliminators*) 

88 
Split_def: "Split c M == THE u. EX x y. M = Scons x y & u = c x y" 

89 

90 
Case_def: "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) 

91 
 (EX y . M = In1(y) & u = d(y))" 

92 

93 

94 
(** equality for the "universe" **) 

95 

96 
dprod_def: "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" 

97 

98 
dsum_def: "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 

99 
(UN (y,y'):s. {(In1(y),In1(y'))})" 

100 

101 

102 

103 
(** apfst  can be used in similar type definitions **) 

104 

22886  105 
lemma apfst_conv [simp, code]: "apfst f (a, b) = (f a, b)" 
20819  106 
by (simp add: apfst_def) 
107 

108 

109 
lemma apfst_convE: 

110 
"[ q = apfst f p; !!x y. [ p = (x,y); q = (f(x),y) ] ==> R 

111 
] ==> R" 

112 
by (force simp add: apfst_def) 

113 

114 
(** Push  an injection, analogous to Cons on lists **) 

115 

116 
lemma Push_inject1: "Push i f = Push j g ==> i=j" 

117 
apply (simp add: Push_def expand_fun_eq) 

118 
apply (drule_tac x=0 in spec, simp) 

119 
done 

120 

121 
lemma Push_inject2: "Push i f = Push j g ==> f=g" 

122 
apply (auto simp add: Push_def expand_fun_eq) 

123 
apply (drule_tac x="Suc x" in spec, simp) 

124 
done 

125 

126 
lemma Push_inject: 

127 
"[ Push i f =Push j g; [ i=j; f=g ] ==> P ] ==> P" 

128 
by (blast dest: Push_inject1 Push_inject2) 

129 

130 
lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P" 

131 
by (auto simp add: Push_def expand_fun_eq split: nat.split_asm) 

132 

133 
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard] 

134 

135 

136 
(*** Introduction rules for Node ***) 

137 

138 
lemma Node_K0_I: "(%k. Inr 0, a) : Node" 

139 
by (simp add: Node_def) 

140 

141 
lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node" 

142 
apply (simp add: Node_def Push_def) 

143 
apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) 

144 
done 

145 

146 

147 
subsection{*Freeness: Distinctness of Constructors*} 

148 

149 
(** Scons vs Atom **) 

150 

151 
lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)" 

152 
apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) 

153 
apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 

154 
dest!: Abs_Node_inj 

155 
elim!: apfst_convE sym [THEN Push_neq_K0]) 

156 
done 

157 

21407  158 
lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard] 
159 

20819  160 

161 
(*** Injectiveness ***) 

162 

163 
(** Atomic nodes **) 

164 

165 
lemma inj_Atom: "inj(Atom)" 

166 
apply (simp add: Atom_def) 

167 
apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj) 

168 
done 

169 
lemmas Atom_inject = inj_Atom [THEN injD, standard] 

170 

171 
lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)" 

172 
by (blast dest!: Atom_inject) 

173 

174 
lemma inj_Leaf: "inj(Leaf)" 

175 
apply (simp add: Leaf_def o_def) 

176 
apply (rule inj_onI) 

177 
apply (erule Atom_inject [THEN Inl_inject]) 

178 
done 

179 

21407  180 
lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard] 
20819  181 

182 
lemma inj_Numb: "inj(Numb)" 

183 
apply (simp add: Numb_def o_def) 

184 
apply (rule inj_onI) 

185 
apply (erule Atom_inject [THEN Inr_inject]) 

186 
done 

187 

21407  188 
lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard] 
20819  189 

190 

191 
(** Injectiveness of Push_Node **) 

192 

193 
lemma Push_Node_inject: 

194 
"[ Push_Node i m =Push_Node j n; [ i=j; m=n ] ==> P 

195 
] ==> P" 

196 
apply (simp add: Push_Node_def) 

197 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

198 
apply (rule Rep_Node [THEN Node_Push_I])+ 

199 
apply (erule sym [THEN apfst_convE]) 

200 
apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject) 

201 
done 

202 

203 

204 
(** Injectiveness of Scons **) 

205 

206 
lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'" 

207 
apply (simp add: Scons_def One_nat_def) 

208 
apply (blast dest!: Push_Node_inject) 

209 
done 

210 

211 
lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'" 

212 
apply (simp add: Scons_def One_nat_def) 

213 
apply (blast dest!: Push_Node_inject) 

214 
done 

215 

216 
lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'" 

217 
apply (erule equalityE) 

218 
apply (iprover intro: equalityI Scons_inject_lemma1) 

219 
done 

220 

221 
lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'" 

222 
apply (erule equalityE) 

223 
apply (iprover intro: equalityI Scons_inject_lemma2) 

224 
done 

225 

226 
lemma Scons_inject: 

227 
"[ Scons M N = Scons M' N'; [ M=M'; N=N' ] ==> P ] ==> P" 

228 
by (iprover dest: Scons_inject1 Scons_inject2) 

229 

230 
lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')" 

231 
by (blast elim!: Scons_inject) 

232 

233 
(*** Distinctness involving Leaf and Numb ***) 

234 

235 
(** Scons vs Leaf **) 

236 

237 
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)" 

238 
by (simp add: Leaf_def o_def Scons_not_Atom) 

239 

21407  240 
lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym, standard] 
20819  241 

242 
(** Scons vs Numb **) 

243 

244 
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)" 

245 
by (simp add: Numb_def o_def Scons_not_Atom) 

246 

21407  247 
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard] 
20819  248 

249 

250 
(** Leaf vs Numb **) 

251 

252 
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)" 

253 
by (simp add: Leaf_def Numb_def) 

254 

21407  255 
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard] 
20819  256 

257 

258 
(*** ndepth  the depth of a node ***) 

259 

260 
lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0" 

261 
by (simp add: ndepth_def Node_K0_I [THEN Abs_Node_inverse] Least_equality) 

262 

263 
lemma ndepth_Push_Node_aux: 

264 
"nat_case (Inr (Suc i)) f k = Inr 0 > Suc(LEAST x. f x = Inr 0) <= k" 

265 
apply (induct_tac "k", auto) 

266 
apply (erule Least_le) 

267 
done 

268 

269 
lemma ndepth_Push_Node: 

270 
"ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))" 

271 
apply (insert Rep_Node [of n, unfolded Node_def]) 

272 
apply (auto simp add: ndepth_def Push_Node_def 

273 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

274 
apply (rule Least_equality) 

275 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

276 
apply (erule LeastI) 

277 
done 

278 

279 

280 
(*** ntrunc applied to the various node sets ***) 

281 

282 
lemma ntrunc_0 [simp]: "ntrunc 0 M = {}" 

283 
by (simp add: ntrunc_def) 

284 

285 
lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)" 

286 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

287 

288 
lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)" 

289 
by (simp add: Leaf_def o_def ntrunc_Atom) 

290 

291 
lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)" 

292 
by (simp add: Numb_def o_def ntrunc_Atom) 

293 

294 
lemma ntrunc_Scons [simp]: 

295 
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)" 

296 
by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) 

297 

298 

299 

300 
(** Injection nodes **) 

301 

302 
lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}" 

303 
apply (simp add: In0_def) 

304 
apply (simp add: Scons_def) 

305 
done 

306 

307 
lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)" 

308 
by (simp add: In0_def) 

309 

310 
lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}" 

311 
apply (simp add: In1_def) 

312 
apply (simp add: Scons_def) 

313 
done 

314 

315 
lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)" 

316 
by (simp add: In1_def) 

317 

318 

319 
subsection{*Set Constructions*} 

320 

321 

322 
(*** Cartesian Product ***) 

323 

324 
lemma uprodI [intro!]: "[ M:A; N:B ] ==> Scons M N : uprod A B" 

325 
by (simp add: uprod_def) 

326 

327 
(*The general elimination rule*) 

328 
lemma uprodE [elim!]: 

329 
"[ c : uprod A B; 

330 
!!x y. [ x:A; y:B; c = Scons x y ] ==> P 

331 
] ==> P" 

332 
by (auto simp add: uprod_def) 

333 

334 

335 
(*Elimination of a pair  introduces no eigenvariables*) 

336 
lemma uprodE2: "[ Scons M N : uprod A B; [ M:A; N:B ] ==> P ] ==> P" 

337 
by (auto simp add: uprod_def) 

338 

339 

340 
(*** Disjoint Sum ***) 

341 

342 
lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B" 

343 
by (simp add: usum_def) 

344 

345 
lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B" 

346 
by (simp add: usum_def) 

347 

348 
lemma usumE [elim!]: 

349 
"[ u : usum A B; 

350 
!!x. [ x:A; u=In0(x) ] ==> P; 

351 
!!y. [ y:B; u=In1(y) ] ==> P 

352 
] ==> P" 

353 
by (auto simp add: usum_def) 

354 

355 

356 
(** Injection **) 

357 

358 
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)" 

359 
by (auto simp add: In0_def In1_def One_nat_def) 

360 

21407  361 
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard] 
20819  362 

363 
lemma In0_inject: "In0(M) = In0(N) ==> M=N" 

364 
by (simp add: In0_def) 

365 

366 
lemma In1_inject: "In1(M) = In1(N) ==> M=N" 

367 
by (simp add: In1_def) 

368 

369 
lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)" 

370 
by (blast dest!: In0_inject) 

371 

372 
lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)" 

373 
by (blast dest!: In1_inject) 

374 

375 
lemma inj_In0: "inj In0" 

376 
by (blast intro!: inj_onI) 

377 

378 
lemma inj_In1: "inj In1" 

379 
by (blast intro!: inj_onI) 

380 

381 

382 
(*** Function spaces ***) 

383 

384 
lemma Lim_inject: "Lim f = Lim g ==> f = g" 

385 
apply (simp add: Lim_def) 

386 
apply (rule ext) 

387 
apply (blast elim!: Push_Node_inject) 

388 
done 

389 

390 

391 
(*** proving equality of sets and functions using ntrunc ***) 

392 

393 
lemma ntrunc_subsetI: "ntrunc k M <= M" 

394 
by (auto simp add: ntrunc_def) 

395 

396 
lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N" 

397 
by (auto simp add: ntrunc_def) 

398 

399 
(*A generalized form of the takelemma*) 

400 
lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N" 

401 
apply (rule equalityI) 

402 
apply (rule_tac [!] ntrunc_subsetD) 

403 
apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 

404 
done 

405 

406 
lemma ntrunc_o_equality: 

407 
"[ !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) ] ==> h1=h2" 

408 
apply (rule ntrunc_equality [THEN ext]) 

409 
apply (simp add: expand_fun_eq) 

410 
done 

411 

412 

413 
(*** Monotonicity ***) 

414 

415 
lemma uprod_mono: "[ A<=A'; B<=B' ] ==> uprod A B <= uprod A' B'" 

416 
by (simp add: uprod_def, blast) 

417 

418 
lemma usum_mono: "[ A<=A'; B<=B' ] ==> usum A B <= usum A' B'" 

419 
by (simp add: usum_def, blast) 

420 

421 
lemma Scons_mono: "[ M<=M'; N<=N' ] ==> Scons M N <= Scons M' N'" 

422 
by (simp add: Scons_def, blast) 

423 

424 
lemma In0_mono: "M<=N ==> In0(M) <= In0(N)" 

425 
by (simp add: In0_def subset_refl Scons_mono) 

426 

427 
lemma In1_mono: "M<=N ==> In1(M) <= In1(N)" 

428 
by (simp add: In1_def subset_refl Scons_mono) 

429 

430 

431 
(*** Split and Case ***) 

432 

433 
lemma Split [simp]: "Split c (Scons M N) = c M N" 

434 
by (simp add: Split_def) 

435 

436 
lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)" 

437 
by (simp add: Case_def) 

438 

439 
lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)" 

440 
by (simp add: Case_def) 

441 

442 

443 

444 
(**** UN x. B(x) rules ****) 

445 

446 
lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))" 

447 
by (simp add: ntrunc_def, blast) 

448 

449 
lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)" 

450 
by (simp add: Scons_def, blast) 

451 

452 
lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))" 

453 
by (simp add: Scons_def, blast) 

454 

455 
lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))" 

456 
by (simp add: In0_def Scons_UN1_y) 

457 

458 
lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))" 

459 
by (simp add: In1_def Scons_UN1_y) 

460 

461 

462 
(*** Equality for Cartesian Product ***) 

463 

464 
lemma dprodI [intro!]: 

465 
"[ (M,M'):r; (N,N'):s ] ==> (Scons M N, Scons M' N') : dprod r s" 

466 
by (auto simp add: dprod_def) 

467 

468 
(*The general elimination rule*) 

469 
lemma dprodE [elim!]: 

470 
"[ c : dprod r s; 

471 
!!x y x' y'. [ (x,x') : r; (y,y') : s; 

472 
c = (Scons x y, Scons x' y') ] ==> P 

473 
] ==> P" 

474 
by (auto simp add: dprod_def) 

475 

476 

477 
(*** Equality for Disjoint Sum ***) 

478 

479 
lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s" 

480 
by (auto simp add: dsum_def) 

481 

482 
lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s" 

483 
by (auto simp add: dsum_def) 

484 

485 
lemma dsumE [elim!]: 

486 
"[ w : dsum r s; 

487 
!!x x'. [ (x,x') : r; w = (In0(x), In0(x')) ] ==> P; 

488 
!!y y'. [ (y,y') : s; w = (In1(y), In1(y')) ] ==> P 

489 
] ==> P" 

490 
by (auto simp add: dsum_def) 

491 

492 

493 
(*** Monotonicity ***) 

494 

495 
lemma dprod_mono: "[ r<=r'; s<=s' ] ==> dprod r s <= dprod r' s'" 

496 
by blast 

497 

498 
lemma dsum_mono: "[ r<=r'; s<=s' ] ==> dsum r s <= dsum r' s'" 

499 
by blast 

500 

501 

502 
(*** Bounding theorems ***) 

503 

504 
lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)" 

505 
by blast 

506 

507 
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard] 

508 

509 
(*Dependent version*) 

510 
lemma dprod_subset_Sigma2: 

511 
"(dprod (Sigma A B) (Sigma C D)) <= 

512 
Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" 

513 
by auto 

514 

515 
lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)" 

516 
by blast 

517 

518 
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard] 

519 

520 

521 
(*** Domain ***) 

522 

523 
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" 

524 
by auto 

525 

526 
lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" 

527 
by auto 

528 

529 

530 
subsection {* Finishing the datatype package setup *} 

531 

20847  532 
setup "DatatypeCodegen.setup_hooks" 
24162
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

533 
text {* hides popular names *} 
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

534 
hide (open) type node item 
20819  535 
hide (open) const Push Node Atom Leaf Numb Lim Split Case 
536 

537 

538 
section {* Datatypes *} 

539 

11954  540 
subsection {* Representing primitive types *} 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

541 

24194  542 
rep_datatype bool 
543 
distinct True_not_False False_not_True 

544 
induction bool_induct 

545 

11954  546 
declare case_split [cases type: bool] 
547 
 "prefer plain propositional version" 

548 

24194  549 
lemma size_bool [code func]: 
550 
"size (b\<Colon>bool) = 0" by (cases b) auto 

551 

552 
rep_datatype unit 

553 
induction unit_induct 

554 

555 
rep_datatype prod 

556 
inject Pair_eq 

557 
induction prod_induct 

558 

22782  559 
lemmas prod_caseI = prod.cases [THEN iffD2, standard] 
560 

561 
lemma prod_caseI2: "!!p. [ !!a b. p = (a, b) ==> c a b ] ==> prod_case c p" 

562 
by auto 

563 

564 
lemma prod_caseI2': "!!p. [ !!a b. (a, b) = p ==> c a b x ] ==> prod_case c p x" 

565 
by (auto simp: split_tupled_all) 

566 

567 
lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" 

568 
by (induct p) auto 

569 

570 
lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" 

571 
by (induct p) auto 

572 

573 
lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" 

574 
by (simp add: expand_fun_eq) 

575 

576 
declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] 

577 
declare prod_caseE' [elim!] prod_caseE [elim!] 

578 

24162
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

579 
lemma prod_case_split [code post]: 
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

580 
"prod_case = split" 
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

581 
by (auto simp add: expand_fun_eq) 
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

582 

8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

583 
lemmas [code inline] = prod_case_split [symmetric] 
12918  584 

24194  585 
rep_datatype sum 
586 
distinct Inl_not_Inr Inr_not_Inl 

587 
inject Inl_eq Inr_eq 

588 
induction sum_induct 

589 

590 
lemma size_sum [code func]: 

591 
"size (x \<Colon> 'a + 'b) = 0" by (cases x) auto 

592 

22230  593 
lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)" 
594 
by (rule ext) (simp split: sum.split) 

595 

12918  596 
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" 
597 
apply (rule_tac s = s in sumE) 

598 
apply (erule ssubst) 

20798  599 
apply (rule sum.cases(1)) 
12918  600 
apply (erule ssubst) 
20798  601 
apply (rule sum.cases(2)) 
12918  602 
done 
603 

604 
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" 

605 
 {* Prevents simplification of @{text f} and @{text g}: much faster. *} 

20798  606 
by simp 
12918  607 

608 
lemma sum_case_inject: 

609 
"sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" 

610 
proof  

611 
assume a: "sum_case f1 f2 = sum_case g1 g2" 

612 
assume r: "f1 = g1 ==> f2 = g2 ==> P" 

613 
show P 

614 
apply (rule r) 

615 
apply (rule ext) 

14208  616 
apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) 
12918  617 
apply (rule ext) 
14208  618 
apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) 
12918  619 
done 
620 
qed 

621 

13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

622 
constdefs 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

623 
Suml :: "('a => 'c) => 'a + 'b => 'c" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

624 
"Suml == (%f. sum_case f arbitrary)" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

625 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

626 
Sumr :: "('b => 'c) => 'a + 'b => 'c" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

627 
"Sumr == sum_case arbitrary" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

628 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

629 
lemma Suml_inject: "Suml f = Suml g ==> f = g" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

630 
by (unfold Suml_def) (erule sum_case_inject) 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

631 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

632 
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

633 
by (unfold Sumr_def) (erule sum_case_inject) 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

634 

20798  635 
hide (open) const Suml Sumr 
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

636 

12918  637 

638 
subsection {* Further cases/induct rules for tuples *} 

11954  639 

20798  640 
lemma prod_cases3 [cases type]: 
641 
obtains (fields) a b c where "y = (a, b, c)" 

642 
by (cases y, case_tac b) blast 

11954  643 

644 
lemma prod_induct3 [case_names fields, induct type]: 

645 
"(!!a b c. P (a, b, c)) ==> P x" 

646 
by (cases x) blast 

647 

20798  648 
lemma prod_cases4 [cases type]: 
649 
obtains (fields) a b c d where "y = (a, b, c, d)" 

650 
by (cases y, case_tac c) blast 

11954  651 

652 
lemma prod_induct4 [case_names fields, induct type]: 

653 
"(!!a b c d. P (a, b, c, d)) ==> P x" 

654 
by (cases x) blast 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

655 

20798  656 
lemma prod_cases5 [cases type]: 
657 
obtains (fields) a b c d e where "y = (a, b, c, d, e)" 

658 
by (cases y, case_tac d) blast 

11954  659 

660 
lemma prod_induct5 [case_names fields, induct type]: 

661 
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" 

662 
by (cases x) blast 

663 

20798  664 
lemma prod_cases6 [cases type]: 
665 
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" 

666 
by (cases y, case_tac e) blast 

11954  667 

668 
lemma prod_induct6 [case_names fields, induct type]: 

669 
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" 

670 
by (cases x) blast 

671 

20798  672 
lemma prod_cases7 [cases type]: 
673 
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" 

674 
by (cases y, case_tac f) blast 

11954  675 

676 
lemma prod_induct7 [case_names fields, induct type]: 

677 
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" 

678 
by (cases x) blast 

5759  679 

24194  680 

681 
subsection {* The option datatype *} 

682 

683 
datatype 'a option = None  Some 'a 

684 

685 
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" 

686 
by (induct x) auto 

687 

688 
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" 

689 
by (induct x) auto 

690 

691 
text{*Although it may appear that both of these equalities are helpful 

692 
only when applied to assumptions, in practice it seems better to give 

693 
them the uniform iff attribute. *} 

694 

695 
lemma option_caseE: 

696 
assumes c: "(case x of None => P  Some y => Q y)" 

697 
obtains 

698 
(None) "x = None" and P 

699 
 (Some) y where "x = Some y" and "Q y" 

700 
using c by (cases x) simp_all 

701 

702 

703 
subsubsection {* Operations *} 

704 

705 
consts 

706 
the :: "'a option => 'a" 

707 
primrec 

708 
"the (Some x) = x" 

709 

710 
consts 

711 
o2s :: "'a option => 'a set" 

712 
primrec 

713 
"o2s None = {}" 

714 
"o2s (Some x) = {x}" 

715 

716 
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" 

717 
by simp 

718 

719 
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} 

720 

721 
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" 

722 
by (cases xo) auto 

723 

724 
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" 

725 
by (cases xo) auto 

726 

727 

728 
constdefs 

729 
option_map :: "('a => 'b) => ('a option => 'b option)" 

730 
"option_map == %f y. case y of None => None  Some x => Some (f x)" 

731 

732 
lemmas [code func del] = option_map_def 

733 

734 
lemma option_map_None [simp, code]: "option_map f None = None" 

735 
by (simp add: option_map_def) 

736 

737 
lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)" 

738 
by (simp add: option_map_def) 

739 

740 
lemma option_map_is_None [iff]: 

741 
"(option_map f opt = None) = (opt = None)" 

742 
by (simp add: option_map_def split add: option.split) 

743 

744 
lemma option_map_eq_Some [iff]: 

745 
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" 

746 
by (simp add: option_map_def split add: option.split) 

747 

748 
lemma option_map_comp: 

749 
"option_map f (option_map g opt) = option_map (f o g) opt" 

750 
by (simp add: option_map_def split add: option.split) 

751 

752 
lemma option_map_o_sum_case [simp]: 

753 
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" 

754 
by (rule ext) (simp split: sum.split) 

755 

756 

757 
subsubsection {* Code generator setup *} 

758 

759 
definition 

760 
is_none :: "'a option \<Rightarrow> bool" where 

761 
is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" 

762 

763 
lemma is_none_code [code]: 

764 
shows "is_none None \<longleftrightarrow> True" 

765 
and "is_none (Some x) \<longleftrightarrow> False" 

766 
unfolding is_none_none [symmetric] by simp_all 

767 

768 
hide (open) const is_none 

769 

770 
code_type option 

771 
(SML "_ option") 

772 
(OCaml "_ option") 

773 
(Haskell "Maybe _") 

774 

775 
code_const None and Some 

776 
(SML "NONE" and "SOME") 

777 
(OCaml "None" and "Some _") 

778 
(Haskell "Nothing" and "Just") 

779 

780 
code_instance option :: eq 

781 
(Haskell ) 

782 

783 
code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" 

784 
(Haskell infixl 4 "==") 

785 

786 
code_reserved SML 

787 
option NONE SOME 

788 

789 
code_reserved OCaml 

790 
option None Some 

791 

792 
code_modulename SML 

793 
Datatype Nat 

794 

795 
code_modulename OCaml 

796 
Datatype Nat 

797 

798 
code_modulename Haskell 

799 
Datatype Nat 

800 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

801 
end 