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