author | clasohm |
Fri, 15 Jul 1994 13:34:31 +0200 | |
changeset 477 | 53fc8ad84b33 |
parent 445 | 7b6d8b8d4580 |
child 515 | abcc438e7c27 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/ex/bt.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Datatype definition of binary trees |
|
7 |
*) |
|
8 |
||
9 |
structure BT = Datatype_Fun |
|
10 |
(val thy = Univ.thy; |
|
477 | 11 |
val thy_name = "BT"; |
0 | 12 |
val rec_specs = |
13 |
[("bt", "univ(A)", |
|
445 | 14 |
[(["Lf"],"i",NoSyn), |
15 |
(["Br"],"[i,i,i]=>i", NoSyn)])]; |
|
0 | 16 |
val rec_styp = "i=>i"; |
17 |
val sintrs = |
|
18 |
["Lf : bt(A)", |
|
19 |
"[| a: A; t1: bt(A); t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"]; |
|
20 |
val monos = []; |
|
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
56
diff
changeset
|
21 |
val type_intrs = datatype_intrs |
0 | 22 |
val type_elims = []); |
23 |
||
24 |
val [LfI, BrI] = BT.intrs; |
|
25 |
||
26 |
(*Perform induction on l, then prove the major premise using prems. *) |
|
27 |
fun bt_ind_tac a prems i = |
|
28 |
EVERY [res_inst_tac [("x",a)] BT.induct i, |
|
29 |
rename_last_tac a ["1","2"] (i+2), |
|
30 |
ares_tac prems i]; |
|
31 |
||
32 |
||
33 |
(** Lemmas to justify using "bt" in other recursive type definitions **) |
|
34 |
||
35 |
goalw BT.thy BT.defs "!!A B. A<=B ==> bt(A) <= bt(B)"; |
|
36 |
by (rtac lfp_mono 1); |
|
37 |
by (REPEAT (rtac BT.bnd_mono 1)); |
|
38 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
|
39 |
val bt_mono = result(); |
|
40 |
||
41 |
goalw BT.thy (BT.defs@BT.con_defs) "bt(univ(A)) <= univ(A)"; |
|
42 |
by (rtac lfp_lowerbound 1); |
|
43 |
by (rtac (A_subset_univ RS univ_mono) 2); |
|
44 |
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
|
45 |
Pair_in_univ]) 1); |
|
46 |
val bt_univ = result(); |
|
47 |
||
56 | 48 |
val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans); |
0 | 49 |