author  wenzelm 
Sun, 01 Oct 2006 22:19:21 +0200  
changeset 20819  cb6ae81dd0be 
parent 20798  3275b03e2fff 
child 20847  7e8c724339e0 
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 
20819  12 
imports NatArith Sum_Type 
15131  13 
begin 
11954  14 

20819  15 

16 
typedef (Node) 

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

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

19 
by auto 

20 

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

22 

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

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

25 

26 
consts 

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

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

29 

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

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

32 

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

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

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

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

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

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

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

40 

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

42 

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

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

45 

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

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

48 

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

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

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

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

53 

54 

55 
defs 

56 

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

58 

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

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

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

62 

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

64 

65 
(*Sexpression constructors*) 

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

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

68 

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

70 
Leaf_def: "Leaf == Atom o Inl" 

71 
Numb_def: "Numb == Atom o Inr" 

72 

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

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

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

76 

77 
(*Function spaces*) 

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

79 

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

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

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

83 

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

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

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

87 

88 
(*the corresponding eliminators*) 

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

90 

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

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

93 

94 

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

96 

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

98 

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

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

101 

102 

103 

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

105 

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

107 
by (simp add: apfst_def) 

108 

109 

110 
lemma apfst_convE: 

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

112 
] ==> R" 

113 
by (force simp add: apfst_def) 

114 

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

116 

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

118 
apply (simp add: Push_def expand_fun_eq) 

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

120 
done 

121 

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

123 
apply (auto simp add: Push_def expand_fun_eq) 

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

125 
done 

126 

127 
lemma Push_inject: 

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

129 
by (blast dest: Push_inject1 Push_inject2) 

130 

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

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

133 

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

135 

136 

137 
(*** Introduction rules for Node ***) 

138 

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

140 
by (simp add: Node_def) 

141 

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

143 
apply (simp add: Node_def Push_def) 

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

145 
done 

146 

147 

148 
subsection{*Freeness: Distinctness of Constructors*} 

149 

150 
(** Scons vs Atom **) 

151 

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

153 
apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) 

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

155 
dest!: Abs_Node_inj 

156 
elim!: apfst_convE sym [THEN Push_neq_K0]) 

157 
done 

158 

159 
lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard] 

160 
declare Atom_not_Scons [iff] 

161 

162 
(*** Injectiveness ***) 

163 

164 
(** Atomic nodes **) 

165 

166 
lemma inj_Atom: "inj(Atom)" 

167 
apply (simp add: Atom_def) 

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

169 
done 

170 
lemmas Atom_inject = inj_Atom [THEN injD, standard] 

171 

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

173 
by (blast dest!: Atom_inject) 

174 

175 
lemma inj_Leaf: "inj(Leaf)" 

176 
apply (simp add: Leaf_def o_def) 

177 
apply (rule inj_onI) 

178 
apply (erule Atom_inject [THEN Inl_inject]) 

179 
done 

180 

181 
lemmas Leaf_inject = inj_Leaf [THEN injD, standard] 

182 
declare Leaf_inject [dest!] 

183 

184 
lemma inj_Numb: "inj(Numb)" 

185 
apply (simp add: Numb_def o_def) 

186 
apply (rule inj_onI) 

187 
apply (erule Atom_inject [THEN Inr_inject]) 

188 
done 

189 

190 
lemmas Numb_inject = inj_Numb [THEN injD, standard] 

191 
declare Numb_inject [dest!] 

192 

193 

194 
(** Injectiveness of Push_Node **) 

195 

196 
lemma Push_Node_inject: 

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

198 
] ==> P" 

199 
apply (simp add: Push_Node_def) 

200 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

201 
apply (rule Rep_Node [THEN Node_Push_I])+ 

202 
apply (erule sym [THEN apfst_convE]) 

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

204 
done 

205 

206 

207 
(** Injectiveness of Scons **) 

208 

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

210 
apply (simp add: Scons_def One_nat_def) 

211 
apply (blast dest!: Push_Node_inject) 

212 
done 

213 

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

215 
apply (simp add: Scons_def One_nat_def) 

216 
apply (blast dest!: Push_Node_inject) 

217 
done 

218 

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

220 
apply (erule equalityE) 

221 
apply (iprover intro: equalityI Scons_inject_lemma1) 

222 
done 

223 

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

225 
apply (erule equalityE) 

226 
apply (iprover intro: equalityI Scons_inject_lemma2) 

227 
done 

228 

229 
lemma Scons_inject: 

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

231 
by (iprover dest: Scons_inject1 Scons_inject2) 

232 

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

234 
by (blast elim!: Scons_inject) 

235 

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

237 

238 
(** Scons vs Leaf **) 

239 

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

241 
by (simp add: Leaf_def o_def Scons_not_Atom) 

242 

243 
lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard] 

244 
declare Leaf_not_Scons [iff] 

245 

246 
(** Scons vs Numb **) 

247 

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

249 
by (simp add: Numb_def o_def Scons_not_Atom) 

250 

251 
lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard] 

252 
declare Numb_not_Scons [iff] 

253 

254 

255 
(** Leaf vs Numb **) 

256 

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

258 
by (simp add: Leaf_def Numb_def) 

259 

260 
lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard] 

261 
declare Numb_not_Leaf [iff] 

262 

263 

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

265 

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

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

268 

269 
lemma ndepth_Push_Node_aux: 

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

271 
apply (induct_tac "k", auto) 

272 
apply (erule Least_le) 

273 
done 

274 

275 
lemma ndepth_Push_Node: 

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

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

278 
apply (auto simp add: ndepth_def Push_Node_def 

279 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

280 
apply (rule Least_equality) 

281 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

282 
apply (erule LeastI) 

283 
done 

284 

285 

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

287 

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

289 
by (simp add: ntrunc_def) 

290 

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

292 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

293 

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

295 
by (simp add: Leaf_def o_def ntrunc_Atom) 

296 

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

298 
by (simp add: Numb_def o_def ntrunc_Atom) 

299 

300 
lemma ntrunc_Scons [simp]: 

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

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

303 

304 

305 

306 
(** Injection nodes **) 

307 

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

309 
apply (simp add: In0_def) 

310 
apply (simp add: Scons_def) 

311 
done 

312 

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

314 
by (simp add: In0_def) 

315 

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

317 
apply (simp add: In1_def) 

318 
apply (simp add: Scons_def) 

319 
done 

320 

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

322 
by (simp add: In1_def) 

323 

324 

325 
subsection{*Set Constructions*} 

326 

327 

328 
(*** Cartesian Product ***) 

329 

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

331 
by (simp add: uprod_def) 

332 

333 
(*The general elimination rule*) 

334 
lemma uprodE [elim!]: 

335 
"[ c : uprod A B; 

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

337 
] ==> P" 

338 
by (auto simp add: uprod_def) 

339 

340 

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

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

343 
by (auto simp add: uprod_def) 

344 

345 

346 
(*** Disjoint Sum ***) 

347 

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

349 
by (simp add: usum_def) 

350 

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

352 
by (simp add: usum_def) 

353 

354 
lemma usumE [elim!]: 

355 
"[ u : usum A B; 

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

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

358 
] ==> P" 

359 
by (auto simp add: usum_def) 

360 

361 

362 
(** Injection **) 

363 

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

365 
by (auto simp add: In0_def In1_def One_nat_def) 

366 

367 
lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard] 

368 
declare In1_not_In0 [iff] 

369 

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

371 
by (simp add: In0_def) 

372 

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

374 
by (simp add: In1_def) 

375 

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

377 
by (blast dest!: In0_inject) 

378 

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

380 
by (blast dest!: In1_inject) 

381 

382 
lemma inj_In0: "inj In0" 

383 
by (blast intro!: inj_onI) 

384 

385 
lemma inj_In1: "inj In1" 

386 
by (blast intro!: inj_onI) 

387 

388 

389 
(*** Function spaces ***) 

390 

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

392 
apply (simp add: Lim_def) 

393 
apply (rule ext) 

394 
apply (blast elim!: Push_Node_inject) 

395 
done 

396 

397 

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

399 

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

401 
by (auto simp add: ntrunc_def) 

402 

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

404 
by (auto simp add: ntrunc_def) 

405 

406 
(*A generalized form of the takelemma*) 

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

408 
apply (rule equalityI) 

409 
apply (rule_tac [!] ntrunc_subsetD) 

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

411 
done 

412 

413 
lemma ntrunc_o_equality: 

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

415 
apply (rule ntrunc_equality [THEN ext]) 

416 
apply (simp add: expand_fun_eq) 

417 
done 

418 

419 

420 
(*** Monotonicity ***) 

421 

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

423 
by (simp add: uprod_def, blast) 

424 

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

426 
by (simp add: usum_def, blast) 

427 

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

429 
by (simp add: Scons_def, blast) 

430 

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

432 
by (simp add: In0_def subset_refl Scons_mono) 

433 

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

435 
by (simp add: In1_def subset_refl Scons_mono) 

436 

437 

438 
(*** Split and Case ***) 

439 

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

441 
by (simp add: Split_def) 

442 

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

444 
by (simp add: Case_def) 

445 

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

447 
by (simp add: Case_def) 

448 

449 

450 

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

452 

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

454 
by (simp add: ntrunc_def, blast) 

455 

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

457 
by (simp add: Scons_def, blast) 

458 

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

460 
by (simp add: Scons_def, blast) 

461 

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

463 
by (simp add: In0_def Scons_UN1_y) 

464 

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

466 
by (simp add: In1_def Scons_UN1_y) 

467 

468 

469 
(*** Equality for Cartesian Product ***) 

470 

471 
lemma dprodI [intro!]: 

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

473 
by (auto simp add: dprod_def) 

474 

475 
(*The general elimination rule*) 

476 
lemma dprodE [elim!]: 

477 
"[ c : dprod r s; 

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

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

480 
] ==> P" 

481 
by (auto simp add: dprod_def) 

482 

483 

484 
(*** Equality for Disjoint Sum ***) 

485 

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

487 
by (auto simp add: dsum_def) 

488 

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

490 
by (auto simp add: dsum_def) 

491 

492 
lemma dsumE [elim!]: 

493 
"[ w : dsum r s; 

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

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

496 
] ==> P" 

497 
by (auto simp add: dsum_def) 

498 

499 

500 
(*** Monotonicity ***) 

501 

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

503 
by blast 

504 

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

506 
by blast 

507 

508 

509 
(*** Bounding theorems ***) 

510 

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

512 
by blast 

513 

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

515 

516 
(*Dependent version*) 

517 
lemma dprod_subset_Sigma2: 

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

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

520 
by auto 

521 

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

523 
by blast 

524 

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

526 

527 

528 
(*** Domain ***) 

529 

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

531 
by auto 

532 

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

534 
by auto 

535 

536 

537 
subsection {* Finishing the datatype package setup *} 

538 

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

540 
hide (open) const Push Node Atom Leaf Numb Lim Split Case 

541 
hide (open) type node item 

542 

543 

544 
section {* Datatypes *} 

545 

20588  546 
setup "DatatypeCodegen.setup2" 
547 

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

549 

5759  550 
rep_datatype bool 
11954  551 
distinct True_not_False False_not_True 
552 
induction bool_induct 

553 

554 
declare case_split [cases type: bool] 

555 
 "prefer plain propositional version" 

556 

557 
rep_datatype unit 

558 
induction unit_induct 

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

559 

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

560 
rep_datatype prod 
11954  561 
inject Pair_eq 
562 
induction prod_induct 

563 

12918  564 
rep_datatype sum 
565 
distinct Inl_not_Inr Inr_not_Inl 

566 
inject Inl_eq Inr_eq 

567 
induction sum_induct 

568 

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

570 
apply (rule_tac s = s in sumE) 

571 
apply (erule ssubst) 

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

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

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

20798  579 
by simp 
12918  580 

581 
lemma sum_case_inject: 

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

583 
proof  

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

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

586 
show P 

587 
apply (rule r) 

588 
apply (rule ext) 

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

594 

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

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

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

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

598 

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

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

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

601 

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

602 
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

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

604 

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

605 
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

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

607 

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

609 

12918  610 

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

11954  612 

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

615 
by (cases y, case_tac b) blast 

11954  616 

617 
lemma prod_induct3 [case_names fields, induct type]: 

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

619 
by (cases x) blast 

620 

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

623 
by (cases y, case_tac c) blast 

11954  624 

625 
lemma prod_induct4 [case_names fields, induct type]: 

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

627 
by (cases x) blast 

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

628 

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

631 
by (cases y, case_tac d) blast 

11954  632 

633 
lemma prod_induct5 [case_names fields, induct type]: 

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

635 
by (cases x) blast 

636 

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

639 
by (cases y, case_tac e) blast 

11954  640 

641 
lemma prod_induct6 [case_names fields, induct type]: 

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

643 
by (cases x) blast 

644 

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

647 
by (cases y, case_tac f) blast 

11954  648 

649 
lemma prod_induct7 [case_names fields, induct type]: 

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

651 
by (cases x) blast 

5759  652 

12918  653 

654 
subsection {* The option type *} 

655 

656 
datatype 'a option = None  Some 'a 

657 

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

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

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

666 
them the uniform iff attribute. *} 

12918  667 

668 
lemma option_caseE: 

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

671 
(None) "x = None" and P 

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

673 
using c by (cases x) simp_all 

12918  674 

675 

676 
subsubsection {* Operations *} 

677 

678 
consts 

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

680 
primrec 

681 
"the (Some x) = x" 

682 

683 
consts 

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

685 
primrec 

686 
"o2s None = {}" 

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

688 

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

690 
by simp 

691 

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

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

695 
by (cases xo) auto 

696 

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

698 
by (cases xo) auto 

699 

700 

701 
constdefs 

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

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

704 

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

706 
by (simp add: option_map_def) 

707 

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

709 
by (simp add: option_map_def) 

710 

20798  711 
lemma option_map_is_None [iff]: 
712 
"(option_map f opt = None) = (opt = None)" 

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

14187  714 

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

20798  717 
by (simp add: option_map_def split add: option.split) 
14187  718 

719 
lemma option_map_comp: 

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

12918  722 

723 
lemma option_map_o_sum_case [simp]: 

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

20798  725 
by (rule ext) (simp split: sum.split) 
12918  726 

19787  727 

19817  728 
subsubsection {* Codegenerator setup *} 
729 

19787  730 
consts 
731 
is_none :: "'a option \<Rightarrow> bool" 

732 
primrec 

733 
"is_none None = True" 

734 
"is_none (Some x) = False" 

735 

20105  736 
lemma is_none_none [code inline]: 
20798  737 
"(x = None) = (is_none x)" 
738 
by (cases x) simp_all 

19787  739 

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

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

741 

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

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

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

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

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

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

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

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

19138  753 

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

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

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

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

19138  759 

760 
declare 

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

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

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

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

764 
snd_conv [code] 
19138  765 

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

20105  769 

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

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

771 
(SML target_atom "bool") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

772 
(Haskell target_atom "Bool") 
19138  773 

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

774 
code_const True and False and Not and "op &" and "op " and If 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

775 
(SML target_atom "true" and target_atom "false" and target_atom "not" 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

776 
and infixl 1 "andalso" and infixl 0 "orelse" 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

777 
and target_atom "(if __/ then __/ else __)") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

778 
(Haskell target_atom "True" and target_atom "False" and target_atom "not" 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

779 
and infixl 3 "&&" and infixl 2 "" 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

780 
and target_atom "(if __/ then __/ else __)") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

781 

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

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

783 
(SML infix 2 "*") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

784 
(Haskell target_atom "(__,/ __)") 
19138  785 

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

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

787 
(SML target_atom "(__,/ __)") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

788 
(Haskell target_atom "(__,/ __)") 
18702  789 

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

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

791 
(SML target_atom "unit") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

792 
(Haskell target_atom "()") 
19150  793 

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

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

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

796 
(Haskell target_atom "()") 
19150  797 

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

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

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

800 
(Haskell "Maybe _") 
19150  801 

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

802 
code_const None and Some 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

803 
(SML target_atom "NONE" and target_atom "SOME") 
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset

804 
(Haskell target_atom "Nothing" and target_atom "Just") 
19150  805 

20588  806 
code_instance option :: eq 
807 
(Haskell ) 

808 

809 
code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" 

810 
(Haskell infixl 4 "==") 

811 

20819  812 
ML 
813 
{* 

814 
val apfst_conv = thm "apfst_conv"; 

815 
val apfst_convE = thm "apfst_convE"; 

816 
val Push_inject1 = thm "Push_inject1"; 

817 
val Push_inject2 = thm "Push_inject2"; 

818 
val Push_inject = thm "Push_inject"; 

819 
val Push_neq_K0 = thm "Push_neq_K0"; 

820 
val Abs_Node_inj = thm "Abs_Node_inj"; 

821 
val Node_K0_I = thm "Node_K0_I"; 

822 
val Node_Push_I = thm "Node_Push_I"; 

823 
val Scons_not_Atom = thm "Scons_not_Atom"; 

824 
val Atom_not_Scons = thm "Atom_not_Scons"; 

825 
val inj_Atom = thm "inj_Atom"; 

826 
val Atom_inject = thm "Atom_inject"; 

827 
val Atom_Atom_eq = thm "Atom_Atom_eq"; 

828 
val inj_Leaf = thm "inj_Leaf"; 

829 
val Leaf_inject = thm "Leaf_inject"; 

830 
val inj_Numb = thm "inj_Numb"; 

831 
val Numb_inject = thm "Numb_inject"; 

832 
val Push_Node_inject = thm "Push_Node_inject"; 

833 
val Scons_inject1 = thm "Scons_inject1"; 

834 
val Scons_inject2 = thm "Scons_inject2"; 

835 
val Scons_inject = thm "Scons_inject"; 

836 
val Scons_Scons_eq = thm "Scons_Scons_eq"; 

837 
val Scons_not_Leaf = thm "Scons_not_Leaf"; 

838 
val Leaf_not_Scons = thm "Leaf_not_Scons"; 

839 
val Scons_not_Numb = thm "Scons_not_Numb"; 

840 
val Numb_not_Scons = thm "Numb_not_Scons"; 

841 
val Leaf_not_Numb = thm "Leaf_not_Numb"; 

842 
val Numb_not_Leaf = thm "Numb_not_Leaf"; 

843 
val ndepth_K0 = thm "ndepth_K0"; 

844 
val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux"; 

845 
val ndepth_Push_Node = thm "ndepth_Push_Node"; 

846 
val ntrunc_0 = thm "ntrunc_0"; 

847 
val ntrunc_Atom = thm "ntrunc_Atom"; 

848 
val ntrunc_Leaf = thm "ntrunc_Leaf"; 

849 
val ntrunc_Numb = thm "ntrunc_Numb"; 

850 
val ntrunc_Scons = thm "ntrunc_Scons"; 

851 
val ntrunc_one_In0 = thm "ntrunc_one_In0"; 

852 
val ntrunc_In0 = thm "ntrunc_In0"; 

853 
val ntrunc_one_In1 = thm "ntrunc_one_In1"; 

854 
val ntrunc_In1 = thm "ntrunc_In1"; 

855 
val uprodI = thm "uprodI"; 

856 
val uprodE = thm "uprodE"; 

857 
val uprodE2 = thm "uprodE2"; 

858 
val usum_In0I = thm "usum_In0I"; 

859 
val usum_In1I = thm "usum_In1I"; 

860 
val usumE = thm "usumE"; 

861 
val In0_not_In1 = thm "In0_not_In1"; 

862 
val In1_not_In0 = thm "In1_not_In0"; 

863 
val In0_inject = thm "In0_inject"; 

864 
val In1_inject = thm "In1_inject"; 

865 
val In0_eq = thm "In0_eq"; 

866 
val In1_eq = thm "In1_eq"; 

867 
val inj_In0 = thm "inj_In0"; 

868 
val inj_In1 = thm "inj_In1"; 

869 
val Lim_inject = thm "Lim_inject"; 

870 
val ntrunc_subsetI = thm "ntrunc_subsetI"; 

871 
val ntrunc_subsetD = thm "ntrunc_subsetD"; 

872 
val ntrunc_equality = thm "ntrunc_equality"; 

873 
val ntrunc_o_equality = thm "ntrunc_o_equality"; 

874 
val uprod_mono = thm "uprod_mono"; 

875 
val usum_mono = thm "usum_mono"; 

876 
val Scons_mono = thm "Scons_mono"; 

877 
val In0_mono = thm "In0_mono"; 

878 
val In1_mono = thm "In1_mono"; 

879 
val Split = thm "Split"; 

880 
val Case_In0 = thm "Case_In0"; 

881 
val Case_In1 = thm "Case_In1"; 

882 
val ntrunc_UN1 = thm "ntrunc_UN1"; 

883 
val Scons_UN1_x = thm "Scons_UN1_x"; 

884 
val Scons_UN1_y = thm "Scons_UN1_y"; 

885 
val In0_UN1 = thm "In0_UN1"; 

886 
val In1_UN1 = thm "In1_UN1"; 

887 
val dprodI = thm "dprodI"; 

888 
val dprodE = thm "dprodE"; 

889 
val dsum_In0I = thm "dsum_In0I"; 

890 
val dsum_In1I = thm "dsum_In1I"; 

891 
val dsumE = thm "dsumE"; 

892 
val dprod_mono = thm "dprod_mono"; 

893 
val dsum_mono = thm "dsum_mono"; 

894 
val dprod_Sigma = thm "dprod_Sigma"; 

895 
val dprod_subset_Sigma = thm "dprod_subset_Sigma"; 

896 
val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2"; 

897 
val dsum_Sigma = thm "dsum_Sigma"; 

898 
val dsum_subset_Sigma = thm "dsum_subset_Sigma"; 

899 
val Domain_dprod = thm "Domain_dprod"; 

900 
val Domain_dsum = thm "Domain_dsum"; 

901 
*} 

902 

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

903 
end 