[isabelle] Problems with proof terms


I’m currently trying to do some experiments using proof terms in Isabelle,
but I’m having some difficulty getting it to work. I’m working in the
HOL-Proofs heap. To illustrate, if I have the simple lemma:

theory ProofTermTest

imports Main


  lemma t: "A ∧ B --> A"

    apply (rule impI)

   apply (elim conjE)

   apply assumption



   prf t

   full_prf t

gives the error message “reconstruct_proof: minimal proof object”.

I also had a go at the ML level, but


  val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of @{thm

  Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);


only prints `?’.

Does anyone have any experience working with proof terms and if so, can you
point out where I’m going wrong?


Colin Farquhar

PhD Student

Dependable Systems Group

School of Mathematical and Computer Sciences

Heriot-Watt University

Sunday Times Scottish University of the Year 2011-2013
Top in the UK for student experience
Fourth university in the UK and top in Scotland (National Student Survey 2012)

We invite research leaders and ambitious early career researchers to 
join us in leading and driving research in key inter-disciplinary themes. 
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.