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.

Tobias




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