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