[isabelle] Addition to List?: rev_nonempty_induct


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)
      case Cons with snoc show ?thesis by (fastforce intro!: snoc')
  qed simp

- René

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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