Re: [isabelle] prove set (tl L) ⊆ set L



On 23.05.2013 18:46, Roger H. wrote:
> lemma "set (tl L) ⊆ set L"

Properties of functions defined by pattern matching can usually be
proved by induction. "tl" is not recursive, so case analysis suffices.
See the "induct" and "cases" methods.

  -- Lars




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