Re: [isabelle] Problems with proof terms



Hi Colin,

you must both
a) base your work in HOL-Proofs rather than HOL
b) and, at the beginning of your theory, tun proof recording on using

	ML_val {* proofs := 2 *}

See the section on proof terms in the (old) Isabelle reference manual
available by

	isabelle doc ref

Hope this helps,
	Florian

Am 26.04.2013 16:27, schrieb Colin Farquhar:
> 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.
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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