author | paulson |
Wed, 06 Jan 1999 13:24:33 +0100 | |
changeset 6065 | 3b4a29166f26 |
parent 6046 | 2c8a8be36c94 |
child 6112 | 5e4871c5136b |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/BT.ML |
0 | 2 |
ID: $Id$ |
1461 | 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 |
||
6046 | 9 |
Addsimps bt.intrs; |
10 |
||
0 | 11 |
(** Lemmas to justify using "bt" in other recursive type definitions **) |
12 |
||
5137 | 13 |
Goalw bt.defs "A<=B ==> bt(A) <= bt(B)"; |
0 | 14 |
by (rtac lfp_mono 1); |
515 | 15 |
by (REPEAT (rtac bt.bnd_mono 1)); |
0 | 16 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
17 |
qed "bt_mono"; |
0 | 18 |
|
5068 | 19 |
Goalw (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)"; |
0 | 20 |
by (rtac lfp_lowerbound 1); |
21 |
by (rtac (A_subset_univ RS univ_mono) 2); |
|
4091 | 22 |
by (fast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
1461 | 23 |
Pair_in_univ]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
24 |
qed "bt_univ"; |
0 | 25 |
|
6046 | 26 |
bind_thm ("bt_subset_univ", [bt_mono, bt_univ] MRS subset_trans); |
515 | 27 |
|
2469 | 28 |
|
515 | 29 |
(*Type checking -- proved by induction, as usual*) |
6065 | 30 |
val major::prems = goal BT.thy |
515 | 31 |
"[| t: bt(A); \ |
32 |
\ c: C(Lf); \ |
|
33 |
\ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \ |
|
1461 | 34 |
\ h(x,y,z,r,s): C(Br(x,y,z)) \ |
6046 | 35 |
\ |] ==> bt_rec(c,h,t) : C(t)"; |
6065 | 36 |
(*instead of induct_tac "t", since t: bt(A) isn't an assumption*) |
37 |
by (rtac (major RS bt.induct) 1); |
|
4091 | 38 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
760 | 39 |
qed "bt_rec_type"; |
515 | 40 |
|
41 |
(** n_nodes **) |
|
42 |
||
6046 | 43 |
Goal "t: bt(A) ==> n_nodes(t) : nat"; |
6065 | 44 |
by (induct_tac "t" 1); |
6046 | 45 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
46 |
qed "n_nodes_type"; |
515 | 47 |
|
48 |
||
49 |
(** n_leaves **) |
|
50 |
||
6046 | 51 |
Goal "t: bt(A) ==> n_leaves(t) : nat"; |
6065 | 52 |
by (induct_tac "t" 1); |
6046 | 53 |
by Auto_tac; |
760 | 54 |
qed "n_leaves_type"; |
515 | 55 |
|
56 |
(** bt_reflect **) |
|
57 |
||
6046 | 58 |
Goal "t: bt(A) ==> bt_reflect(t) : bt(A)"; |
6065 | 59 |
by (induct_tac "t" 1); |
6046 | 60 |
by Auto_tac; |
515 | 61 |
by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
62 |
qed "bt_reflect_type"; |
515 | 63 |
|
64 |
||
65 |
(** BT simplification **) |
|
66 |
||
67 |
||
6046 | 68 |
Addsimps [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type]; |
515 | 69 |
|
70 |
||
71 |
(*** theorems about n_leaves ***) |
|
72 |
||
6065 | 73 |
Goal "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"; |
74 |
by (induct_tac "t" 1); |
|
4091 | 75 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute, n_leaves_type]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
76 |
qed "n_leaves_reflect"; |
515 | 77 |
|
6065 | 78 |
Goal "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))"; |
79 |
by (induct_tac "t" 1); |
|
4091 | 80 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_succ_right]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
81 |
qed "n_leaves_nodes"; |
515 | 82 |
|
83 |
(*** theorems about bt_reflect ***) |
|
84 |
||
6065 | 85 |
Goal "t: bt(A) ==> bt_reflect(bt_reflect(t))=t"; |
86 |
by (induct_tac "t" 1); |
|
2469 | 87 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
88 |
qed "bt_reflect_bt_reflect_ident"; |
515 | 89 |
|
90 |