[isabelle-dev] Referring to unfolded chained facts

[Jasmin Blanchette]

Hi all,

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"
    proof -
      assume "null xs"
      show "tl xs = xs"
        using `null xs`
        unfolding null_def
        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).

Hence:

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?

Thanks,

Jasmin