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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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