[isabelle-dev] Backticks and schematic variables

[Jasmin Christian Blanchette]

Am 09.09.2010 um 16:58 schrieb Jasmin Christian Blanchette:

> I was wondering if there's a reason why facts with backticks can't contain schematic variables. For example,
> 
>    thm `?s = ?t ⟹ ?t = ?s`
> 
> gives
> 
>    *** Unbound schematic variable: ?s
>    *** At command "thm"
> 
> That theorem in particular has a name ("sym"), but when local or chained facts have no name and have schematic variables, this causes problems for Sledgehammer, since it needs to generate some Isar text to refer to the fact.

Johannes just gave me an answer: Apparently it's OK to meta-universal-quantify over the local facts I want to refer to when they are local facts. E.g.

    thm `⋀Z. anarchic Z ⟹ anarchic ({#any M, any (scan (drop M))#} + Z)`

retrieves

    anarchic ?Z ⟹ anarchic ({#any M, any (scan (drop M))#} + ?Z)

And `` is apparently not made for global facts, which is fine.

Jasmin