src/ZF/list.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
equal deleted inserted replaced
5:75e163863e16 6:8ce8c4d13d4d
    60     "[| l: list(A);    \
    60     "[| l: list(A);    \
    61 \       c: C(0);       \
    61 \       c: C(0);       \
    62 \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
    62 \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
    63 \    |] ==> list_case(l,c,h) : C(l)";
    63 \    |] ==> list_case(l,c,h) : C(l)";
    64 by (rtac (major RS list_induct) 1);
    64 by (rtac (major RS list_induct) 1);
    65 by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
    65 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
    66 			    ([list_case_0,list_case_Pair]@prems))));
    66 			    ([list_case_0,list_case_Pair]@prems))));
    67 val list_case_type = result();
    67 val list_case_type = result();
    68 ****)
    68 ****)
    69 
    69 
    70 
    70 
    71 (** For recursion **)
    71 (** For recursion **)
    72 
    72 
    73 goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
    73 goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
    74 by (SIMP_TAC rank_ss 1);
    74 by (simp_tac rank_ss 1);
    75 val rank_Cons1 = result();
    75 val rank_Cons1 = result();
    76 
    76 
    77 goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
    77 goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
    78 by (SIMP_TAC rank_ss 1);
    78 by (simp_tac rank_ss 1);
    79 val rank_Cons2 = result();
    79 val rank_Cons2 = result();
    80 
    80