[isabelle] attribute "simplified"

Dear all,

This is just an observation about the "simplified" attribute. Maybe it is well-known and its just me who wasn't aware of it.

Suppose I have a lemma like

  consts foo :: "'a list ⇒ 'b list ⇒ 'a list list"

  lemma foo:
    "i < length ys ==>
      foo xs ys ! i = take (ys ! i) (drop (listsum (take i ys)) xs)"

and now I want a special version for when "ys" is actually "map size ys". So I do

  thm foo [of _ "map size ys" for ys, simplified]

Now in the result the assumption "?i < length (map size ?ys2)" is simplified to "?i < length ?ys2". However, "map size ?ys2 ! ?i" is *not* simplified to "size (?ys2 ! i)" (which I expected in presence of "?i < length ?ys2").

Conclusion: The simplifier treats schematic variables in conditions differently than free variables (which is no surprise). Is there a way to obtain the result I expected without having to restate the whole lemma?



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