[isabelle] attribute "simplified"
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"
"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 <
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