# HG changeset patch
# User paulson
# Date 837524661 -7200
# Node ID 9402e633fe53451686cb7b51c60e4e4243b4a03e
# Parent  74d4ae2f6fc3f76c4483faf87085e4d1a105784b
Tidied up; added "syntax" decl

diff -r 74d4ae2f6fc3 -r 9402e633fe53 src/LK/LK.thy
--- a/src/LK/LK.thy	Mon Jul 15 14:58:28 1996 +0200
+++ b/src/LK/LK.thy	Tue Jul 16 15:44:21 1996 +0200
@@ -4,6 +4,9 @@
     Copyright   1993  University of Cambridge
 
 Classical First-Order Sequent Calculus
+
+There may be printing problems if a seqent is in expanded normal form
+	(eta-expanded, beta-contracted)
 *)
 
 LK = Pure +
@@ -13,33 +16,35 @@
 default term
 
 types
- o sequence seqobj seqcont sobj
+  o sequence seqobj seqcont sobj
 
 arities
- o :: logic
+  o :: logic
 
 consts
- True,False     :: "o"
- "="            :: "['a,'a] => o"       (infixl 50)
- "Not"          :: "o => o"             ("~ _" [40] 40)
- "&"            :: "[o,o] => o"         (infixr 35)
- "|"            :: "[o,o] => o"         (infixr 30)
- "-->","<->"    :: "[o,o] => o"         (infixr 25)
- The            :: "('a => o) => 'a"    (binder "THE " 10)
- All            :: "('a => o) => o"     (binder "ALL " 10)
- Ex             :: "('a => o) => o"     (binder "EX " 10)
+  True,False   :: o
+  "="          :: ['a,'a] => o       (infixl 50)
+  Not          :: o => o             ("~ _" [40] 40)
+  "&"          :: [o,o] => o         (infixr 35)
+  "|"          :: [o,o] => o         (infixr 30)
+  "-->","<->"  :: [o,o] => o         (infixr 25)
+  The          :: ('a => o) => 'a    (binder "THE " 10)
+  All          :: ('a => o) => o     (binder "ALL " 10)
+  Ex           :: ('a => o) => o     (binder "EX " 10)
 
- (*Representation of sequents*)
- Trueprop       :: "[sobj=>sobj,sobj=>sobj] => prop"
- Seqof          :: "o => sobj=>sobj"
- "@Trueprop"    :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
- "@MtSeq"       :: "sequence"                           ("" [] 1000)
- "@NmtSeq"      :: "[seqobj,seqcont] => sequence"       ("__" [] 1000)
- "@MtSeqCont"   :: "seqcont"                            ("" [] 1000)
- "@SeqCont"     :: "[seqobj,seqcont] => seqcont"        (",/ __" [] 1000)
- ""             :: "o => seqobj"                        ("_" [] 1000)
- "@SeqId"       :: "id => seqobj"                       ("$_" [] 1000)
- "@SeqVar"      :: "var => seqobj"                      ("$_")
+  (*Representation of sequents*)
+  Trueprop     :: [sobj=>sobj, sobj=>sobj] => prop
+  Seqof        :: [o, sobj] => sobj
+
+syntax
+  "@Trueprop"  :: [sequence,sequence] => prop     ("((_)/ |- (_))" [6,6] 5)
+  NullSeq      :: sequence                        ("" [] 1000)
+  NonNullSeq   :: [seqobj,seqcont] => sequence    ("__" [] 1000)
+  NullSeqCont  :: seqcont                         ("" [] 1000)
+  SeqCont      :: [seqobj,seqcont] => seqcont     (",/ __" [] 1000)
+  ""           :: o => seqobj                     ("_" [] 1000)
+  SeqId        :: id => seqobj                    ("$_" [] 1000)
+  SeqVar       :: var => seqobj                   ("$_")
 
 rules
   (*Structural rules*)
@@ -99,31 +104,31 @@
 (*Representation of empty sequence*)
 val Sempty =  abs_sobj (Bound 0);
 
-fun seq_obj_tr(Const("@SeqId",_)$id) = id |
-    seq_obj_tr(Const("@SeqVar",_)$id) = id |
-    seq_obj_tr(fm) = Const("Seqof",dummyT)$fm;
+fun seq_obj_tr (Const("SeqId",_)$id) = id
+  | seq_obj_tr (Const("SeqVar",_)$id) = id
+  | seq_obj_tr (fm) = Const("Seqof",dummyT)$fm;
 
-fun seq_tr(_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq) |
-    seq_tr(_) = Bound 0;
+fun seq_tr (_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq)
+  | seq_tr (_) = Bound 0;
 
-fun seq_tr1(Const("@MtSeq",_)) = Sempty |
-    seq_tr1(seq) = abs_sobj(seq_tr seq);
+fun seq_tr1 (Const("NullSeq",_)) = Sempty
+  | seq_tr1 (seq) = abs_sobj(seq_tr seq);
 
 fun true_tr[s1,s2] = Const("Trueprop",dummyT)$seq_tr1 s1$seq_tr1 s2;
 
-fun seq_obj_tr'(Const("Seqof",_)$fm) = fm |
-    seq_obj_tr'(id) = Const("@SeqId",dummyT)$id;
+fun seq_obj_tr' (Const("Seqof",_)$fm) = fm
+  | seq_obj_tr' (id) = Const("SeqId",dummyT)$id;
 
-fun seq_tr'(obj$sq,C) =
+fun seq_tr' (obj$sq,C) =
       let val sq' = case sq of
-            Bound 0 => Const("@MtSeqCont",dummyT) |
-            _ => seq_tr'(sq,Const("@SeqCont",dummyT))
+            Bound 0 => Const("NullSeqCont",dummyT)
+  |         _ => seq_tr'(sq,Const("SeqCont",dummyT))
       in C $ seq_obj_tr' obj $ sq' end;
 
-fun seq_tr1'(Bound 0) = Const("@MtSeq",dummyT) |
-    seq_tr1' s = seq_tr'(s,Const("@NmtSeq",dummyT));
+fun seq_tr1' (Bound 0) = Const("NullSeq",dummyT)
+  | seq_tr1' s = seq_tr'(s,Const("NonNullSeq",dummyT));
 
-fun true_tr'[Abs(_,_,s1),Abs(_,_,s2)] =
+fun true_tr' [Abs(_,_,s1),Abs(_,_,s2)] =
       Const("@Trueprop",dummyT)$seq_tr1' s1$seq_tr1' s2;
 
 val parse_translation = [("@Trueprop",true_tr)];