author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 21243  afffe1f72143 
child 21407  af60523da908 
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 

20819  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 

105 
lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)" 

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 

158 
lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard] 

159 
declare Atom_not_Scons [iff] 

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 

180 
lemmas Leaf_inject = inj_Leaf [THEN injD, standard] 

181 
declare Leaf_inject [dest!] 

182 

183 
lemma inj_Numb: "inj(Numb)" 

184 
apply (simp add: Numb_def o_def) 

185 
apply (rule inj_onI) 

186 
apply (erule Atom_inject [THEN Inr_inject]) 

187 
done 

188 

189 
lemmas Numb_inject = inj_Numb [THEN injD, standard] 

190 
declare Numb_inject [dest!] 

191 

192 

193 
(** Injectiveness of Push_Node **) 

194 

195 
lemma Push_Node_inject: 

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

197 
] ==> P" 

198 
apply (simp add: Push_Node_def) 

199 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

200 
apply (rule Rep_Node [THEN Node_Push_I])+ 

201 
apply (erule sym [THEN apfst_convE]) 

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

203 
done 

204 

205 

206 
(** Injectiveness of Scons **) 

207 

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

209 
apply (simp add: Scons_def One_nat_def) 

210 
apply (blast dest!: Push_Node_inject) 

211 
done 

212 

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

214 
apply (simp add: Scons_def One_nat_def) 

215 
apply (blast dest!: Push_Node_inject) 

216 
done 

217 

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

219 
apply (erule equalityE) 

220 
apply (iprover intro: equalityI Scons_inject_lemma1) 

221 
done 

222 

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

224 
apply (erule equalityE) 

225 
apply (iprover intro: equalityI Scons_inject_lemma2) 

226 
done 

227 

228 
lemma Scons_inject: 

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

230 
by (iprover dest: Scons_inject1 Scons_inject2) 

231 

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

233 
by (blast elim!: Scons_inject) 

234 

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

236 

237 
(** Scons vs Leaf **) 

238 

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

240 
by (simp add: Leaf_def o_def Scons_not_Atom) 

241 

242 
lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard] 

243 
declare Leaf_not_Scons [iff] 

244 

245 
(** Scons vs Numb **) 

246 

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

248 
by (simp add: Numb_def o_def Scons_not_Atom) 

249 

250 
lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard] 

251 
declare Numb_not_Scons [iff] 

252 

253 

254 
(** Leaf vs Numb **) 

255 

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

257 
by (simp add: Leaf_def Numb_def) 

258 

259 
lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard] 

260 
declare Numb_not_Leaf [iff] 

261 

262 

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

264 

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

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

267 

268 
lemma ndepth_Push_Node_aux: 

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

270 
apply (induct_tac "k", auto) 

271 
apply (erule Least_le) 

272 
done 

273 

274 
lemma ndepth_Push_Node: 

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

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

277 
apply (auto simp add: ndepth_def Push_Node_def 

278 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

279 
apply (rule Least_equality) 

280 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

281 
apply (erule LeastI) 

282 
done 

283 

284 

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

286 

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

288 
by (simp add: ntrunc_def) 

289 

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

291 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

292 

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

294 
by (simp add: Leaf_def o_def ntrunc_Atom) 

295 

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

297 
by (simp add: Numb_def o_def ntrunc_Atom) 

298 

299 
lemma ntrunc_Scons [simp]: 

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

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

302 

303 

304 

305 
(** Injection nodes **) 

306 

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

308 
apply (simp add: In0_def) 

309 
apply (simp add: Scons_def) 

310 
done 

311 

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

313 
by (simp add: In0_def) 

314 

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

316 
apply (simp add: In1_def) 

317 
apply (simp add: Scons_def) 

318 
done 

319 

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

321 
by (simp add: In1_def) 

322 

323 

324 
subsection{*Set Constructions*} 

325 

326 

327 
(*** Cartesian Product ***) 

328 

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

330 
by (simp add: uprod_def) 

331 

332 
(*The general elimination rule*) 

333 
lemma uprodE [elim!]: 

334 
"[ c : uprod A B; 

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

336 
] ==> P" 

337 
by (auto simp add: uprod_def) 

338 

339 

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

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

342 
by (auto simp add: uprod_def) 

343 

344 

345 
(*** Disjoint Sum ***) 

346 

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

348 
by (simp add: usum_def) 

349 

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

351 
by (simp add: usum_def) 

352 

353 
lemma usumE [elim!]: 

354 
"[ u : usum A B; 

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

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

357 
] ==> P" 

358 
by (auto simp add: usum_def) 

359 

360 

361 
(** Injection **) 

362 

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

364 
by (auto simp add: In0_def In1_def One_nat_def) 

365 

366 
lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard] 

367 
declare In1_not_In0 [iff] 

368 

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

370 
by (simp add: In0_def) 

371 

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

373 
by (simp add: In1_def) 

374 

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

376 
by (blast dest!: In0_inject) 

377 

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

379 
by (blast dest!: In1_inject) 

380 

381 
lemma inj_In0: "inj In0" 

382 
by (blast intro!: inj_onI) 

383 

384 
lemma inj_In1: "inj In1" 

385 
by (blast intro!: inj_onI) 

386 

387 

388 
(*** Function spaces ***) 

389 

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

391 
apply (simp add: Lim_def) 

392 
apply (rule ext) 

393 
apply (blast elim!: Push_Node_inject) 

394 
done 

395 

396 

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

398 

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

400 
by (auto simp add: ntrunc_def) 

401 

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

403 
by (auto simp add: ntrunc_def) 

404 

405 
(*A generalized form of the takelemma*) 

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

407 
apply (rule equalityI) 

408 
apply (rule_tac [!] ntrunc_subsetD) 

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

410 
done 

411 

412 
lemma ntrunc_o_equality: 

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

414 
apply (rule ntrunc_equality [THEN ext]) 

415 
apply (simp add: expand_fun_eq) 

416 
done 

417 

418 

419 
(*** Monotonicity ***) 

420 

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

422 
by (simp add: uprod_def, blast) 

423 

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

425 
by (simp add: usum_def, blast) 

426 

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

428 
by (simp add: Scons_def, blast) 

429 

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

431 
by (simp add: In0_def subset_refl Scons_mono) 

432 

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

434 
by (simp add: In1_def subset_refl Scons_mono) 

435 

436 

437 
(*** Split and Case ***) 

438 

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

440 
by (simp add: Split_def) 

441 

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

443 
by (simp add: Case_def) 

444 

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

446 
by (simp add: Case_def) 

447 

448 

449 

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

451 

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

453 
by (simp add: ntrunc_def, blast) 

454 

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

456 
by (simp add: Scons_def, blast) 

457 

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

459 
by (simp add: Scons_def, blast) 

460 

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

462 
by (simp add: In0_def Scons_UN1_y) 

463 

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

465 
by (simp add: In1_def Scons_UN1_y) 

466 

467 

468 
(*** Equality for Cartesian Product ***) 

469 

470 
lemma dprodI [intro!]: 

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

472 
by (auto simp add: dprod_def) 

473 

474 
(*The general elimination rule*) 

475 
lemma dprodE [elim!]: 

476 
"[ c : dprod r s; 

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

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

479 
] ==> P" 

480 
by (auto simp add: dprod_def) 

481 

482 

483 
(*** Equality for Disjoint Sum ***) 

484 

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

486 
by (auto simp add: dsum_def) 

487 

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

489 
by (auto simp add: dsum_def) 

490 

491 
lemma dsumE [elim!]: 

492 
"[ w : dsum r s; 

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

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

495 
] ==> P" 

496 
by (auto simp add: dsum_def) 

497 

498 

499 
(*** Monotonicity ***) 

500 

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

502 
by blast 

503 

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

505 
by blast 

506 

507 

508 
(*** Bounding theorems ***) 

509 

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

511 
by blast 

512 

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

514 

515 
(*Dependent version*) 

516 
lemma dprod_subset_Sigma2: 

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

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

519 
by auto 

520 

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

522 
by blast 

523 

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

525 

526 

527 
(*** Domain ***) 

528 

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

530 
by auto 

531 

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

533 
by auto 

534 

535 

536 
subsection {* Finishing the datatype package setup *} 

537 

538 
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} 

20847  539 
setup "DatatypeCodegen.setup_hooks" 
20819  540 
hide (open) const Push Node Atom Leaf Numb Lim Split Case 
541 
hide (open) type node item 

542 

543 

544 
section {* Datatypes *} 

545 

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

547 

5759  548 
rep_datatype bool 
11954  549 
distinct True_not_False False_not_True 
550 
induction bool_induct 

551 

552 
declare case_split [cases type: bool] 

553 
 "prefer plain propositional version" 

554 

555 
rep_datatype unit 

556 
induction unit_induct 

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

557 

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

558 
rep_datatype prod 
11954  559 
inject Pair_eq 
560 
induction prod_induct 

561 

12918  562 
rep_datatype sum 
563 
distinct Inl_not_Inr Inr_not_Inl 

564 
inject Inl_eq Inr_eq 

565 
induction sum_induct 

566 

567 
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" 

568 
apply (rule_tac s = s in sumE) 

569 
apply (erule ssubst) 

20798  570 
apply (rule sum.cases(1)) 
12918  571 
apply (erule ssubst) 
20798  572 
apply (rule sum.cases(2)) 
12918  573 
done 
574 

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

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

20798  577 
by simp 
12918  578 

579 
lemma sum_case_inject: 

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

581 
proof  

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

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

584 
show P 

585 
apply (rule r) 

586 
apply (rule ext) 

14208  587 
apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) 
12918  588 
apply (rule ext) 
14208  589 
apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) 
12918  590 
done 
591 
qed 

592 

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

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

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

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

596 

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

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

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

599 

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

600 
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

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

602 

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

603 
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

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

605 

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

607 

12918  608 

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

11954  610 

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

613 
by (cases y, case_tac b) blast 

11954  614 

615 
lemma prod_induct3 [case_names fields, induct type]: 

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

617 
by (cases x) blast 

618 

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

621 
by (cases y, case_tac c) blast 

11954  622 

623 
lemma prod_induct4 [case_names fields, induct type]: 

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

625 
by (cases x) blast 

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

626 

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

629 
by (cases y, case_tac d) blast 

11954  630 

631 
lemma prod_induct5 [case_names fields, induct type]: 

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

633 
by (cases x) blast 

634 

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

637 
by (cases y, case_tac e) blast 

11954  638 

639 
lemma prod_induct6 [case_names fields, induct type]: 

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

641 
by (cases x) blast 

642 

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

645 
by (cases y, case_tac f) blast 

11954  646 

647 
lemma prod_induct7 [case_names fields, induct type]: 

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

649 
by (cases x) blast 

5759  650 

12918  651 

652 
subsection {* The option type *} 

653 

654 
datatype 'a option = None  Some 'a 

655 

20798  656 
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" 
18576  657 
by (induct x) auto 
658 

20798  659 
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" 
18447  660 
by (induct x) auto 
661 

18576  662 
text{*Although it may appear that both of these equalities are helpful 
663 
only when applied to assumptions, in practice it seems better to give 

664 
them the uniform iff attribute. *} 

12918  665 

666 
lemma option_caseE: 

20798  667 
assumes c: "(case x of None => P  Some y => Q y)" 
668 
obtains 

669 
(None) "x = None" and P 

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

671 
using c by (cases x) simp_all 

12918  672 

673 

674 
subsubsection {* Operations *} 

675 

676 
consts 

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

678 
primrec 

679 
"the (Some x) = x" 

680 

681 
consts 

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

683 
primrec 

684 
"o2s None = {}" 

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

686 

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

688 
by simp 

689 

17876  690 
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} 
12918  691 

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

693 
by (cases xo) auto 

694 

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

696 
by (cases xo) auto 

697 

698 

699 
constdefs 

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

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

702 

703 
lemma option_map_None [simp]: "option_map f None = None" 

704 
by (simp add: option_map_def) 

705 

706 
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" 

707 
by (simp add: option_map_def) 

708 

20798  709 
lemma option_map_is_None [iff]: 
710 
"(option_map f opt = None) = (opt = None)" 

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

14187  712 

12918  713 
lemma option_map_eq_Some [iff]: 
714 
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" 

20798  715 
by (simp add: option_map_def split add: option.split) 
14187  716 

717 
lemma option_map_comp: 

20798  718 
"option_map f (option_map g opt) = option_map (f o g) opt" 
719 
by (simp add: option_map_def split add: option.split) 

12918  720 

721 
lemma option_map_o_sum_case [simp]: 

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

20798  723 
by (rule ext) (simp split: sum.split) 
12918  724 

19787  725 

21111  726 
subsubsection {* Code generator setup *} 
19817  727 

21111  728 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21243
diff
changeset

729 
is_none :: "'a option \<Rightarrow> bool" where 
21111  730 
is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" 
19787  731 

21111  732 
lemma is_none_code [code]: 
733 
shows "is_none None \<longleftrightarrow> True" 

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

735 
unfolding is_none_none [symmetric] by simp_all 

736 

737 
hide (open) const is_none 

19787  738 

17458
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy)  Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset

739 
lemmas [code] = imp_conv_disj 
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy)  Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset

740 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset

741 
lemma [code func]: 
19138  742 
"(\<not> True) = False" by (rule HOL.simp_thms) 
743 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset

744 
lemma [code func]: 
19138  745 
"(\<not> False) = True" by (rule HOL.simp_thms) 
746 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset

747 
lemma [code func]: 
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset

748 
shows "(False \<and> x) = False" 
20798  749 
and "(True \<and> x) = x" 
750 
and "(x \<and> False) = False" 

751 
and "(x \<and> True) = x" by simp_all 

19138  752 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset

753 
lemma [code func]: 
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset

754 
shows "(False \<or> x) = x" 
20798  755 
and "(True \<or> x) = True" 
756 
and "(x \<or> False) = x" 

757 
and "(x \<or> True) = True" by simp_all 

19138  758 

759 
declare 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset

760 
if_True [code func] 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset

761 
if_False [code func] 
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset

762 
fst_conv [code] 
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset

763 
snd_conv [code] 
19138  764 

20105  765 
lemma split_is_prod_case [code inline]: 
20798  766 
"split = prod_case" 
767 
by (simp add: expand_fun_eq split_def prod.cases) 

20105  768 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

769 
code_type bool 
21111  770 
(SML "bool") 
771 
(Haskell "Bool") 

19138  772 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

773 
code_const True and False and Not and "op &" and "op " and If 
21111  774 
(SML "true" and "false" and "not" 
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

775 
and infixl 1 "andalso" and infixl 0 "orelse" 
21126  776 
and "!(if (_)/ then (_)/ else (_))") 
21111  777 
(Haskell "True" and "False" and "not" 
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

778 
and infixl 3 "&&" and infixl 2 "" 
21126  779 
and "!(if (_)/ then (_)/ else (_))") 
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

780 

855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

781 
code_type * 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

782 
(SML infix 2 "*") 
21126  783 
(Haskell "!((_),/ (_))") 
19138  784 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

785 
code_const Pair 
21126  786 
(SML "!((_),/ (_))") 
787 
(Haskell "!((_),/ (_))") 

18702  788 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

789 
code_type unit 
21111  790 
(SML "unit") 
791 
(Haskell "()") 

19150  792 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

793 
code_const Unity 
21111  794 
(SML "()") 
795 
(Haskell "()") 

19150  796 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

797 
code_type option 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

798 
(SML "_ option") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

799 
(Haskell "Maybe _") 
19150  800 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

801 
code_const None and Some 
21111  802 
(SML "NONE" and "SOME") 
803 
(Haskell "Nothing" and "Just") 

19150  804 

20588  805 
code_instance option :: eq 
806 
(Haskell ) 

807 

21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20847
diff
changeset

808 
code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" 
20588  809 
(Haskell infixl 4 "==") 
810 

21079  811 
code_reserved SML 
812 
bool true false not unit option NONE SOME 

813 

814 
code_reserved Haskell 

815 
Bool True False not Maybe Nothing Just 

816 

20819  817 
ML 
818 
{* 

819 
val apfst_conv = thm "apfst_conv"; 

820 
val apfst_convE = thm "apfst_convE"; 

821 
val Push_inject1 = thm "Push_inject1"; 

822 
val Push_inject2 = thm "Push_inject2"; 

823 
val Push_inject = thm "Push_inject"; 

824 
val Push_neq_K0 = thm "Push_neq_K0"; 

825 
val Abs_Node_inj = thm "Abs_Node_inj"; 

826 
val Node_K0_I = thm "Node_K0_I"; 

827 
val Node_Push_I = thm "Node_Push_I"; 

828 
val Scons_not_Atom = thm "Scons_not_Atom"; 

829 
val Atom_not_Scons = thm "Atom_not_Scons"; 

830 
val inj_Atom = thm "inj_Atom"; 

831 
val Atom_inject = thm "Atom_inject"; 

832 
val Atom_Atom_eq = thm "Atom_Atom_eq"; 

833 
val inj_Leaf = thm "inj_Leaf"; 

834 
val Leaf_inject = thm "Leaf_inject"; 

835 
val inj_Numb = thm "inj_Numb"; 

836 
val Numb_inject = thm "Numb_inject"; 

837 
val Push_Node_inject = thm "Push_Node_inject"; 

838 
val Scons_inject1 = thm "Scons_inject1"; 

839 
val Scons_inject2 = thm "Scons_inject2"; 

840 
val Scons_inject = thm "Scons_inject"; 

841 
val Scons_Scons_eq = thm "Scons_Scons_eq"; 

842 
val Scons_not_Leaf = thm "Scons_not_Leaf"; 

843 
val Leaf_not_Scons = thm "Leaf_not_Scons"; 

844 
val Scons_not_Numb = thm "Scons_not_Numb"; 

845 
val Numb_not_Scons = thm "Numb_not_Scons"; 

846 
val Leaf_not_Numb = thm "Leaf_not_Numb"; 

847 
val Numb_not_Leaf = thm "Numb_not_Leaf"; 

848 
val ndepth_K0 = thm "ndepth_K0"; 

849 
val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux"; 

850 
val ndepth_Push_Node = thm "ndepth_Push_Node"; 

851 
val ntrunc_0 = thm "ntrunc_0"; 

852 
val ntrunc_Atom = thm "ntrunc_Atom"; 

853 
val ntrunc_Leaf = thm "ntrunc_Leaf"; 

854 
val ntrunc_Numb = thm "ntrunc_Numb"; 

855 
val ntrunc_Scons = thm "ntrunc_Scons"; 

856 
val ntrunc_one_In0 = thm "ntrunc_one_In0"; 

857 
val ntrunc_In0 = thm "ntrunc_In0"; 

858 
val ntrunc_one_In1 = thm "ntrunc_one_In1"; 

859 
val ntrunc_In1 = thm "ntrunc_In1"; 

860 
val uprodI = thm "uprodI"; 

861 
val uprodE = thm "uprodE"; 

862 
val uprodE2 = thm "uprodE2"; 

863 
val usum_In0I = thm "usum_In0I"; 

864 
val usum_In1I = thm "usum_In1I"; 

865 
val usumE = thm "usumE"; 

866 
val In0_not_In1 = thm "In0_not_In1"; 

867 
val In1_not_In0 = thm "In1_not_In0"; 

868 
val In0_inject = thm "In0_inject"; 

869 
val In1_inject = thm "In1_inject"; 

870 
val In0_eq = thm "In0_eq"; 

871 
val In1_eq = thm "In1_eq"; 

872 
val inj_In0 = thm "inj_In0"; 

873 
val inj_In1 = thm "inj_In1"; 

874 
val Lim_inject = thm "Lim_inject"; 

875 
val ntrunc_subsetI = thm "ntrunc_subsetI"; 

876 
val ntrunc_subsetD = thm "ntrunc_subsetD"; 

877 
val ntrunc_equality = thm "ntrunc_equality"; 

878 
val ntrunc_o_equality = thm "ntrunc_o_equality"; 

879 
val uprod_mono = thm "uprod_mono"; 

880 
val usum_mono = thm "usum_mono"; 

881 
val Scons_mono = thm "Scons_mono"; 

882 
val In0_mono = thm "In0_mono"; 

883 
val In1_mono = thm "In1_mono"; 

884 
val Split = thm "Split"; 

885 
val Case_In0 = thm "Case_In0"; 

886 
val Case_In1 = thm "Case_In1"; 

887 
val ntrunc_UN1 = thm "ntrunc_UN1"; 

888 
val Scons_UN1_x = thm "Scons_UN1_x"; 

889 
val Scons_UN1_y = thm "Scons_UN1_y"; 

890 
val In0_UN1 = thm "In0_UN1"; 

891 
val In1_UN1 = thm "In1_UN1"; 

892 
val dprodI = thm "dprodI"; 

893 
val dprodE = thm "dprodE"; 

894 
val dsum_In0I = thm "dsum_In0I"; 

895 
val dsum_In1I = thm "dsum_In1I"; 

896 
val dsumE = thm "dsumE"; 

897 
val dprod_mono = thm "dprod_mono"; 

898 
val dsum_mono = thm "dsum_mono"; 

899 
val dprod_Sigma = thm "dprod_Sigma"; 

900 
val dprod_subset_Sigma = thm "dprod_subset_Sigma"; 

901 
val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2"; 

902 
val dsum_Sigma = thm "dsum_Sigma"; 

903 
val dsum_subset_Sigma = thm "dsum_subset_Sigma"; 

904 
val Domain_dprod = thm "Domain_dprod"; 

905 
val Domain_dsum = thm "Domain_dsum"; 

906 
*} 

907 

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

908 
end 