HOL-Theorem-Prover
Amjad style lazy theorems
As per Hasan Amjad’s TPHOLs’05 paper. These could be used interactively at the level of calls to prove and store_thm, with worker thread(s) spawned to handle proofs in the background. I think the extra assumptions needed to make the theorem valid should be a transient constant defined to be equal to the desired goal. The VALID tactical could then ignore extra assumptions that looked like such constants so that previously proved theorems could be used in subsequent tactics.
To make this work you need to explicitly pass what Isabelle would call the proof context to the tactic that solves the goal. In HOL, this context would include (at least) the grammar, the simplifier state and (ideally) the computeLib state. These are all things that later code in the same script file might change and which will affect the behaviour of the tactics. This requires a scary change to the fundamental type of tactic, though if you make the type take the context last, existing tactic definitions that are defined purely with combinators or by examining the standard g as (asl,w) parameter might not need changing.
Do Amjad lazy theorems differ from Boulton lazy theorems? I vaguely recall that the latter was based on a different type of theorems in the kernel.
I been wondering whether contexts can be emulated with PolyML.NameSpaces
- Amjad theorems don’t require a kernel change.
- The contexts are a dynamic thing; I don’t see how PolyML namespaces would help
If there are type variables in the goal (quite plausibly), the constant standing in for the game will need to take type variable parameters (most easily using the itself type), and tools instantiating such theorems will have to not balk at such hypotheses appearing and contaminating the goal state.