author | lcp |
Fri, 17 Sep 1993 16:52:10 +0200 | |
changeset 7 | 268f93ab3bc4 |
parent 0 | a5a9c433f639 |
child 29 | 4ec9b266ccd1 |
permissions | -rw-r--r-- |
0 | 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 |
goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))"; |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
16 |
by (simp_tac rank_ss 1); |
0 | 17 |
val rank_Br1 = result(); |
18 |
||
19 |
goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))"; |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
20 |
by (simp_tac rank_ss 1); |
0 | 21 |
val rank_Br2 = result(); |
22 |
||
23 |
goal BT_Fn.thy "bt_rec(Lf,c,h) = c"; |
|
24 |
by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
25 |
by (simp_tac (ZF_ss addsimps BT.case_eqns) 1); |
0 | 26 |
val bt_rec_Lf = result(); |
27 |
||
28 |
goal BT_Fn.thy |
|
29 |
"bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))"; |
|
30 |
by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
31 |
by (simp_tac (ZF_ss addsimps |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
32 |
(BT.case_eqns @ [Vset_rankI, rank_Br1, rank_Br2])) 1); |
0 | 33 |
val bt_rec_Br = result(); |
34 |
||
35 |
(*Type checking -- proved by induction, as usual*) |
|
36 |
val prems = goal BT_Fn.thy |
|
37 |
"[| t: bt(A); \ |
|
38 |
\ c: C(Lf); \ |
|
39 |
\ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \ |
|
40 |
\ h(x,y,z,r,s): C(Br(x,y,z)) \ |
|
41 |
\ |] ==> bt_rec(t,c,h) : C(t)"; |
|
42 |
by (bt_ind_tac "t" prems 1); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
43 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
0 | 44 |
(prems@[bt_rec_Lf,bt_rec_Br])))); |
45 |
val bt_rec_type = result(); |
|
46 |
||
47 |
(** Versions for use with definitions **) |
|
48 |
||
49 |
val [rew] = goal BT_Fn.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c"; |
|
50 |
by (rewtac rew); |
|
51 |
by (rtac bt_rec_Lf 1); |
|
52 |
val def_bt_rec_Lf = result(); |
|
53 |
||
54 |
val [rew] = goal BT_Fn.thy |
|
55 |
"[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))"; |
|
56 |
by (rewtac rew); |
|
57 |
by (rtac bt_rec_Br 1); |
|
58 |
val def_bt_rec_Br = result(); |
|
59 |
||
60 |
fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]); |
|
61 |
||
62 |
(** n_nodes **) |
|
63 |
||
64 |
val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def; |
|
65 |
||
66 |
val prems = goalw BT_Fn.thy [n_nodes_def] |
|
67 |
"xs: bt(A) ==> n_nodes(xs) : nat"; |
|
68 |
by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1)); |
|
69 |
val n_nodes_type = result(); |
|
70 |
||
71 |
||
72 |
(** n_leaves **) |
|
73 |
||
74 |
val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def; |
|
75 |
||
76 |
val prems = goalw BT_Fn.thy [n_leaves_def] |
|
77 |
"xs: bt(A) ==> n_leaves(xs) : nat"; |
|
78 |
by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1)); |
|
79 |
val n_leaves_type = result(); |
|
80 |
||
81 |
(** bt_reflect **) |
|
82 |
||
83 |
val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def; |
|
84 |
||
85 |
val prems = goalw BT_Fn.thy [bt_reflect_def] |
|
86 |
"xs: bt(A) ==> bt_reflect(xs) : bt(A)"; |
|
87 |
by (REPEAT (ares_tac (prems @ [bt_rec_type, LfI, BrI]) 1)); |
|
88 |
val bt_reflect_type = result(); |
|
89 |
||
90 |
||
91 |
(** BT_Fn simplification **) |
|
92 |
||
93 |
||
94 |
val bt_typechecks = |
|
95 |
[LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type]; |
|
96 |
||
97 |
val bt_ss = arith_ss |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
98 |
addsimps BT.case_eqns |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
99 |
addsimps bt_typechecks |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
100 |
addsimps [bt_rec_Lf, bt_rec_Br, |
0 | 101 |
n_nodes_Lf, n_nodes_Br, |
102 |
n_leaves_Lf, n_leaves_Br, |
|
103 |
bt_reflect_Lf, bt_reflect_Br]; |
|
104 |
||
105 |
||
106 |
(*** theorems about n_leaves ***) |
|
107 |
||
108 |
val prems = goal BT_Fn.thy |
|
109 |
"t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"; |
|
110 |
by (bt_ind_tac "t" prems 1); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
111 |
by (ALLGOALS (asm_simp_tac bt_ss)); |
0 | 112 |
by (REPEAT (ares_tac [add_commute, n_leaves_type] 1)); |
113 |
val n_leaves_reflect = result(); |
|
114 |
||
115 |
val prems = goal BT_Fn.thy |
|
116 |
"t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))"; |
|
117 |
by (bt_ind_tac "t" prems 1); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
118 |
by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right]))); |
0 | 119 |
val n_leaves_nodes = result(); |
120 |
||
121 |
(*** theorems about bt_reflect ***) |
|
122 |
||
123 |
val prems = goal BT_Fn.thy |
|
124 |
"t: bt(A) ==> bt_reflect(bt_reflect(t))=t"; |
|
125 |
by (bt_ind_tac "t" prems 1); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
126 |
by (ALLGOALS (asm_simp_tac bt_ss)); |
0 | 127 |
val bt_reflect_bt_reflect_ident = result(); |
128 |
||
129 |