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