summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Statespace/DistinctTreeProver.thy

author | wenzelm |

Sun Nov 06 14:09:24 2011 +0100 (2011-11-06) | |

changeset 45355 | c0704e988526 |

parent 44890 | 22f665a2e91c |

child 45358 | 4849133d7a78 |

permissions | -rw-r--r-- |

misc tuning and modernization;

1 (* Title: HOL/Statespace/DistinctTreeProver.thy

2 Author: Norbert Schirmer, TU Muenchen

3 *)

5 header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}

7 theory DistinctTreeProver

8 imports Main

9 uses ("distinct_tree_prover.ML")

10 begin

12 text {* A state space manages a set of (abstract) names and assumes

13 that the names are distinct. The names are stored as parameters of a

14 locale and distinctness as an assumption. The most common request is

15 to proof distinctness of two given names. We maintain the names in a

16 balanced binary tree and formulate a predicate that all nodes in the

17 tree have distinct names. This setup leads to logarithmic certificates.

18 *}

20 subsection {* The Binary Tree *}

22 datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip

25 text {* The boolean flag in the node marks the content of the node as

26 deleted, without having to build a new tree. We prefer the boolean

27 flag to an option type, so that the ML-layer can still use the node

28 content to facilitate binary search in the tree. The ML code keeps the

29 nodes sorted using the term order. We do not have to push ordering to

30 the HOL level. *}

32 subsection {* Distinctness of Nodes *}

35 primrec set_of :: "'a tree \<Rightarrow> 'a set"

36 where

37 "set_of Tip = {}"

38 | "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"

40 primrec all_distinct :: "'a tree \<Rightarrow> bool"

41 where

42 "all_distinct Tip = True"

43 | "all_distinct (Node l x d r) =

44 ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and>

45 set_of l \<inter> set_of r = {} \<and>

46 all_distinct l \<and> all_distinct r)"

48 text {* Given a binary tree @{term "t"} for which

49 @{const all_distinct} holds, given two different nodes contained in the tree,

50 we want to write a ML function that generates a logarithmic

51 certificate that the content of the nodes is distinct. We use the

52 following lemmas to achieve this. *}

54 lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"

55 by simp

57 lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"

58 by simp

60 lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y"

61 by auto

63 lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y"

64 by auto

66 lemma distinct_left_right: "\<lbrakk>all_distinct (Node l z b r); x \<in> set_of l; y \<in> set_of r\<rbrakk>

67 \<Longrightarrow> x\<noteq>y"

68 by auto

70 lemma in_set_root: "x \<in> set_of (Node l x False r)"

71 by simp

73 lemma in_set_left: "y \<in> set_of l \<Longrightarrow> y \<in> set_of (Node l x False r)"

74 by simp

76 lemma in_set_right: "y \<in> set_of r \<Longrightarrow> y \<in> set_of (Node l x False r)"

77 by simp

79 lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x"

80 by blast

82 lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False"

83 by simp

85 subsection {* Containment of Trees *}

87 text {* When deriving a state space from other ones, we create a new

88 name tree which contains all the names of the parent state spaces and

89 assumme the predicate @{const all_distinct}. We then prove that the new locale

90 interprets all parent locales. Hence we have to show that the new

91 distinctness assumption on all names implies the distinctness

92 assumptions of the parent locales. This proof is implemented in ML. We

93 do this efficiently by defining a kind of containment check of trees

94 by 'subtraction'. We subtract the parent tree from the new tree. If this

95 succeeds we know that @{const all_distinct} of the new tree implies

96 @{const all_distinct} of the parent tree. The resulting certificate is

97 of the order @{term "n * log(m)"} where @{term "n"} is the size of the

98 (smaller) parent tree and @{term "m"} the size of the (bigger) new tree.

99 *}

102 primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"

103 where

104 "delete x Tip = None"

105 | "delete x (Node l y d r) = (case delete x l of

106 Some l' \<Rightarrow>

107 (case delete x r of

108 Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')

109 | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))

110 | None \<Rightarrow>

111 (case (delete x r) of

112 Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')

113 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)

114 else None))"

117 lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"

118 proof (induct t)

119 case Tip thus ?case by simp

120 next

121 case (Node l y d r)

122 have del: "delete x (Node l y d r) = Some t'" by fact

123 show ?case

124 proof (cases "delete x l")

125 case (Some l')

126 note x_l_Some = this

127 with Node.hyps

128 have l'_l: "set_of l' \<subseteq> set_of l"

129 by simp

130 show ?thesis

131 proof (cases "delete x r")

132 case (Some r')

133 with Node.hyps

134 have "set_of r' \<subseteq> set_of r"

135 by simp

136 with l'_l Some x_l_Some del

137 show ?thesis

138 by (auto split: split_if_asm)

139 next

140 case None

141 with l'_l Some x_l_Some del

142 show ?thesis

143 by (fastforce split: split_if_asm)

144 qed

145 next

146 case None

147 note x_l_None = this

148 show ?thesis

149 proof (cases "delete x r")

150 case (Some r')

151 with Node.hyps

152 have "set_of r' \<subseteq> set_of r"

153 by simp

154 with Some x_l_None del

155 show ?thesis

156 by (fastforce split: split_if_asm)

157 next

158 case None

159 with x_l_None del

160 show ?thesis

161 by (fastforce split: split_if_asm)

162 qed

163 qed

164 qed

166 lemma delete_Some_all_distinct:

167 "\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"

168 proof (induct t)

169 case Tip thus ?case by simp

170 next

171 case (Node l y d r)

172 have del: "delete x (Node l y d r) = Some t'" by fact

173 have "all_distinct (Node l y d r)" by fact

174 then obtain

175 dist_l: "all_distinct l" and

176 dist_r: "all_distinct r" and

177 d: "d \<or> (y \<notin> set_of l \<and> y \<notin> set_of r)" and

178 dist_l_r: "set_of l \<inter> set_of r = {}"

179 by auto

180 show ?case

181 proof (cases "delete x l")

182 case (Some l')

183 note x_l_Some = this

184 from Node.hyps (1) [OF Some dist_l]

185 have dist_l': "all_distinct l'"

186 by simp

187 from delete_Some_set_of [OF x_l_Some]

188 have l'_l: "set_of l' \<subseteq> set_of l".

189 show ?thesis

190 proof (cases "delete x r")

191 case (Some r')

192 from Node.hyps (2) [OF Some dist_r]

193 have dist_r': "all_distinct r'"

194 by simp

195 from delete_Some_set_of [OF Some]

196 have "set_of r' \<subseteq> set_of r".

198 with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r

199 show ?thesis

200 by fastforce

201 next

202 case None

203 with l'_l dist_l' x_l_Some del d dist_l_r dist_r

204 show ?thesis

205 by fastforce

206 qed

207 next

208 case None

209 note x_l_None = this

210 show ?thesis

211 proof (cases "delete x r")

212 case (Some r')

213 with Node.hyps (2) [OF Some dist_r]

214 have dist_r': "all_distinct r'"

215 by simp

216 from delete_Some_set_of [OF Some]

217 have "set_of r' \<subseteq> set_of r".

218 with Some dist_r' x_l_None del dist_l d dist_l_r

219 show ?thesis

220 by fastforce

221 next

222 case None

223 with x_l_None del dist_l dist_r d dist_l_r

224 show ?thesis

225 by (fastforce split: split_if_asm)

226 qed

227 qed

228 qed

230 lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"

231 proof (induct t)

232 case Tip thus ?case by simp

233 next

234 case (Node l y d r)

235 thus ?case

236 by (auto split: option.splits)

237 qed

239 lemma delete_Some_x_set_of:

240 "\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"

241 proof (induct t)

242 case Tip thus ?case by simp

243 next

244 case (Node l y d r)

245 have del: "delete x (Node l y d r) = Some t'" by fact

246 show ?case

247 proof (cases "delete x l")

248 case (Some l')

249 note x_l_Some = this

250 from Node.hyps (1) [OF Some]

251 obtain x_l: "x \<in> set_of l" "x \<notin> set_of l'"

252 by simp

253 show ?thesis

254 proof (cases "delete x r")

255 case (Some r')

256 from Node.hyps (2) [OF Some]

257 obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"

258 by simp

259 from x_r x_l Some x_l_Some del

260 show ?thesis

261 by (clarsimp split: split_if_asm)

262 next

263 case None

264 then have "x \<notin> set_of r"

265 by (simp add: delete_None_set_of_conv)

266 with x_l None x_l_Some del

267 show ?thesis

268 by (clarsimp split: split_if_asm)

269 qed

270 next

271 case None

272 note x_l_None = this

273 then have x_notin_l: "x \<notin> set_of l"

274 by (simp add: delete_None_set_of_conv)

275 show ?thesis

276 proof (cases "delete x r")

277 case (Some r')

278 from Node.hyps (2) [OF Some]

279 obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"

280 by simp

281 from x_r x_notin_l Some x_l_None del

282 show ?thesis

283 by (clarsimp split: split_if_asm)

284 next

285 case None

286 then have "x \<notin> set_of r"

287 by (simp add: delete_None_set_of_conv)

288 with None x_l_None x_notin_l del

289 show ?thesis

290 by (clarsimp split: split_if_asm)

291 qed

292 qed

293 qed

296 primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"

297 where

298 "subtract Tip t = Some t"

299 | "subtract (Node l x b r) t =

300 (case delete x t of

301 Some t' \<Rightarrow> (case subtract l t' of

302 Some t'' \<Rightarrow> subtract r t''

303 | None \<Rightarrow> None)

304 | None \<Rightarrow> None)"

306 lemma subtract_Some_set_of_res:

307 "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"

308 proof (induct t\<^isub>1)

309 case Tip thus ?case by simp

310 next

311 case (Node l x b r)

312 have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact

313 show ?case

314 proof (cases "delete x t\<^isub>2")

315 case (Some t\<^isub>2')

316 note del_x_Some = this

317 from delete_Some_set_of [OF Some]

318 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

319 show ?thesis

320 proof (cases "subtract l t\<^isub>2'")

321 case (Some t\<^isub>2'')

322 note sub_l_Some = this

323 from Node.hyps (1) [OF Some]

324 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

325 show ?thesis

326 proof (cases "subtract r t\<^isub>2''")

327 case (Some t\<^isub>2''')

328 from Node.hyps (2) [OF Some ]

329 have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .

330 with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2

331 show ?thesis

332 by simp

333 next

334 case None

335 with del_x_Some sub_l_Some sub

336 show ?thesis

337 by simp

338 qed

339 next

340 case None

341 with del_x_Some sub

342 show ?thesis

343 by simp

344 qed

345 next

346 case None

347 with sub show ?thesis by simp

348 qed

349 qed

351 lemma subtract_Some_set_of:

352 "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2"

353 proof (induct t\<^isub>1)

354 case Tip thus ?case by simp

355 next

356 case (Node l x d r)

357 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

358 show ?case

359 proof (cases "delete x t\<^isub>2")

360 case (Some t\<^isub>2')

361 note del_x_Some = this

362 from delete_Some_set_of [OF Some]

363 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

364 from delete_None_set_of_conv [of x t\<^isub>2] Some

365 have x_t2: "x \<in> set_of t\<^isub>2"

366 by simp

367 show ?thesis

368 proof (cases "subtract l t\<^isub>2'")

369 case (Some t\<^isub>2'')

370 note sub_l_Some = this

371 from Node.hyps (1) [OF Some]

372 have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .

373 from subtract_Some_set_of_res [OF Some]

374 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

375 show ?thesis

376 proof (cases "subtract r t\<^isub>2''")

377 case (Some t\<^isub>2''')

378 from Node.hyps (2) [OF Some ]

379 have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .

380 from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2

381 show ?thesis

382 by auto

383 next

384 case None

385 with del_x_Some sub_l_Some sub

386 show ?thesis

387 by simp

388 qed

389 next

390 case None

391 with del_x_Some sub

392 show ?thesis

393 by simp

394 qed

395 next

396 case None

397 with sub show ?thesis by simp

398 qed

399 qed

401 lemma subtract_Some_all_distinct_res:

402 "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t"

403 proof (induct t\<^isub>1)

404 case Tip thus ?case by simp

405 next

406 case (Node l x d r)

407 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

408 have dist_t2: "all_distinct t\<^isub>2" by fact

409 show ?case

410 proof (cases "delete x t\<^isub>2")

411 case (Some t\<^isub>2')

412 note del_x_Some = this

413 from delete_Some_all_distinct [OF Some dist_t2]

414 have dist_t2': "all_distinct t\<^isub>2'" .

415 show ?thesis

416 proof (cases "subtract l t\<^isub>2'")

417 case (Some t\<^isub>2'')

418 note sub_l_Some = this

419 from Node.hyps (1) [OF Some dist_t2']

420 have dist_t2'': "all_distinct t\<^isub>2''" .

421 show ?thesis

422 proof (cases "subtract r t\<^isub>2''")

423 case (Some t\<^isub>2''')

424 from Node.hyps (2) [OF Some dist_t2'']

425 have dist_t2''': "all_distinct t\<^isub>2'''" .

426 from Some sub_l_Some del_x_Some sub

427 dist_t2'''

428 show ?thesis

429 by simp

430 next

431 case None

432 with del_x_Some sub_l_Some sub

433 show ?thesis

434 by simp

435 qed

436 next

437 case None

438 with del_x_Some sub

439 show ?thesis

440 by simp

441 qed

442 next

443 case None

444 with sub show ?thesis by simp

445 qed

446 qed

449 lemma subtract_Some_dist_res:

450 "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"

451 proof (induct t\<^isub>1)

452 case Tip thus ?case by simp

453 next

454 case (Node l x d r)

455 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

456 show ?case

457 proof (cases "delete x t\<^isub>2")

458 case (Some t\<^isub>2')

459 note del_x_Some = this

460 from delete_Some_x_set_of [OF Some]

461 obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"

462 by simp

463 from delete_Some_set_of [OF Some]

464 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

465 show ?thesis

466 proof (cases "subtract l t\<^isub>2'")

467 case (Some t\<^isub>2'')

468 note sub_l_Some = this

469 from Node.hyps (1) [OF Some ]

470 have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".

471 from subtract_Some_set_of_res [OF Some]

472 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

473 show ?thesis

474 proof (cases "subtract r t\<^isub>2''")

475 case (Some t\<^isub>2''')

476 from Node.hyps (2) [OF Some]

477 have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .

478 from subtract_Some_set_of_res [OF Some]

479 have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".

481 from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''

482 t2''_t2' t2'_t2 x_not_t2'

483 show ?thesis

484 by auto

485 next

486 case None

487 with del_x_Some sub_l_Some sub

488 show ?thesis

489 by simp

490 qed

491 next

492 case None

493 with del_x_Some sub

494 show ?thesis

495 by simp

496 qed

497 next

498 case None

499 with sub show ?thesis by simp

500 qed

501 qed

503 lemma subtract_Some_all_distinct:

504 "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t\<^isub>1"

505 proof (induct t\<^isub>1)

506 case Tip thus ?case by simp

507 next

508 case (Node l x d r)

509 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

510 have dist_t2: "all_distinct t\<^isub>2" by fact

511 show ?case

512 proof (cases "delete x t\<^isub>2")

513 case (Some t\<^isub>2')

514 note del_x_Some = this

515 from delete_Some_all_distinct [OF Some dist_t2 ]

516 have dist_t2': "all_distinct t\<^isub>2'" .

517 from delete_Some_set_of [OF Some]

518 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

519 from delete_Some_x_set_of [OF Some]

520 obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"

521 by simp

523 show ?thesis

524 proof (cases "subtract l t\<^isub>2'")

525 case (Some t\<^isub>2'')

526 note sub_l_Some = this

527 from Node.hyps (1) [OF Some dist_t2' ]

528 have dist_l: "all_distinct l" .

529 from subtract_Some_all_distinct_res [OF Some dist_t2']

530 have dist_t2'': "all_distinct t\<^isub>2''" .

531 from subtract_Some_set_of [OF Some]

532 have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .

533 from subtract_Some_set_of_res [OF Some]

534 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

535 from subtract_Some_dist_res [OF Some]

536 have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".

537 show ?thesis

538 proof (cases "subtract r t\<^isub>2''")

539 case (Some t\<^isub>2''')

540 from Node.hyps (2) [OF Some dist_t2'']

541 have dist_r: "all_distinct r" .

542 from subtract_Some_set_of [OF Some]

543 have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .

544 from subtract_Some_dist_res [OF Some]

545 have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".

547 from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2'

548 t2''_t2' dist_l_t2'' dist_r_t2'''

549 show ?thesis

550 by auto

551 next

552 case None

553 with del_x_Some sub_l_Some sub

554 show ?thesis

555 by simp

556 qed

557 next

558 case None

559 with del_x_Some sub

560 show ?thesis

561 by simp

562 qed

563 next

564 case None

565 with sub show ?thesis by simp

566 qed

567 qed

570 lemma delete_left:

571 assumes dist: "all_distinct (Node l y d r)"

572 assumes del_l: "delete x l = Some l'"

573 shows "delete x (Node l y d r) = Some (Node l' y d r)"

574 proof -

575 from delete_Some_x_set_of [OF del_l]

576 obtain "x \<in> set_of l"

577 by simp

578 moreover with dist

579 have "delete x r = None"

580 by (cases "delete x r") (auto dest:delete_Some_x_set_of)

582 ultimately

583 show ?thesis

584 using del_l dist

585 by (auto split: option.splits)

586 qed

588 lemma delete_right:

589 assumes dist: "all_distinct (Node l y d r)"

590 assumes del_r: "delete x r = Some r'"

591 shows "delete x (Node l y d r) = Some (Node l y d r')"

592 proof -

593 from delete_Some_x_set_of [OF del_r]

594 obtain "x \<in> set_of r"

595 by simp

596 moreover with dist

597 have "delete x l = None"

598 by (cases "delete x l") (auto dest:delete_Some_x_set_of)

600 ultimately

601 show ?thesis

602 using del_r dist

603 by (auto split: option.splits)

604 qed

606 lemma delete_root:

607 assumes dist: "all_distinct (Node l x False r)"

608 shows "delete x (Node l x False r) = Some (Node l x True r)"

609 proof -

610 from dist have "delete x r = None"

611 by (cases "delete x r") (auto dest:delete_Some_x_set_of)

612 moreover

613 from dist have "delete x l = None"

614 by (cases "delete x l") (auto dest:delete_Some_x_set_of)

615 ultimately show ?thesis

616 using dist

617 by (auto split: option.splits)

618 qed

620 lemma subtract_Node:

621 assumes del: "delete x t = Some t'"

622 assumes sub_l: "subtract l t' = Some t''"

623 assumes sub_r: "subtract r t'' = Some t'''"

624 shows "subtract (Node l x False r) t = Some t'''"

625 using del sub_l sub_r

626 by simp

628 lemma subtract_Tip: "subtract Tip t = Some t"

629 by simp

631 text {* Now we have all the theorems in place that are needed for the

632 certificate generating ML functions. *}

634 use "distinct_tree_prover.ML"

636 (* Uncomment for profiling or debugging *)

637 (*

638 ML {*

639 (*

640 val nums = (0 upto 10000);

641 val nums' = (200 upto 3000);

642 *)

643 val nums = (0 upto 10000);

644 val nums' = (0 upto 3000);

645 val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums

647 val consts = sort Term_Ord.fast_term_ord

648 (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)

649 val consts' = sort Term_Ord.fast_term_ord

650 (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')

652 val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts

655 val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'

658 val dist =

659 HOLogic.Trueprop$

660 (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)

662 val dist' =

663 HOLogic.Trueprop$

664 (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')

666 val da = Unsynchronized.ref refl;

668 *}

670 setup {*

671 Theory.add_consts_i const_decls

672 #> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy

673 in (da := thm; thy') end)

674 *}

677 ML {*

678 val ct' = cterm_of @{theory} t';

679 *}

681 ML {*

682 timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);()))

683 *}

685 (* 590 s *)

687 ML {*

690 val p1 =

691 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)

692 val p2 =

693 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)

694 *}

697 ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )

698 p1

699 p2)*}

702 ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}

707 ML {*

708 val cdist' = cterm_of @{theory} dist';

709 DistinctTreeProver.distinct_implProver (!da) cdist';

710 *}

712 *)

714 end