*To*: "Aaron W. Hsu" <arcfide at sacrideo.us>*Subject*: Re: [isabelle] Dealing with mod and lists*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Tue, 02 Oct 2012 08:53:13 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <op.wlingjj10p3ku8@localhost>*References*: <op.wlingjj10p3ku8@localhost>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Dear Aaron,

"sv2vl n ls == if ls = [] then (replicate n fill) else take n (concat (replicate n ls))"

lemma nth_concat_replicate: "i < n * length xs ==> concat (replicate n xs) ! i = xs ! (i mod length xs)" by(induct n arbitrary: i)(auto simp add: nth_append mod_geq) Then, your lemma can be proven automatically: lemma sv2vl_mod [simp]: "i < n & ls ~= [] ==> sv2vl n ls ! i = ls ! (i mod length ls)" by(auto simp add: sv2vl_def neq_Nil_conv nth_concat_replicate) Hope this helps, Andreas Am 01.10.2012 22:06, schrieb Aaron W. Hsu:

Dear Isabelle Users: I have been trying unsuccessfully for the past couple of days to get Isabelle to do my bidding when it comes to the following lemma and definition. I wonder if someone might be able to give me some hints on how to approach this. It seems like it ought to be a simple thing to prove, but I think my Isabelle skills are still too weak. definition sv2vl :: "nat ⇒ 'a list ⇒ 'a list" where "sv2vl n ls ≡ if ls = [] then (replicate n fill) else take n (concat (replicate (1 + n div length ls) ls))" lemma sv2vl_mod [simp]: "i < n ∧ ls ≠ [] ⟹ sv2vl n ls ! i = ls ! (i mod length ls)" by ??? I have been able to prove the following: lemma sv2vl_len [simp]: "length (sv2vl n ls) = n" but that required significantly more work than I would have thought it ought to. If someone could provide some assistance on these, I would appreciate it.

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] Dealing with mod and lists***From:*Aaron W. Hsu

- Previous by Date: [isabelle] Dealing with mod and lists
- Next by Date: [isabelle] UITP'12 Post-Proceedings - Call for Papers
- Previous by Thread: [isabelle] Dealing with mod and lists
- Next by Thread: [isabelle] UITP'12 Post-Proceedings - Call for Papers
- Cl-isabelle-users October 2012 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