[isabelle] Problems with proof terms



Hi,



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

begin

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

    apply (rule impI)

   apply (elim conjE)

   apply assumption

  done



Then

   prf t

   full_prf t



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



I also had a go at the ML level, but



ML{*

  val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of @{thm
"t"};));

  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?




Thanks,



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.