Email Gateway (Apr 28 2021 at 22:43): Email Gateway (Apr 28 2021 at 22:43):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: Apr 19 2024 at 12:27 UTC