src/Sequents/Sequents.thy
author wenzelm
Tue Jun 01 12:33:50 2004 +0200 (2004-06-01)
changeset 14854 61bdf2ae4dc5
parent 14765 bafb24c150c1
child 17481 75166ebb619b
permissions -rw-r--r--
removed obsolete sort 'logic';
     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 Basis theory for parsing and pretty-printing of sequences to be used in
     7 Sequent Calculi. 
     8 *)
     9 
    10 Sequents = Pure +
    11 
    12 global
    13 
    14 types
    15   o 
    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 nonterminals
    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          :: 'a => seqobj                       ("$_")
    43 
    44 types
    45     
    46  single_seqe = [seq,seqobj] => prop
    47  single_seqi = [seq'=>seq',seq'=>seq'] => prop
    48  two_seqi    = [seq'=>seq', seq'=>seq'] => prop
    49  two_seqe    = [seq, seq] => prop
    50  three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
    51  three_seqe  = [seq, seq, seq] => prop
    52  four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
    53  four_seqe   = [seq, seq, seq, seq] => prop
    54 
    55 
    56  sequence_name = seq'=>seq'
    57 
    58 
    59 syntax
    60   (*Constant to allow definitions of SEQUENCES of formulas*)
    61   "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
    62 
    63 end
    64 
    65 ML
    66 
    67 (* parse translation for sequences *)
    68 
    69 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    70 
    71 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
    72     seqobj_tr(_ $ i) = i;
    73     
    74 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    75     seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
    76       (seqobj_tr so) $ (seqcont_tr sc);
    77 
    78 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    79     seq_tr(Const("SeqApp",_) $ so $ sc) = 
    80       abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
    81 
    82 
    83 fun singlobj_tr(Const("SeqO",_) $ f) =
    84     abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
    85     
    86 
    87     
    88 (* print translation for sequences *)
    89 
    90 fun seqcont_tr' (Bound 0) = 
    91       Const("SeqContEmp",dummyT) |
    92     seqcont_tr' (Const("SeqO'",_) $ f $ s) =
    93       Const("SeqContApp",dummyT) $ 
    94       (Const("SeqO",dummyT) $ f) $ 
    95       (seqcont_tr' s) |
    96 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
    97       seqcont_tr'(betapply(a,s)) | *)
    98     seqcont_tr' (i $ s) = 
    99       Const("SeqContApp",dummyT) $ 
   100       (Const("SeqId",dummyT) $ i) $ 
   101       (seqcont_tr' s);
   102 
   103 fun seq_tr' s =
   104     let fun seq_itr' (Bound 0) = 
   105               Const("SeqEmp",dummyT) |
   106             seq_itr' (Const("SeqO'",_) $ f $ s) =
   107               Const("SeqApp",dummyT) $ 
   108               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
   109 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
   110               seq_itr'(betapply(a,s)) |    *)
   111             seq_itr' (i $ s) =
   112               Const("SeqApp",dummyT) $ 
   113               (Const("SeqId",dummyT) $ i) $ 
   114               (seqcont_tr' s)
   115     in case s of 
   116          Abs(_,_,t) => seq_itr' t |
   117          _ => s $ (Bound 0)
   118     end;
   119 
   120 
   121 
   122 
   123 fun single_tr c [s1,s2] =
   124     Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
   125 
   126 fun two_seq_tr c [s1,s2] =
   127     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
   128 
   129 fun three_seq_tr c [s1,s2,s3] =
   130     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
   131 
   132 fun four_seq_tr c [s1,s2,s3,s4] =
   133     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
   134 
   135 
   136 fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
   137     singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
   138 
   139 
   140 fun single_tr' c [s1, s2] =
   141 (Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
   142 
   143 
   144 fun two_seq_tr' c [s1, s2] =
   145   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
   146 
   147 fun three_seq_tr' c [s1, s2, s3] =
   148   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
   149 
   150 fun four_seq_tr' c [s1, s2, s3, s4] =
   151   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
   152 
   153 
   154 			 
   155 (** for the <<...>> notation **)
   156   
   157 fun side_tr [s1] = seq_tr s1;
   158 
   159 val parse_translation = [("@Side", side_tr)];