|
1 (* Title: ZF/bt.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For bt.thy. Binary trees |
|
7 *) |
|
8 |
|
9 open BT_Fn; |
|
10 |
|
11 |
|
12 |
|
13 (** bt_rec -- by Vset recursion **) |
|
14 |
|
15 (*Used to verify bt_rec*) |
|
16 val bt_rec_ss = ZF_ss |
|
17 addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")]) |
|
18 addrews BT.case_eqns; |
|
19 |
|
20 goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))"; |
|
21 by (SIMP_TAC rank_ss 1); |
|
22 val rank_Br1 = result(); |
|
23 |
|
24 goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))"; |
|
25 by (SIMP_TAC rank_ss 1); |
|
26 val rank_Br2 = result(); |
|
27 |
|
28 goal BT_Fn.thy "bt_rec(Lf,c,h) = c"; |
|
29 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
|
30 by (SIMP_TAC bt_rec_ss 1); |
|
31 val bt_rec_Lf = result(); |
|
32 |
|
33 goal BT_Fn.thy |
|
34 "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))"; |
|
35 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
|
36 by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1); |
|
37 val bt_rec_Br = result(); |
|
38 |
|
39 (*Type checking -- proved by induction, as usual*) |
|
40 val prems = goal BT_Fn.thy |
|
41 "[| t: bt(A); \ |
|
42 \ c: C(Lf); \ |
|
43 \ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \ |
|
44 \ h(x,y,z,r,s): C(Br(x,y,z)) \ |
|
45 \ |] ==> bt_rec(t,c,h) : C(t)"; |
|
46 by (bt_ind_tac "t" prems 1); |
|
47 by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews |
|
48 (prems@[bt_rec_Lf,bt_rec_Br])))); |
|
49 val bt_rec_type = result(); |
|
50 |
|
51 (** Versions for use with definitions **) |
|
52 |
|
53 val [rew] = goal BT_Fn.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c"; |
|
54 by (rewtac rew); |
|
55 by (rtac bt_rec_Lf 1); |
|
56 val def_bt_rec_Lf = result(); |
|
57 |
|
58 val [rew] = goal BT_Fn.thy |
|
59 "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))"; |
|
60 by (rewtac rew); |
|
61 by (rtac bt_rec_Br 1); |
|
62 val def_bt_rec_Br = result(); |
|
63 |
|
64 fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]); |
|
65 |
|
66 (** n_nodes **) |
|
67 |
|
68 val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def; |
|
69 |
|
70 val prems = goalw BT_Fn.thy [n_nodes_def] |
|
71 "xs: bt(A) ==> n_nodes(xs) : nat"; |
|
72 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1)); |
|
73 val n_nodes_type = result(); |
|
74 |
|
75 |
|
76 (** n_leaves **) |
|
77 |
|
78 val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def; |
|
79 |
|
80 val prems = goalw BT_Fn.thy [n_leaves_def] |
|
81 "xs: bt(A) ==> n_leaves(xs) : nat"; |
|
82 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1)); |
|
83 val n_leaves_type = result(); |
|
84 |
|
85 (** bt_reflect **) |
|
86 |
|
87 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def; |
|
88 |
|
89 val prems = goalw BT_Fn.thy [bt_reflect_def] |
|
90 "xs: bt(A) ==> bt_reflect(xs) : bt(A)"; |
|
91 by (REPEAT (ares_tac (prems @ [bt_rec_type, LfI, BrI]) 1)); |
|
92 val bt_reflect_type = result(); |
|
93 |
|
94 |
|
95 (** BT_Fn simplification **) |
|
96 |
|
97 |
|
98 val bt_typechecks = |
|
99 [LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type]; |
|
100 |
|
101 val bt_congs = |
|
102 BT.congs @ |
|
103 mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"]; |
|
104 |
|
105 val bt_ss = arith_ss |
|
106 addcongs bt_congs |
|
107 addrews BT.case_eqns |
|
108 addrews bt_typechecks |
|
109 addrews [bt_rec_Lf, bt_rec_Br, |
|
110 n_nodes_Lf, n_nodes_Br, |
|
111 n_leaves_Lf, n_leaves_Br, |
|
112 bt_reflect_Lf, bt_reflect_Br]; |
|
113 |
|
114 |
|
115 (*** theorems about n_leaves ***) |
|
116 |
|
117 val prems = goal BT_Fn.thy |
|
118 "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"; |
|
119 by (bt_ind_tac "t" prems 1); |
|
120 by (ALLGOALS (ASM_SIMP_TAC bt_ss)); |
|
121 by (REPEAT (ares_tac [add_commute, n_leaves_type] 1)); |
|
122 val n_leaves_reflect = result(); |
|
123 |
|
124 val prems = goal BT_Fn.thy |
|
125 "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))"; |
|
126 by (bt_ind_tac "t" prems 1); |
|
127 by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right]))); |
|
128 val n_leaves_nodes = result(); |
|
129 |
|
130 (*** theorems about bt_reflect ***) |
|
131 |
|
132 val prems = goal BT_Fn.thy |
|
133 "t: bt(A) ==> bt_reflect(bt_reflect(t))=t"; |
|
134 by (bt_ind_tac "t" prems 1); |
|
135 by (ALLGOALS (ASM_SIMP_TAC bt_ss)); |
|
136 val bt_reflect_bt_reflect_ident = result(); |
|
137 |
|
138 |