equal
deleted
inserted
replaced
48 Goal "bt_rec(Lf,c,h) = c"; |
48 Goal "bt_rec(Lf,c,h) = c"; |
49 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
49 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
50 by (Simp_tac 1); |
50 by (Simp_tac 1); |
51 qed "bt_rec_Lf"; |
51 qed "bt_rec_Lf"; |
52 |
52 |
53 Goal |
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 "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))"; |
|
55 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
54 by (rtac (bt_rec_def RS def_Vrec RS trans) 1); |
56 by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1); |
55 by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1); |
57 qed "bt_rec_Br"; |
56 qed "bt_rec_Br"; |
58 |
57 |
59 Addsimps [bt_rec_Lf, bt_rec_Br]; |
58 Addsimps [bt_rec_Lf, bt_rec_Br]; |