[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
We support two new methods how to give proofs: Annotated proofs and proof terms. Annotated proofs are Tutch proofs in which each line is annotated by a proof term. Since proof terms record all information necessary to reconstruct a proof, they alone (without a deduction tree) are sufficient as well. For the syntax see the section Proof Terms in the A. Reference. Here are two examples, annotating proofs from the last chapter.
% prop0-ann.tut % Modus ponens annotated proof mp: A & (A=>B) => B = begin [ x : A & (A=>B); fst x : A; snd x : A=>B; (snd x) (fst x) : B ]; fn x => (snd x) (fst x) : A & (A=>B) => B end; |
% prop3-ann.tut % Classical implication definition ~A|B => A=>B annotated proof classImpDef : ~A|B => A=>B = begin [ x : ~A|B; [ a : A; [ na : ~A; na a : F; abort (na a) : B ]; [ b : B; b : B ]; case x of inl na => abort (na a) | inr b => b end : B ]; fn a => case x of inl na => abort (na a) | inr b => b end : A=>B ]; fn x => fn a => case x of inl na => abort (na a) | inr b => b end : ~A|B => A=>B end; term classImpDef : ~A|B => A=>B = fn x => fn a => case x of inl na => abort (na a) | inr b => b end; |
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |