equal
deleted
inserted
replaced
436 !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) |
436 !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) |
437 |] ==> P(l)" |
437 |] ==> P(l)" |
438 apply (subgoal_tac "P(rev(rev(l)))", simp) |
438 apply (subgoal_tac "P(rev(rev(l)))", simp) |
439 apply (erule rev_type [THEN list.induct], simp_all) |
439 apply (erule rev_type [THEN list.induct], simp_all) |
440 done |
440 done |
|
441 |
|
442 lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1] |
441 |
443 |
442 |
444 |
443 (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) |
445 (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) |
444 |
446 |
445 (** min FIXME: replace by Int! **) |
447 (** min FIXME: replace by Int! **) |