Example file grabbed from twelf distrib

1 files changed, 59 insertions, 0 deletions

diff --git a/twelf/example.elf b/twelf/example.elf
new file mode 100644
index 00000000..e52d5a06
--- /dev/null
+++ b/twelf/example.elf
@@ -0,0 +1,59 @@
+%%% 
+%%% Example script for Twelf Proof General.
+%%%
+%%% $Id$
+%%%
+
+
+%%% Intuitionistic propositional calculus
+%%% Positive fragment with implies, and, true.
+%%% Two formulations here: natural deduction and Hilbert-style system.
+%%% Author: Frank Pfenning
+
+% Type of propositions.
+o : type.
+%name o A.
+
+% Syntax: implication, plus a few constants.
+=> : o -> o -> o.  %infix right 10 =>.
+&  : o -> o -> o.  %infix right 11 &.
+true : o.
+
+% Provability.
+|- : o -> type.    %prefix 9 |-.
+%name |- P.
+
+% Axioms.
+K : |- A => B => A.
+S : |- (A => B => C) => (A => B) => A => C.
+ONE : |- true.
+PAIR : |- A => B => A & B.
+LEFT : |- A & B => A.
+RIGHT : |- A & B => B.
+
+% Inference Rule.
+MP : |- A => B -> |- A -> |- B. 
+
+% Natural Deduction.
+
+! : o -> type.   %prefix 9 !.
+%name ! D.
+
+trueI : ! true.
+andI  : ! A -> ! B -> ! A & B.
+andEL : ! A & B -> ! A.
+andER : ! A & B -> ! B.
+impliesI : (! A -> ! B) -> ! A => B.
+impliesE : ! A => B -> ! A -> ! B.
+
+% Normal deductions (for faster search)
+!^ : o -> type.
+!v : o -> type.
+
+trueI^ : !^ true.
+andI^ : !^ A -> !^ B -> !^ (A & B).
+andEvL : !v (A & B) -> !v A.
+andEvR : !v (A & B) -> !v B.
+impI^ : (!v A -> !^ B) -> !^ (A => B).
+impEv : !v (A => B) -> !^ A -> !v B.
+close : !v A -> !^ A.