src/Sequents/Sequents.thy
author paulson
Tue Jul 27 19:02:43 1999 +0200 (1999-07-27)
changeset 7098 86583034aacf
parent 6819 433a980103b4
child 7121 0e3d09451b7a
permissions -rw-r--r--
installation of simplifier and classical reasoner, better rules etc
     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  SeqVar         :: "var => 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 end
    59 
    60 ML
    61 
    62 (* parse translation for sequences *)
    63 
    64 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    65 
    66 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
    67     seqobj_tr(_ $ i) = i;
    68     
    69 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    70     seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
    71       (seqobj_tr so) $ (seqcont_tr sc);
    72 
    73 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    74     seq_tr(Const("SeqApp",_) $ so $ sc) = 
    75       abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
    76 
    77 
    78 fun singlobj_tr(Const("SeqO",_) $ f) =
    79     abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
    80     
    81 
    82     
    83 (* print translation for sequences *)
    84 
    85 fun seqcont_tr' (Bound 0) = 
    86       Const("SeqContEmp",dummyT) |
    87     seqcont_tr' (Const("SeqO'",_) $ f $ s) =
    88       Const("SeqContApp",dummyT) $ 
    89       (Const("SeqO",dummyT) $ f) $ 
    90       (seqcont_tr' s) |
    91 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
    92       seqcont_tr'(betapply(a,s)) | *)
    93     seqcont_tr' (i $ s) = 
    94       Const("SeqContApp",dummyT) $ 
    95       (Const("SeqId",dummyT) $ i) $ 
    96       (seqcont_tr' s);
    97 
    98 fun seq_tr' s =
    99     let fun seq_itr' (Bound 0) = 
   100               Const("SeqEmp",dummyT) |
   101             seq_itr' (Const("SeqO'",_) $ f $ s) =
   102               Const("SeqApp",dummyT) $ 
   103               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
   104 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
   105               seq_itr'(betapply(a,s)) |    *)
   106             seq_itr' (i $ s) =
   107               Const("SeqApp",dummyT) $ 
   108               (Const("SeqId",dummyT) $ i) $ 
   109               (seqcont_tr' s)
   110     in case s of 
   111          Abs(_,_,t) => seq_itr' t |
   112          _ => s $ (Bound 0)
   113     end;
   114 
   115 
   116 
   117 
   118 fun single_tr c [s1,s2] =
   119     Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
   120 
   121 fun two_seq_tr c [s1,s2] =
   122     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
   123 
   124 fun three_seq_tr c [s1,s2,s3] =
   125     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
   126 
   127 fun four_seq_tr c [s1,s2,s3,s4] =
   128     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
   129 
   130 
   131 fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
   132     singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
   133 
   134 
   135 fun single_tr' c [s1, s2] =
   136 (Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
   137 
   138 
   139 fun two_seq_tr' c [s1, s2] =
   140   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
   141 
   142 fun three_seq_tr' c [s1, s2, s3] =
   143   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
   144 
   145 fun four_seq_tr' c [s1, s2, s3, s4] =
   146   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
   147 
   148 
   149