src/Sequents/Sequents.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 2073 fb0655539d05
child 6819 433a980103b4
permissions -rw-r--r--
tidying
     1 (*  Title: 	LK/lk.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Classical First-Order Sequent Calculus
     7 *)
     8 
     9 Sequents = Pure +
    10 
    11 types
    12   o 
    13 
    14 arities
    15   o :: logic
    16 
    17 
    18 (* Sequences *)
    19 
    20 types
    21  seq'
    22 
    23 consts
    24  SeqO'         :: "[o,seq']=>seq'"
    25  Seq1'         :: "o=>seq'"
    26     
    27 
    28 (* concrete syntax *)
    29 
    30 types
    31   seq seqobj seqcont
    32 
    33 
    34 syntax
    35  SeqEmp         :: "seq"                                ("")
    36  SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
    37 
    38  SeqContEmp     :: "seqcont"                            ("")
    39  SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
    40   
    41  SeqO           :: "o => seqobj"                        ("_")
    42  SeqId          :: "id => seqobj"                       ("$_")
    43  SeqVar         :: "var => seqobj"                      ("$_")
    44 
    45 types
    46     
    47  single_seqe = "[seq,seqobj] => prop"
    48  single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
    49  two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
    50  two_seqe = "[seq, seq] => prop"
    51  three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    52  three_seqe = "[seq, seq, seq] => prop"
    53  four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    54  four_seqe = "[seq, seq, seq, seq] => prop"
    55 
    56 end
    57 
    58 ML
    59 
    60 (* parse translation for sequences *)
    61 
    62 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    63 
    64 fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
    65     seqobj_tr(_$i) = i;
    66     
    67 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    68     seqcont_tr(Const("SeqContApp",_)$so$sc) = 
    69       (seqobj_tr so)$(seqcont_tr sc);
    70 
    71 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    72     seq_tr(Const("SeqApp",_)$so$sc) = 
    73       abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
    74 
    75 
    76 fun singlobj_tr(Const("SeqO",_)$f) =
    77     abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
    78     
    79 
    80     
    81 (* print translation for sequences *)
    82 
    83 fun seqcont_tr' (Bound 0) = 
    84       Const("SeqContEmp",dummyT) |
    85     seqcont_tr' (Const("SeqO'",_)$f$s) =
    86       Const("SeqContApp",dummyT)$
    87       (Const("SeqO",dummyT)$f)$
    88       (seqcont_tr' s) |
    89 (*    seqcont_tr' ((a as Abs(_,_,_))$s)= 
    90       seqcont_tr'(betapply(a,s)) | *)
    91     seqcont_tr' (i$s) = 
    92       Const("SeqContApp",dummyT)$
    93       (Const("SeqId",dummyT)$i)$
    94       (seqcont_tr' s);
    95 
    96 fun seq_tr' s =
    97     let fun seq_itr' (Bound 0) = 
    98               Const("SeqEmp",dummyT) |
    99             seq_itr' (Const("SeqO'",_)$f$s) =
   100               Const("SeqApp",dummyT)$
   101               (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
   102 (*            seq_itr' ((a as Abs(_,_,_))$s) =
   103               seq_itr'(betapply(a,s)) |    *)
   104             seq_itr' (i$s) =
   105               Const("SeqApp",dummyT)$
   106               (Const("SeqId",dummyT)$i)$
   107               (seqcont_tr' s)
   108     in case s of 
   109          Abs(_,_,t) => seq_itr' t |
   110          _ => s$(Bound 0)
   111     end;
   112 
   113 
   114 
   115 
   116 fun single_tr c [s1,s2] =
   117     Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
   118 
   119 fun two_seq_tr c [s1,s2] =
   120     Const(c,dummyT)$seq_tr s1$seq_tr s2;
   121 
   122 fun three_seq_tr c [s1,s2,s3] =
   123     Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
   124 
   125 fun four_seq_tr c [s1,s2,s3,s4] =
   126     Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
   127 
   128 
   129 fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
   130     singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
   131 
   132 
   133 fun single_tr' c [s1, s2] =
   134 (Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); 
   135 
   136 
   137 fun two_seq_tr' c [s1, s2] =
   138   Const (c, dummyT)$seq_tr' s1$seq_tr' s2; 
   139 
   140 fun three_seq_tr' c [s1, s2, s3] =
   141   Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; 
   142 
   143 fun four_seq_tr' c [s1, s2, s3, s4] =
   144   Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; 
   145 
   146 
   147