src/Sequents/Sequents.thy
author paulson
Wed Jul 28 13:52:59 1999 +0200 (1999-07-28)
changeset 7121 0e3d09451b7a
parent 7098 86583034aacf
child 7166 a4a870ec2e67
permissions -rw-r--r--
removed the unused SeqVar option
     1 (*  Title: 	Sequents/Sequents.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 global
    12 
    13 types
    14   o 
    15 
    16 arities
    17   o :: logic
    18 
    19 
    20 (* Sequences *)
    21 
    22 types
    23  seq'
    24 
    25 consts
    26  SeqO'         :: "[o,seq']=>seq'"
    27  Seq1'         :: "o=>seq'"
    28     
    29 
    30 (* concrete syntax *)
    31 
    32 types
    33   seq seqobj seqcont
    34 
    35 
    36 syntax
    37  SeqEmp         :: "seq"                                ("")
    38  SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
    39 
    40  SeqContEmp     :: "seqcont"                            ("")
    41  SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
    42   
    43  SeqO           :: "o => seqobj"                        ("_")
    44  SeqId          :: "'a => seqobj"                       ("$_")
    45 
    46 types
    47     
    48  single_seqe = "[seq,seqobj] => prop"
    49  single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
    50  two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
    51  two_seqe = "[seq, seq] => prop"
    52  three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    53  three_seqe = "[seq, seq, seq] => prop"
    54  four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    55  four_seqe = "[seq, seq, seq, seq] => prop"
    56 
    57 end
    58 
    59 ML
    60 
    61 (* parse translation for sequences *)
    62 
    63 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    64 
    65 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
    66     seqobj_tr(_ $ i) = i;
    67     
    68 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    69     seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
    70       (seqobj_tr so) $ (seqcont_tr sc);
    71 
    72 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    73     seq_tr(Const("SeqApp",_) $ so $ sc) = 
    74       abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
    75 
    76 
    77 fun singlobj_tr(Const("SeqO",_) $ f) =
    78     abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
    79     
    80 
    81     
    82 (* print translation for sequences *)
    83 
    84 fun seqcont_tr' (Bound 0) = 
    85       Const("SeqContEmp",dummyT) |
    86     seqcont_tr' (Const("SeqO'",_) $ f $ s) =
    87       Const("SeqContApp",dummyT) $ 
    88       (Const("SeqO",dummyT) $ f) $ 
    89       (seqcont_tr' s) |
    90 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
    91       seqcont_tr'(betapply(a,s)) | *)
    92     seqcont_tr' (i $ s) = 
    93       Const("SeqContApp",dummyT) $ 
    94       (Const("SeqId",dummyT) $ i) $ 
    95       (seqcont_tr' s);
    96 
    97 fun seq_tr' s =
    98     let fun seq_itr' (Bound 0) = 
    99               Const("SeqEmp",dummyT) |
   100             seq_itr' (Const("SeqO'",_) $ f $ s) =
   101               Const("SeqApp",dummyT) $ 
   102               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
   103 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
   104               seq_itr'(betapply(a,s)) |    *)
   105             seq_itr' (i $ s) =
   106               Const("SeqApp",dummyT) $ 
   107               (Const("SeqId",dummyT) $ i) $ 
   108               (seqcont_tr' s)
   109     in case s of 
   110          Abs(_,_,t) => seq_itr' t |
   111          _ => s $ (Bound 0)
   112     end;
   113 
   114 
   115 
   116 
   117 fun single_tr c [s1,s2] =
   118     Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
   119 
   120 fun two_seq_tr c [s1,s2] =
   121     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
   122 
   123 fun three_seq_tr c [s1,s2,s3] =
   124     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
   125 
   126 fun four_seq_tr c [s1,s2,s3,s4] =
   127     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
   128 
   129 
   130 fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
   131     singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
   132 
   133 
   134 fun single_tr' c [s1, s2] =
   135 (Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
   136 
   137 
   138 fun two_seq_tr' c [s1, s2] =
   139   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
   140 
   141 fun three_seq_tr' c [s1, s2, s3] =
   142   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
   143 
   144 fun four_seq_tr' c [s1, s2, s3, s4] =
   145   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
   146 
   147 
   148