Re: [isabelle] Addition to List?: rev_nonempty_induct
On 11/07/2014 13:38, Florian Haftmann wrote:
>> 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?
I am happy to see it go in.
This archive was generated by a fusion of
Pipermail (Mailman edition) and