Tidied up; added "syntax" decl
authorpaulson
Tue Jul 16 15:44:21 1996 +0200 (1996-07-16)
changeset 18639402e633fe53
parent 1862 74d4ae2f6fc3
child 1864 9ac4c2240d89
Tidied up; added "syntax" decl
src/LK/LK.thy
     1.1 --- a/src/LK/LK.thy	Mon Jul 15 14:58:28 1996 +0200
     1.2 +++ b/src/LK/LK.thy	Tue Jul 16 15:44:21 1996 +0200
     1.3 @@ -4,6 +4,9 @@
     1.4      Copyright   1993  University of Cambridge
     1.5  
     1.6  Classical First-Order Sequent Calculus
     1.7 +
     1.8 +There may be printing problems if a seqent is in expanded normal form
     1.9 +	(eta-expanded, beta-contracted)
    1.10  *)
    1.11  
    1.12  LK = Pure +
    1.13 @@ -13,33 +16,35 @@
    1.14  default term
    1.15  
    1.16  types
    1.17 - o sequence seqobj seqcont sobj
    1.18 +  o sequence seqobj seqcont sobj
    1.19  
    1.20  arities
    1.21 - o :: logic
    1.22 +  o :: logic
    1.23  
    1.24  consts
    1.25 - True,False     :: "o"
    1.26 - "="            :: "['a,'a] => o"       (infixl 50)
    1.27 - "Not"          :: "o => o"             ("~ _" [40] 40)
    1.28 - "&"            :: "[o,o] => o"         (infixr 35)
    1.29 - "|"            :: "[o,o] => o"         (infixr 30)
    1.30 - "-->","<->"    :: "[o,o] => o"         (infixr 25)
    1.31 - The            :: "('a => o) => 'a"    (binder "THE " 10)
    1.32 - All            :: "('a => o) => o"     (binder "ALL " 10)
    1.33 - Ex             :: "('a => o) => o"     (binder "EX " 10)
    1.34 +  True,False   :: o
    1.35 +  "="          :: ['a,'a] => o       (infixl 50)
    1.36 +  Not          :: o => o             ("~ _" [40] 40)
    1.37 +  "&"          :: [o,o] => o         (infixr 35)
    1.38 +  "|"          :: [o,o] => o         (infixr 30)
    1.39 +  "-->","<->"  :: [o,o] => o         (infixr 25)
    1.40 +  The          :: ('a => o) => 'a    (binder "THE " 10)
    1.41 +  All          :: ('a => o) => o     (binder "ALL " 10)
    1.42 +  Ex           :: ('a => o) => o     (binder "EX " 10)
    1.43  
    1.44 - (*Representation of sequents*)
    1.45 - Trueprop       :: "[sobj=>sobj,sobj=>sobj] => prop"
    1.46 - Seqof          :: "o => sobj=>sobj"
    1.47 - "@Trueprop"    :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
    1.48 - "@MtSeq"       :: "sequence"                           ("" [] 1000)
    1.49 - "@NmtSeq"      :: "[seqobj,seqcont] => sequence"       ("__" [] 1000)
    1.50 - "@MtSeqCont"   :: "seqcont"                            ("" [] 1000)
    1.51 - "@SeqCont"     :: "[seqobj,seqcont] => seqcont"        (",/ __" [] 1000)
    1.52 - ""             :: "o => seqobj"                        ("_" [] 1000)
    1.53 - "@SeqId"       :: "id => seqobj"                       ("$_" [] 1000)
    1.54 - "@SeqVar"      :: "var => seqobj"                      ("$_")
    1.55 +  (*Representation of sequents*)
    1.56 +  Trueprop     :: [sobj=>sobj, sobj=>sobj] => prop
    1.57 +  Seqof        :: [o, sobj] => sobj
    1.58 +
    1.59 +syntax
    1.60 +  "@Trueprop"  :: [sequence,sequence] => prop     ("((_)/ |- (_))" [6,6] 5)
    1.61 +  NullSeq      :: sequence                        ("" [] 1000)
    1.62 +  NonNullSeq   :: [seqobj,seqcont] => sequence    ("__" [] 1000)
    1.63 +  NullSeqCont  :: seqcont                         ("" [] 1000)
    1.64 +  SeqCont      :: [seqobj,seqcont] => seqcont     (",/ __" [] 1000)
    1.65 +  ""           :: o => seqobj                     ("_" [] 1000)
    1.66 +  SeqId        :: id => seqobj                    ("$_" [] 1000)
    1.67 +  SeqVar       :: var => seqobj                   ("$_")
    1.68  
    1.69  rules
    1.70    (*Structural rules*)
    1.71 @@ -99,31 +104,31 @@
    1.72  (*Representation of empty sequence*)
    1.73  val Sempty =  abs_sobj (Bound 0);
    1.74  
    1.75 -fun seq_obj_tr(Const("@SeqId",_)$id) = id |
    1.76 -    seq_obj_tr(Const("@SeqVar",_)$id) = id |
    1.77 -    seq_obj_tr(fm) = Const("Seqof",dummyT)$fm;
    1.78 +fun seq_obj_tr (Const("SeqId",_)$id) = id
    1.79 +  | seq_obj_tr (Const("SeqVar",_)$id) = id
    1.80 +  | seq_obj_tr (fm) = Const("Seqof",dummyT)$fm;
    1.81  
    1.82 -fun seq_tr(_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq) |
    1.83 -    seq_tr(_) = Bound 0;
    1.84 +fun seq_tr (_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq)
    1.85 +  | seq_tr (_) = Bound 0;
    1.86  
    1.87 -fun seq_tr1(Const("@MtSeq",_)) = Sempty |
    1.88 -    seq_tr1(seq) = abs_sobj(seq_tr seq);
    1.89 +fun seq_tr1 (Const("NullSeq",_)) = Sempty
    1.90 +  | seq_tr1 (seq) = abs_sobj(seq_tr seq);
    1.91  
    1.92  fun true_tr[s1,s2] = Const("Trueprop",dummyT)$seq_tr1 s1$seq_tr1 s2;
    1.93  
    1.94 -fun seq_obj_tr'(Const("Seqof",_)$fm) = fm |
    1.95 -    seq_obj_tr'(id) = Const("@SeqId",dummyT)$id;
    1.96 +fun seq_obj_tr' (Const("Seqof",_)$fm) = fm
    1.97 +  | seq_obj_tr' (id) = Const("SeqId",dummyT)$id;
    1.98  
    1.99 -fun seq_tr'(obj$sq,C) =
   1.100 +fun seq_tr' (obj$sq,C) =
   1.101        let val sq' = case sq of
   1.102 -            Bound 0 => Const("@MtSeqCont",dummyT) |
   1.103 -            _ => seq_tr'(sq,Const("@SeqCont",dummyT))
   1.104 +            Bound 0 => Const("NullSeqCont",dummyT)
   1.105 +  |         _ => seq_tr'(sq,Const("SeqCont",dummyT))
   1.106        in C $ seq_obj_tr' obj $ sq' end;
   1.107  
   1.108 -fun seq_tr1'(Bound 0) = Const("@MtSeq",dummyT) |
   1.109 -    seq_tr1' s = seq_tr'(s,Const("@NmtSeq",dummyT));
   1.110 +fun seq_tr1' (Bound 0) = Const("NullSeq",dummyT)
   1.111 +  | seq_tr1' s = seq_tr'(s,Const("NonNullSeq",dummyT));
   1.112  
   1.113 -fun true_tr'[Abs(_,_,s1),Abs(_,_,s2)] =
   1.114 +fun true_tr' [Abs(_,_,s1),Abs(_,_,s2)] =
   1.115        Const("@Trueprop",dummyT)$seq_tr1' s1$seq_tr1' s2;
   1.116  
   1.117  val parse_translation = [("@Trueprop",true_tr)];