changeset 760 | f0200e91b272 |
parent 515 | abcc438e7c27 |
child 782 | 200a16083201 |
759:e0b172d01c37 | 760:f0200e91b272 |
---|---|
44 val rank_Br2 = result(); |
44 val rank_Br2 = result(); |
45 |
45 |
46 goal BT.thy "bt_rec(Lf,c,h) = c"; |
46 goal BT.thy "bt_rec(Lf,c,h) = c"; |
47 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
47 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
48 by (simp_tac (ZF_ss addsimps bt.case_eqns) 1); |
48 by (simp_tac (ZF_ss addsimps bt.case_eqns) 1); |
49 val bt_rec_Lf = result(); |
49 qed "bt_rec_Lf"; |
50 |
50 |
51 goal BT.thy |
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))"; |
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); |
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); |
54 by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1); |
55 val bt_rec_Br = result(); |
55 qed "bt_rec_Br"; |
56 |
56 |
57 (*Type checking -- proved by induction, as usual*) |
57 (*Type checking -- proved by induction, as usual*) |
58 val prems = goal BT.thy |
58 val prems = goal BT.thy |
59 "[| t: bt(A); \ |
59 "[| t: bt(A); \ |
60 \ c: C(Lf); \ |
60 \ c: C(Lf); \ |
62 \ h(x,y,z,r,s): C(Br(x,y,z)) \ |
62 \ h(x,y,z,r,s): C(Br(x,y,z)) \ |
63 \ |] ==> bt_rec(t,c,h) : C(t)"; |
63 \ |] ==> bt_rec(t,c,h) : C(t)"; |
64 by (bt_ind_tac "t" prems 1); |
64 by (bt_ind_tac "t" prems 1); |
65 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
65 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
66 (prems@[bt_rec_Lf,bt_rec_Br])))); |
66 (prems@[bt_rec_Lf,bt_rec_Br])))); |
67 val bt_rec_type = result(); |
67 qed "bt_rec_type"; |
68 |
68 |
69 (** Versions for use with definitions **) |
69 (** Versions for use with definitions **) |
70 |
70 |
71 val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c"; |
71 val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c"; |
72 by (rewtac rew); |
72 by (rewtac rew); |
96 val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def; |
96 val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def; |
97 |
97 |
98 val prems = goalw BT.thy [n_leaves_def] |
98 val prems = goalw BT.thy [n_leaves_def] |
99 "xs: bt(A) ==> n_leaves(xs) : nat"; |
99 "xs: bt(A) ==> n_leaves(xs) : nat"; |
100 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1)); |
100 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1)); |
101 val n_leaves_type = result(); |
101 qed "n_leaves_type"; |
102 |
102 |
103 (** bt_reflect **) |
103 (** bt_reflect **) |
104 |
104 |
105 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def; |
105 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def; |
106 |
106 |