|
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; |
|
11 val rec_specs = |
|
12 [("bt", "univ(A)", |
|
13 [(["Lf"],"i"), (["Br"],"[i,i,i]=>i")])]; |
|
14 val rec_styp = "i=>i"; |
|
15 val ext = None |
|
16 val sintrs = |
|
17 ["Lf : bt(A)", |
|
18 "[| a: A; t1: bt(A); t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"]; |
|
19 val monos = []; |
|
20 val type_intrs = data_typechecks |
|
21 val type_elims = []); |
|
22 |
|
23 val [LfI, BrI] = BT.intrs; |
|
24 |
|
25 (*Perform induction on l, then prove the major premise using prems. *) |
|
26 fun bt_ind_tac a prems i = |
|
27 EVERY [res_inst_tac [("x",a)] BT.induct i, |
|
28 rename_last_tac a ["1","2"] (i+2), |
|
29 ares_tac prems i]; |
|
30 |
|
31 |
|
32 (** Lemmas to justify using "bt" in other recursive type definitions **) |
|
33 |
|
34 goalw BT.thy BT.defs "!!A B. A<=B ==> bt(A) <= bt(B)"; |
|
35 by (rtac lfp_mono 1); |
|
36 by (REPEAT (rtac BT.bnd_mono 1)); |
|
37 by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
|
38 val bt_mono = result(); |
|
39 |
|
40 goalw BT.thy (BT.defs@BT.con_defs) "bt(univ(A)) <= univ(A)"; |
|
41 by (rtac lfp_lowerbound 1); |
|
42 by (rtac (A_subset_univ RS univ_mono) 2); |
|
43 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
|
44 Pair_in_univ]) 1); |
|
45 val bt_univ = result(); |
|
46 |
|
47 val bt_subset_univ = standard (bt_mono RS (bt_univ RSN (2,subset_trans))); |
|
48 |
|
49 |