Re: [isabelle] How does one reason about the subset of a list?

Thanks for answering that one, Martin.

> (Is there an easier way to get the latter?)

Yes, induction is not needed because the relevant lemma about length and
list-updaate is already known:

lemma listswap_length2:
  "[| i< length xs; j < length xs |] ==> length (listswap xs i j) = length xs"
  by(simp add: listswap_def)


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