From 433010c92cd86bcaaa57896b8516382f7a5f4bb2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 29 Aug 2000 15:31:19 +0000 Subject: Example file grabbed from twelf distrib --- twelf/example.elf | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 twelf/example.elf (limited to 'twelf') 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. -- cgit v1.2.3