author  wenzelm 
Fri, 12 Oct 2012 18:58:20 +0200  
changeset 49834  b27bbb021df1 
parent 48891  c0eafbd55de3 
child 54398  100c0eaf63d5 
permissions  rwrr 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Datatype.thy 
20819  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
11954  3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

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

5 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

6 
header {* Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *} 
11954  7 

15131  8 
theory Datatype 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

9 
imports Product_Type Sum_Type Nat 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
45694
diff
changeset

10 
keywords "datatype" :: thy_decl 
15131  11 
begin 
11954  12 

33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

13 
subsection {* The datatype universe *} 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

14 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

15 
definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

16 

49834  17 
typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

18 
morphisms Rep_Node Abs_Node 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

19 
unfolding Node_def by auto 
20819  20 

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

22 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41505
diff
changeset

23 
type_synonym 'a item = "('a, unit) node set" 
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41505
diff
changeset

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

26 
consts 

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 
Push_def: "Push == (%b h. nat_case b h)" 

60 

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

62 

63 
(*Sexpression constructors*) 

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

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

66 

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

68 
Leaf_def: "Leaf == Atom o Inl" 

69 
Numb_def: "Numb == Atom o Inr" 

70 

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

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

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

74 

75 
(*Function spaces*) 

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

77 

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

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

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

81 

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

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

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

85 

86 
(*the corresponding eliminators*) 

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

88 

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

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

91 

92 

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

94 

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

96 

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

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

99 

100 

101 

102 
lemma apfst_convE: 

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

104 
] ==> R" 

105 
by (force simp add: apfst_def) 

106 

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

108 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

110 
apply (simp add: Push_def fun_eq_iff) 
20819  111 
apply (drule_tac x=0 in spec, simp) 
112 
done 

113 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

115 
apply (auto simp add: Push_def fun_eq_iff) 
20819  116 
apply (drule_tac x="Suc x" in spec, simp) 
117 
done 

118 

119 
lemma Push_inject: 

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

121 
by (blast dest: Push_inject1 Push_inject2) 

122 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

124 
by (auto simp add: Push_def fun_eq_iff split: nat.split_asm) 
20819  125 

45607  126 
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1] 
20819  127 

128 

129 
(*** Introduction rules for Node ***) 

130 

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

132 
by (simp add: Node_def) 

133 

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

135 
apply (simp add: Node_def Push_def) 

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

137 
done 

138 

139 

140 
subsection{*Freeness: Distinctness of Constructors*} 

141 

142 
(** Scons vs Atom **) 

143 

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

35216  145 
unfolding Atom_def Scons_def Push_Node_def One_nat_def 
146 
by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 

20819  147 
dest!: Abs_Node_inj 
148 
elim!: apfst_convE sym [THEN Push_neq_K0]) 

149 

45607  150 
lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym] 
21407  151 

20819  152 

153 
(*** Injectiveness ***) 

154 

155 
(** Atomic nodes **) 

156 

157 
lemma inj_Atom: "inj(Atom)" 

158 
apply (simp add: Atom_def) 

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

160 
done 

45607  161 
lemmas Atom_inject = inj_Atom [THEN injD] 
20819  162 

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

164 
by (blast dest!: Atom_inject) 

165 

166 
lemma inj_Leaf: "inj(Leaf)" 

167 
apply (simp add: Leaf_def o_def) 

168 
apply (rule inj_onI) 

169 
apply (erule Atom_inject [THEN Inl_inject]) 

170 
done 

171 

45607  172 
lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD] 
20819  173 

174 
lemma inj_Numb: "inj(Numb)" 

175 
apply (simp add: Numb_def o_def) 

176 
apply (rule inj_onI) 

177 
apply (erule Atom_inject [THEN Inr_inject]) 

178 
done 

179 

45607  180 
lemmas Numb_inject [dest!] = inj_Numb [THEN injD] 
20819  181 

182 

183 
(** Injectiveness of Push_Node **) 

184 

185 
lemma Push_Node_inject: 

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

187 
] ==> P" 

188 
apply (simp add: Push_Node_def) 

189 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

190 
apply (rule Rep_Node [THEN Node_Push_I])+ 

191 
apply (erule sym [THEN apfst_convE]) 

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

193 
done 

194 

195 

196 
(** Injectiveness of Scons **) 

197 

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

35216  199 
unfolding Scons_def One_nat_def 
200 
by (blast dest!: Push_Node_inject) 

20819  201 

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

35216  203 
unfolding Scons_def One_nat_def 
204 
by (blast dest!: Push_Node_inject) 

20819  205 

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

207 
apply (erule equalityE) 

208 
apply (iprover intro: equalityI Scons_inject_lemma1) 

209 
done 

210 

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

212 
apply (erule equalityE) 

213 
apply (iprover intro: equalityI Scons_inject_lemma2) 

214 
done 

215 

216 
lemma Scons_inject: 

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

218 
by (iprover dest: Scons_inject1 Scons_inject2) 

219 

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

221 
by (blast elim!: Scons_inject) 

222 

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

224 

225 
(** Scons vs Leaf **) 

226 

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

35216  228 
unfolding Leaf_def o_def by (rule Scons_not_Atom) 
20819  229 

45607  230 
lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym] 
20819  231 

232 
(** Scons vs Numb **) 

233 

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

35216  235 
unfolding Numb_def o_def by (rule Scons_not_Atom) 
20819  236 

45607  237 
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym] 
20819  238 

239 

240 
(** Leaf vs Numb **) 

241 

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

243 
by (simp add: Leaf_def Numb_def) 

244 

45607  245 
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym] 
20819  246 

247 

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

249 

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

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

252 

253 
lemma ndepth_Push_Node_aux: 

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

255 
apply (induct_tac "k", auto) 

256 
apply (erule Least_le) 

257 
done 

258 

259 
lemma ndepth_Push_Node: 

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

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

262 
apply (auto simp add: ndepth_def Push_Node_def 

263 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

264 
apply (rule Least_equality) 

265 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

266 
apply (erule LeastI) 

267 
done 

268 

269 

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

271 

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

273 
by (simp add: ntrunc_def) 

274 

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

276 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

277 

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

35216  279 
unfolding Leaf_def o_def by (rule ntrunc_Atom) 
20819  280 

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

35216  282 
unfolding Numb_def o_def by (rule ntrunc_Atom) 
20819  283 

284 
lemma ntrunc_Scons [simp]: 

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

35216  286 
unfolding Scons_def ntrunc_def One_nat_def 
287 
by (auto simp add: ndepth_Push_Node) 

20819  288 

289 

290 

291 
(** Injection nodes **) 

292 

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

294 
apply (simp add: In0_def) 

295 
apply (simp add: Scons_def) 

296 
done 

297 

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

299 
by (simp add: In0_def) 

300 

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

302 
apply (simp add: In1_def) 

303 
apply (simp add: Scons_def) 

304 
done 

305 

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

307 
by (simp add: In1_def) 

308 

309 

310 
subsection{*Set Constructions*} 

311 

312 

313 
(*** Cartesian Product ***) 

314 

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

316 
by (simp add: uprod_def) 

317 

318 
(*The general elimination rule*) 

319 
lemma uprodE [elim!]: 

320 
"[ c : uprod A B; 

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

322 
] ==> P" 

323 
by (auto simp add: uprod_def) 

324 

325 

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

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

328 
by (auto simp add: uprod_def) 

329 

330 

331 
(*** Disjoint Sum ***) 

332 

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

334 
by (simp add: usum_def) 

335 

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

337 
by (simp add: usum_def) 

338 

339 
lemma usumE [elim!]: 

340 
"[ u : usum A B; 

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

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

343 
] ==> P" 

344 
by (auto simp add: usum_def) 

345 

346 

347 
(** Injection **) 

348 

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

35216  350 
unfolding In0_def In1_def One_nat_def by auto 
20819  351 

45607  352 
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym] 
20819  353 

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

355 
by (simp add: In0_def) 

356 

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

358 
by (simp add: In1_def) 

359 

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

361 
by (blast dest!: In0_inject) 

362 

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

364 
by (blast dest!: In1_inject) 

365 

366 
lemma inj_In0: "inj In0" 

367 
by (blast intro!: inj_onI) 

368 

369 
lemma inj_In1: "inj In1" 

370 
by (blast intro!: inj_onI) 

371 

372 

373 
(*** Function spaces ***) 

374 

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

376 
apply (simp add: Lim_def) 

377 
apply (rule ext) 

378 
apply (blast elim!: Push_Node_inject) 

379 
done 

380 

381 

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

383 

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

385 
by (auto simp add: ntrunc_def) 

386 

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

388 
by (auto simp add: ntrunc_def) 

389 

390 
(*A generalized form of the takelemma*) 

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

392 
apply (rule equalityI) 

393 
apply (rule_tac [!] ntrunc_subsetD) 

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

395 
done 

396 

397 
lemma ntrunc_o_equality: 

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

399 
apply (rule ntrunc_equality [THEN ext]) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

400 
apply (simp add: fun_eq_iff) 
20819  401 
done 
402 

403 

404 
(*** Monotonicity ***) 

405 

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

407 
by (simp add: uprod_def, blast) 

408 

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

410 
by (simp add: usum_def, blast) 

411 

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

413 
by (simp add: Scons_def, blast) 

414 

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

35216  416 
by (simp add: In0_def Scons_mono) 
20819  417 

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

35216  419 
by (simp add: In1_def Scons_mono) 
20819  420 

421 

422 
(*** Split and Case ***) 

423 

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

425 
by (simp add: Split_def) 

426 

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

428 
by (simp add: Case_def) 

429 

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

431 
by (simp add: Case_def) 

432 

433 

434 

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

436 

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

438 
by (simp add: ntrunc_def, blast) 

439 

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

441 
by (simp add: Scons_def, blast) 

442 

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

444 
by (simp add: Scons_def, blast) 

445 

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

447 
by (simp add: In0_def Scons_UN1_y) 

448 

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

450 
by (simp add: In1_def Scons_UN1_y) 

451 

452 

453 
(*** Equality for Cartesian Product ***) 

454 

455 
lemma dprodI [intro!]: 

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

457 
by (auto simp add: dprod_def) 

458 

459 
(*The general elimination rule*) 

460 
lemma dprodE [elim!]: 

461 
"[ c : dprod r s; 

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

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

464 
] ==> P" 

465 
by (auto simp add: dprod_def) 

466 

467 

468 
(*** Equality for Disjoint Sum ***) 

469 

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

471 
by (auto simp add: dsum_def) 

472 

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

474 
by (auto simp add: dsum_def) 

475 

476 
lemma dsumE [elim!]: 

477 
"[ w : dsum r s; 

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

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

480 
] ==> P" 

481 
by (auto simp add: dsum_def) 

482 

483 

484 
(*** Monotonicity ***) 

485 

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

487 
by blast 

488 

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

490 
by blast 

491 

492 

493 
(*** Bounding theorems ***) 

494 

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

496 
by blast 

497 

45607  498 
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma] 
20819  499 

500 
(*Dependent version*) 

501 
lemma dprod_subset_Sigma2: 

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

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

504 
by auto 

505 

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

507 
by blast 

508 

45607  509 
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma] 
20819  510 

511 

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

512 
text {* hides popular names *} 
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35216
diff
changeset

513 
hide_type (open) node item 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35216
diff
changeset

514 
hide_const (open) Push Node Atom Leaf Numb Lim Split Case 
20819  515 

48891  516 
ML_file "Tools/Datatype/datatype.ML" 
12918  517 

48891  518 
ML_file "Tools/inductive_realizer.ML" 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

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

520 

48891  521 
ML_file "Tools/Datatype/datatype_realizer.ML" 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

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

523 

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

524 
end 
47488
be6dd389639d
centralized enriched_type declaration, thanks to insitu available Isar commands
haftmann
parents:
46950
diff
changeset

525 