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;
|
|
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 |
|