author paulson Tue Jul 16 15:44:21 1996 +0200 (1996-07-16) changeset 1863 9402e633fe53 parent 1862 74d4ae2f6fc3 child 1864 9ac4c2240d89
 src/LK/LK.thy file | annotate | diff | revisions
```     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)];
```