*To*: Colin Farquhar <cif30 at hw.ac.uk>*Subject*: Re: [isabelle] Extracting Goal Information from Proof Terms*From*: Makarius <makarius at sketis.net>*Date*: Tue, 23 Jun 2015 23:26:55 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <002801d08c99$70b6fdb0$5224f910$@hw.ac.uk>*References*: <002801d08c99$70b6fdb0$5224f910$@hw.ac.uk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 12 May 2015, Colin Farquhar wrote:

I?m currently working on something which requires proofs constructed inIsabelle to be translated into Prolog in order to work with a machinelearning tool. After some testing I have found that using proof terms isthe easiest way to find the structure of a proof and which tactics arebeing used and in which order, but I also need the details of the goalsthe tactics are applied to.

Using ?full_prf a? gives me the proof term, while using ?val pterm_a =Proofterm.Proof_of (Proofterm.strip_thm (Thm.proof_body_of @{thm a}))?gives a detailed description. The code I have written already provides alist of tactics in the order they are used, where each nested listcontains the tactic(s) applied to the subgoal(s) generated by theprevious tactic, eg. here the list would be [impI [conje [conjI[assumption,assumption]]]]. I?m trying to get something similar forgoals where each nested list contains the subgoal(s) generated byapplying a tactic to the previous goal ( eg. [A /\ B à B /\ A [A /\ B èB /\ A [ A è B è B /\ A [A è B è B, A è B è A]]]] ) which I can then mapto the list of tactics to get a list of (tactic, goal) pairs. Theproblem is, I can?t find a way to extract the details of the subgoals inthe middle of the proof. Is this even possible using proof terms in thisway? If so, can anyone help me with where I can find the information I?mlooking for?

I am not sure if you've got any further in this quest in the meantime.

(1) Proof terms are very expensive for anything but rather small applications of Isabelle/HOL. (2) Analyzing proof terms is relatively difficult, because most of the original resoning structure is lost; in particular, the original tactical goal state is no longer there, as you have already noticed.

Makarius

- Previous by Date: Re: [isabelle] How tactic fold instantiates variables
- Next by Date: Re: [isabelle] Sledgehammer 2015 oddity
- Previous by Thread: Re: [isabelle] How tactic fold instantiates variables
- Next by Thread: Re: [isabelle] Sledgehammer 2015 oddity
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list