[isabelle-dev] Referring to unfolded chained facts
jasmin.blanchette at gmail.com
Thu Sep 1 12:30:55 CEST 2011
Isar generally lets users refer to unnamed local facts using the backtick notation. For example,
lemma "hd [x] = x"
using hd.simps[where xs = ""]
thm `!!x. hd [x] = x`
works fine. However, the same mechanism doesn't understand unfolding:
definition "null xs = (xs = )"
lemma "null xs ⟹ tl xs = xs"
assume "null xs"
show "tl xs = xs"
using `null xs`
thm `xs = ` -- FAILS
This is an issue in Sledgehammer. Sledgehammer and Metis obviously honor "unfolding", but sometimes they need to refer to the chained facts explicitly (e.g., if a structured Isar proof is generated).
1. Is the above behavior a bug or a feature?
2. If it's a feature, could we provide an alternative way of referring to chained facts, e.g. an auto-bound "chained" fact list, so that "chained(1)" would retrieve "xs = " in the above example?
3. If it's a bug, can we fix it?
More information about the isabelle-dev