From: Alex Meyer <alex153@outlook.lv>

Hello!

I am trying to combine knowledge from Isabelle/Isar implementation manual, Isabelle code and from QHRL tool https://github.com/dominique-unruh/qrhl-tool .

My aim is to programmatically initiate the proof (open goals) and make (importing and using the Scala objects from qrhl tool) one proof step for theorem.

What I already know:

/1. I can start with the theorem as inner syntax string and convert it into Isabelle term with Scala code from scala-isabelle/qrhl-tool:

val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

val thm = Thm(ctxt, "effect_swapI") //this reads the theorem by name from theory file

val term = Term(ctxt, "x+0 = (y::nat)*1") //this constructs the Term on-the-fly from the string

/2. I understand that the result of single proof stem I can read from the TopLevel.state which has goal objects. I the proof has open goals/subgoals, then this TopLevel.state.goal has object and this object contains the term (in inner syntax) of the statement that should be proved to close that subgoal.

In qrhl-tool such single step is achieved by the code (can be template):

val tl = toplevel()

tl.execCmd("qrhl {top} skip; ~ skip; {top}")

val st = tl.state.applyTactic(CaseTac("y", tl.state.parseExpression(GIsabelle.boolT, "x1")))

//print(st.goal)

assert(st.goal.length==1)

val pre = st.goal.head.asInstanceOf[QRHLSubgoal].pre

assert(pre.toString == "ℭ𝔩𝔞[x1 = y] ⊓ ⊤")

pre.checkWelltyped(tl.state.isabelle, GIsabelle.predicateT)

This code receives the "theorem" (in the qrhl syntax that is some layer over Isabelle - I have read the relevant parts of manual and papers that describe qrhl-tool) "qrhl {top} skip; ~ skip; {top}" and by toplevel.execCmd initiates the proof procedure which generated toplevel.state.goal and that is why toplevel.state.applyTactic and to called to make single proof step.

But here I have questions:

1) Conceptual question: how to issue Isar theorem/lemma command and start proog process? How to generate goals in the toplevel.state? qrhl-tool suggests that I can call topLevel.execCmd with the theorem string/term and thats it! But the actual Toplevel.thy code from pure/isar have not procedures that can accept string/term/theorem as argument and start proof procedure. So - how can I conceptually (from the Isabelle thy, ml point of view) start proof process?

2) Practical question: My question 1) showed that there is no direct parallel between pure/isar/topevel.thy and qrhl-tool.toplevel: qrhl-tool.toplevel can start proof process from string, but there is not such procedure for isar/toplevel. Above mentioned code works for quantum Hoare Logic language, but my practical question is - does qrhl-tool contain code with similara functionality that receives the inner-syntax Isabelle string and initiated the proof process?

I am currently goind thought qrhl-tool code and seeking such capability. As I understand then qrhl language statements are translated into Isabelle statement and so - down the road - there is qrhl-tool Scala code that starts the proof process for the generic Isabelle statement (in inner syntax), but I am still seeking such code. Any suggestion where to find one are welcome. Thanks.

Well - I am a bit afraid (there is such possibility that I have misunderstood something) that there may not be the qrhl-tool Scala code for starting proof process or making proof step for Isabelle inner statement terms or for scala-isabelle terms. In such case - my question is: what it would take to write such code? Is it hard to do? Or maybe there are some prohibitively large roadblocks ahead of such effort?

So - I am just trying to programmatically (from Scala) construct term, initiate proof on such term, issue proof commands on such term (e.g. tactics) and read the generated goals/subgoals and issue proof comands on them and deteced when no goals are remained. I am trying to do this with qrhl-tool, seems to be designed exactly for that.

Thanks,

Alex

Last updated: Jul 15 2022 at 23:21 UTC