--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Sequents.thy Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,147 @@
+(* Title: LK/lk.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Classical First-Order Sequent Calculus
+*)
+
+Sequents = Pure +
+
+types
+ o
+
+arities
+ o :: logic
+
+
+(* Sequences *)
+
+types
+ seq'
+
+consts
+ SeqO' :: "[o,seq']=>seq'"
+ Seq1' :: "o=>seq'"
+
+
+(* concrete syntax *)
+
+types
+ seq seqobj seqcont
+
+
+syntax
+ SeqEmp :: "seq" ("")
+ SeqApp :: "[seqobj,seqcont] => seq" ("__")
+
+ SeqContEmp :: "seqcont" ("")
+ SeqContApp :: "[seqobj,seqcont] => seqcont" (",/ __")
+
+ SeqO :: "o => seqobj" ("_")
+ SeqId :: "id => seqobj" ("$_")
+ SeqVar :: "var => seqobj" ("$_")
+
+types
+
+ single_seqe = "[seq,seqobj] => prop"
+ single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
+ two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
+ two_seqe = "[seq, seq] => prop"
+ three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ three_seqe = "[seq, seq, seq] => prop"
+ four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ four_seqe = "[seq, seq, seq, seq] => prop"
+
+end
+
+ML
+
+(* parse translation for sequences *)
+
+fun abs_seq' t = Abs("s", Type("seq'",[]), t);
+
+fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
+ seqobj_tr(_$i) = i;
+
+fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
+ seqcont_tr(Const("SeqContApp",_)$so$sc) =
+ (seqobj_tr so)$(seqcont_tr sc);
+
+fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
+ seq_tr(Const("SeqApp",_)$so$sc) =
+ abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
+
+
+fun singlobj_tr(Const("SeqO",_)$f) =
+ abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
+
+
+
+(* print translation for sequences *)
+
+fun seqcont_tr' (Bound 0) =
+ Const("SeqContEmp",dummyT) |
+ seqcont_tr' (Const("SeqO'",_)$f$s) =
+ Const("SeqContApp",dummyT)$
+ (Const("SeqO",dummyT)$f)$
+ (seqcont_tr' s) |
+(* seqcont_tr' ((a as Abs(_,_,_))$s)=
+ seqcont_tr'(betapply(a,s)) | *)
+ seqcont_tr' (i$s) =
+ Const("SeqContApp",dummyT)$
+ (Const("SeqId",dummyT)$i)$
+ (seqcont_tr' s);
+
+fun seq_tr' s =
+ let fun seq_itr' (Bound 0) =
+ Const("SeqEmp",dummyT) |
+ seq_itr' (Const("SeqO'",_)$f$s) =
+ Const("SeqApp",dummyT)$
+ (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
+(* seq_itr' ((a as Abs(_,_,_))$s) =
+ seq_itr'(betapply(a,s)) | *)
+ seq_itr' (i$s) =
+ Const("SeqApp",dummyT)$
+ (Const("SeqId",dummyT)$i)$
+ (seqcont_tr' s)
+ in case s of
+ Abs(_,_,t) => seq_itr' t |
+ _ => s$(Bound 0)
+ end;
+
+
+
+
+fun single_tr c [s1,s2] =
+ Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
+
+fun two_seq_tr c [s1,s2] =
+ Const(c,dummyT)$seq_tr s1$seq_tr s2;
+
+fun three_seq_tr c [s1,s2,s3] =
+ Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
+
+fun four_seq_tr c [s1,s2,s3,s4] =
+ Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
+
+
+fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
+ singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
+
+
+fun single_tr' c [s1, s2] =
+(Const (c, dummyT)$seq_tr' s1$seq_tr' s2 );
+
+
+fun two_seq_tr' c [s1, s2] =
+ Const (c, dummyT)$seq_tr' s1$seq_tr' s2;
+
+fun three_seq_tr' c [s1, s2, s3] =
+ Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3;
+
+fun four_seq_tr' c [s1, s2, s3, s4] =
+ Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4;
+
+
+