[isabelle] Getting a fact with attributes from ML



Hi,

I have a string s such as "refl[of x]" and would like to write an ML function that parses this string and returns the corresponding theorem (the same theorem that, e.g., the thm command would show, in this case "x=x").

Note: the string is not known at compile time, so the antiquotation @{thm refl[of x]} is not what I need. Also, Thm.infer_instantiate is not what I need because use of "of" is just an example. I want to be able to use any attribute, e.g., OF, simplified, abs_def, ...

(Proof_Context.get_fact ctxt (Facts.named s) would work if there were no attributes, but not with attributes.)

I tried the following:

   ML ‹
   val toks = Token.explode0 (Thy_Header.get_keywords' \<^context>)
   "refl[of x]"
   val (parsed,leftover) = Scan.catch Parse.thm toks (* [of x] is not
   parsed (stays in leftover) *)
   val fact = Attrib.eval_thms \<^context> [parsed] (* Gives me
   "?t=?t", not "x=x" *)
   ›

But this does not give me the correct result (see the comments in the ML source).

What would be the correct approach be?

(Background: I need this for my qrhl-tool <https://github.com/dominique-unruh/qrhl-tool>. The user can specify the names of facts on the qrhl-tool side, and the fact is retrieved via libisabelle from Isabelle.)

Best wishes,
Dominique.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.