Re: [isabelle] Addition to List?: rev_nonempty_induct



See now http://isabelle.in.tum.de/reports/Isabelle/rev/e848a17d9dee

	Florian

On 09.07.2014 12:02, René Neumann wrote:
> Hi,
> 
> 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é
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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