Stream: Isabelle/ML

Topic: how to instantiate a schematic variable of a theorem?

Jason Hu (Sep 16 2022 at 23:57):

In my tactic implementation, I would like to call resolve_tac on a fixed theorem, called mytheorem. However, I would like to first instantiate a schematic variable based on my previous computation. In vanilla Isabelle, I would have written mytheorem[of t]. How do I do it in ML when t is stored in a ML variable?

Mathias Fleury (Sep 17 2022 at 04:52):

Have you tried Drule.infer_instantiate or Drule.infer_instantiate'?

Mathias Fleury (Sep 17 2022 at 04:55):

For discovery purpose: I did not remember, so I grepped 'instantiate' on ~~src/HOL/Tools/SMT (but I am biased, because I have written some of the code there). If that had failed, I would have search for the type I expect on ~~src/Pure.

Jason Hu (Sep 19 2022 at 13:46):

ok thx for the trick.

Last updated: Apr 23 2024 at 16:19 UTC