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 |