src/ZF/ListFn.ML
changeset 26 5aa9c39b480d
parent 15 6c6d2f6e3185
equal deleted inserted replaced
25:3ac1c0c0016e 26:5aa9c39b480d
    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);    \