LIST_INDUCT_TAC : tactic
A ?- !l. P ===================================================== LIST_INDUCT_TAC A |- P[[]/l] A u {P[t/l]} ?- P[CONS h t/l]
# g `!l f:A->B g:B->C. MAP (g o f) l = MAP g (MAP f l)`;;
# e LIST_INDUCT_TAC;; val it : goalstack = 2 subgoals (2 total) 0 [`!f g. MAP (g o f) t = MAP g (MAP f t)`] `!f g. MAP (g o f) (CONS h t) = MAP g (MAP f (CONS h t))` `!f g. MAP (g o f) [] = MAP g (MAP f [])`
# e(ASM_REWRITE_TAC[MAP; o_THM]);;
# g `!l f:A->B g:B->C. MAP (g o f) l = MAP g (MAP f l)`;;
# e(MATCH_MP_TAC list_INDUCT);; val it : goalstack = 1 subgoal (1 total) `(!f g. MAP (g o f) [] = MAP g (MAP f [])) /\ (!a0 a1. (!f g. MAP (g o f) a1 = MAP g (MAP f a1)) ==> (!f g. MAP (g o f) (CONS a0 a1) = MAP g (MAP f (CONS a0 a1))))`
# e(REWRITE_TAC[MAP]);; val it : goalstack = 1 subgoal (1 total) `!a0 a1. (!f g. MAP (g o f) a1 = MAP g (MAP f a1)) ==> (!f g. CONS ((g o f) a0) (MAP (g o f) a1) = CONS (g (f a0)) (MAP g (MAP f a1)))`
# e(MAP_EVERY X_GEN_TAC [`k:A`; `l:A list`]);; val it : goalstack = 1 subgoal (1 total) `(!f g. MAP (g o f) l = MAP g (MAP f l)) ==> (!f g. CONS ((g o f) k) (MAP (g o f) l) = CONS (g (f k)) (MAP g (MAP f l)))`
# e(SIMP_TAC[o_THM]);; val it : goalstack = No subgoals