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