Re: [isabelle] Addition to List?: rev_nonempty_induct



>>> 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

I'll take a look after it.

	Florian

-- 

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.