*To*: m.a.ellis at ncl.ac.uk*Subject*: Re: [isabelle] How does one reason about the subset of a list?*From*: nipkow at in.tum.de*Date*: Sun, 26 Feb 2006 11:24:16 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <200602260428.21163.m.a.ellis@ncl.ac.uk> (message from Martin Ellis on Sun, 26 Feb 2006 04:28:20 +0000)*References*: <19FD5FDFDE9BF64EADBECBD4B444BDDD061612@mucse307.eu.infineon.com> <200602260428.21163.m.a.ellis@ncl.ac.uk>

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) Tobias

**References**:**[isabelle] How does one reason about the subset of a list?***From:*Primrose.Mbanefo

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

- Previous by Date: Re: [isabelle] How does one reason about the subset of a list?
- Next by Date: Re: [isabelle] found it
- Previous by Thread: Re: [isabelle] How does one reason about the subset of a list?
- Next by Thread: Re: [isabelle] How does one reason about the subset of a list?
- Cl-isabelle-users February 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list