Re: [isabelle] Dealing with mod and lists

Dear Aaron,

it would have helped a lot to describe what you want to achieve with sv2vl. I guess that sv2vl denotes the prefix of length n of the list that always repeats the list ls, i.e., sv2vl 5 [1, 2] = [1, 2, 1, 2, 1]. If this is the case, you can simplify your definition a bit, which makes proofs easier:

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

Both definitions are equivalent because "take n" cuts off any extra stuff that "replicate n" produces. Note that HOL has no notion of computation, so efficiency is not an issue here -- if you want to generate efficient code for it, you can still prove your definition as a code equation later on.

Your sv2vl_mod lemma requires the following lemma that is not yet present in Isabelle's List library:

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,

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 - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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