equal
deleted
inserted
replaced
57 by (simp_tac (ZF_ss addsimps List.case_eqns) 1); |
57 by (simp_tac (ZF_ss addsimps List.case_eqns) 1); |
58 val list_rec_Nil = result(); |
58 val list_rec_Nil = result(); |
59 |
59 |
60 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"; |
60 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"; |
61 by (rtac (list_rec_def RS def_Vrec RS trans) 1); |
61 by (rtac (list_rec_def RS def_Vrec RS trans) 1); |
62 by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1); |
62 by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1); |
63 val list_rec_Cons = result(); |
63 val list_rec_Cons = result(); |
64 |
64 |
65 (*Type checking -- proved by induction, as usual*) |
65 (*Type checking -- proved by induction, as usual*) |
66 val prems = goal ListFn.thy |
66 val prems = goal ListFn.thy |
67 "[| l: list(A); \ |
67 "[| l: list(A); \ |