515
|
1 |
(* Title: ZF/ex/BT.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
515
|
4 |
Copyright 1994 University of Cambridge
|
0
|
5 |
|
|
6 |
Datatype definition of binary trees
|
|
7 |
*)
|
|
8 |
|
515
|
9 |
open BT;
|
0
|
10 |
|
|
11 |
(*Perform induction on l, then prove the major premise using prems. *)
|
|
12 |
fun bt_ind_tac a prems i =
|
515
|
13 |
EVERY [res_inst_tac [("x",a)] bt.induct i,
|
0
|
14 |
rename_last_tac a ["1","2"] (i+2),
|
|
15 |
ares_tac prems i];
|
|
16 |
|
|
17 |
|
|
18 |
(** Lemmas to justify using "bt" in other recursive type definitions **)
|
|
19 |
|
515
|
20 |
goalw BT.thy bt.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
|
0
|
21 |
by (rtac lfp_mono 1);
|
515
|
22 |
by (REPEAT (rtac bt.bnd_mono 1));
|
0
|
23 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
|
|
24 |
val bt_mono = result();
|
|
25 |
|
515
|
26 |
goalw BT.thy (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)";
|
0
|
27 |
by (rtac lfp_lowerbound 1);
|
|
28 |
by (rtac (A_subset_univ RS univ_mono) 2);
|
|
29 |
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
|
|
30 |
Pair_in_univ]) 1);
|
|
31 |
val bt_univ = result();
|
|
32 |
|
56
|
33 |
val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
|
0
|
34 |
|
515
|
35 |
|
|
36 |
(** bt_rec -- by Vset recursion **)
|
|
37 |
|
|
38 |
goalw BT.thy bt.con_defs "rank(l) < rank(Br(a,l,r))";
|
|
39 |
by (simp_tac rank_ss 1);
|
|
40 |
val rank_Br1 = result();
|
|
41 |
|
|
42 |
goalw BT.thy bt.con_defs "rank(r) < rank(Br(a,l,r))";
|
|
43 |
by (simp_tac rank_ss 1);
|
|
44 |
val rank_Br2 = result();
|
|
45 |
|
|
46 |
goal BT.thy "bt_rec(Lf,c,h) = c";
|
|
47 |
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
|
|
48 |
by (simp_tac (ZF_ss addsimps bt.case_eqns) 1);
|
|
49 |
val bt_rec_Lf = result();
|
|
50 |
|
|
51 |
goal BT.thy
|
|
52 |
"bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
|
|
53 |
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
|
|
54 |
by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
|
|
55 |
val bt_rec_Br = result();
|
|
56 |
|
|
57 |
(*Type checking -- proved by induction, as usual*)
|
|
58 |
val prems = goal BT.thy
|
|
59 |
"[| t: bt(A); \
|
|
60 |
\ c: C(Lf); \
|
|
61 |
\ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \
|
|
62 |
\ h(x,y,z,r,s): C(Br(x,y,z)) \
|
|
63 |
\ |] ==> bt_rec(t,c,h) : C(t)";
|
|
64 |
by (bt_ind_tac "t" prems 1);
|
|
65 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
|
|
66 |
(prems@[bt_rec_Lf,bt_rec_Br]))));
|
|
67 |
val bt_rec_type = result();
|
|
68 |
|
|
69 |
(** Versions for use with definitions **)
|
|
70 |
|
|
71 |
val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
|
|
72 |
by (rewtac rew);
|
|
73 |
by (rtac bt_rec_Lf 1);
|
|
74 |
val def_bt_rec_Lf = result();
|
|
75 |
|
|
76 |
val [rew] = goal BT.thy
|
|
77 |
"[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
|
|
78 |
by (rewtac rew);
|
|
79 |
by (rtac bt_rec_Br 1);
|
|
80 |
val def_bt_rec_Br = result();
|
|
81 |
|
|
82 |
fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
|
|
83 |
|
|
84 |
(** n_nodes **)
|
|
85 |
|
|
86 |
val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
|
|
87 |
|
|
88 |
val prems = goalw BT.thy [n_nodes_def]
|
|
89 |
"xs: bt(A) ==> n_nodes(xs) : nat";
|
|
90 |
by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
|
|
91 |
val n_nodes_type = result();
|
|
92 |
|
|
93 |
|
|
94 |
(** n_leaves **)
|
|
95 |
|
|
96 |
val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
|
|
97 |
|
|
98 |
val prems = goalw BT.thy [n_leaves_def]
|
|
99 |
"xs: bt(A) ==> n_leaves(xs) : nat";
|
|
100 |
by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
|
|
101 |
val n_leaves_type = result();
|
|
102 |
|
|
103 |
(** bt_reflect **)
|
|
104 |
|
|
105 |
val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
|
|
106 |
|
|
107 |
goalw BT.thy [bt_reflect_def] "!!xs. xs: bt(A) ==> bt_reflect(xs) : bt(A)";
|
|
108 |
by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
|
|
109 |
val bt_reflect_type = result();
|
|
110 |
|
|
111 |
|
|
112 |
(** BT simplification **)
|
|
113 |
|
|
114 |
|
|
115 |
val bt_typechecks =
|
|
116 |
bt.intrs @ [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
|
|
117 |
|
|
118 |
val bt_ss = arith_ss
|
|
119 |
addsimps bt.case_eqns
|
|
120 |
addsimps bt_typechecks
|
|
121 |
addsimps [bt_rec_Lf, bt_rec_Br,
|
|
122 |
n_nodes_Lf, n_nodes_Br,
|
|
123 |
n_leaves_Lf, n_leaves_Br,
|
|
124 |
bt_reflect_Lf, bt_reflect_Br];
|
|
125 |
|
|
126 |
|
|
127 |
(*** theorems about n_leaves ***)
|
|
128 |
|
|
129 |
val prems = goal BT.thy
|
|
130 |
"t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
|
|
131 |
by (bt_ind_tac "t" prems 1);
|
|
132 |
by (ALLGOALS (asm_simp_tac bt_ss));
|
|
133 |
by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
|
|
134 |
val n_leaves_reflect = result();
|
|
135 |
|
|
136 |
val prems = goal BT.thy
|
|
137 |
"t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
|
|
138 |
by (bt_ind_tac "t" prems 1);
|
|
139 |
by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
|
|
140 |
val n_leaves_nodes = result();
|
|
141 |
|
|
142 |
(*** theorems about bt_reflect ***)
|
|
143 |
|
|
144 |
val prems = goal BT.thy
|
|
145 |
"t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
|
|
146 |
by (bt_ind_tac "t" prems 1);
|
|
147 |
by (ALLGOALS (asm_simp_tac bt_ss));
|
|
148 |
val bt_reflect_bt_reflect_ident = result();
|
|
149 |
|
|
150 |
|