Re: [isabelle] Addition to List?: rev_nonempty_induct

> I noticed that though there is "list_nonempty_induct" and "rev_induct",
> there is no variant for reverse induction on an nonempty list. Would
> this be worth adding (modulo renaming)?
> lemma rev_nonempty_induct[consumes 1, case_names single snoc]:
>   assumes ne: "xs ≠ []"
>   and single: "⋀x. P [x]"
>   and snoc': "⋀x xs. xs ≠ [] ⟹ P xs ⟹ P (xs at [x])"
>   shows "P xs"
>   using ne
>   proof (induct xs rule: rev_induct)
>     case (snoc x xs) thus ?case
>     proof (cases xs)
>       case Nil thus ?thesis by (simp add: single)
>     next
>       case Cons with snoc show ?thesis by (fastforce intro!: snoc')
>     qed
>   qed simp
> - René

I am personally in favour of it.  Further comments?



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.