Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Antiquotation for Theorem Names

Email Gateway (Aug 18 2022 at 14:58):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi!

In the meantime I modified my antiquotation function as follows

fun output_names [name] = [Pretty.str name]
| output_names [n1, n2] = [Pretty.str n1, Pretty.str " and ",
Pretty.str n2]
| output_names names =
let val (ns, n) = split_last (map Pretty.str names) in
Pretty.commas ns @ [Pretty.str ", and ", n]
end

fun output_thm_names
({context = ctxt, ...} : {state : Toplevel.state, source : Args.src,
context: Proof.context})
names =
let
val _ = map (PureThy.get_fact (Context.Proof ctxt)
(ProofContext.theory_of ctxt) o Facts.named) names
in
ThyOutput.output [Pretty.block (output_names names)]
end

This works in principle (for single names). E.g.,

lemma bla: ...

text {* @{lemmas bla} *}

produces "bla" in the resulting pdf. However, this does not work for
'local facts'. E.g.,

...
case (Suc n)
txt {* @{lemmas Suc} *}

results in the error: *** Unknown fact "Suc"

Is it impossible to refer to 'local facts' in antiquotations?

cheers

chris

Email Gateway (Aug 18 2022 at 14:58):

From: Alexander Krauss <krauss@in.tum.de>
Hi Chris,

In the meantime I modified my antiquotation function as follows

[...]

let
val _ = map (PureThy.get_fact (Context.Proof ctxt)
(ProofContext.theory_of ctxt) o Facts.named) names

this only takes the facts from the theory. Did you try something like
ProofContext.get_fact(s) / .get_thm(s) ?

Alex

Last updated: Apr 24 2024 at 16:18 UTC