src/Sequents/Sequents.thy
changeset 6819 433a980103b4
parent 2073 fb0655539d05
child 7098 86583034aacf
equal deleted inserted replaced
6818:852f9ed01a53 6819:433a980103b4
     1 (*  Title: 	LK/lk.thy
     1 (*  Title: 	Sequents/Sequents.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Classical First-Order Sequent Calculus
     6 Classical First-Order Sequent Calculus
    59 
    59 
    60 (* parse translation for sequences *)
    60 (* parse translation for sequences *)
    61 
    61 
    62 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    62 fun abs_seq' t = Abs("s", Type("seq'",[]), t);
    63 
    63 
    64 fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
    64 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
    65     seqobj_tr(_$i) = i;
    65     seqobj_tr(_ $ i) = i;
    66     
    66     
    67 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    67 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
    68     seqcont_tr(Const("SeqContApp",_)$so$sc) = 
    68     seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
    69       (seqobj_tr so)$(seqcont_tr sc);
    69       (seqobj_tr so) $ (seqcont_tr sc);
    70 
    70 
    71 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    71 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
    72     seq_tr(Const("SeqApp",_)$so$sc) = 
    72     seq_tr(Const("SeqApp",_) $ so $ sc) = 
    73       abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
    73       abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
    74 
    74 
    75 
    75 
    76 fun singlobj_tr(Const("SeqO",_)$f) =
    76 fun singlobj_tr(Const("SeqO",_) $ f) =
    77     abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
    77     abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
    78     
    78     
    79 
    79 
    80     
    80     
    81 (* print translation for sequences *)
    81 (* print translation for sequences *)
    82 
    82 
    83 fun seqcont_tr' (Bound 0) = 
    83 fun seqcont_tr' (Bound 0) = 
    84       Const("SeqContEmp",dummyT) |
    84       Const("SeqContEmp",dummyT) |
    85     seqcont_tr' (Const("SeqO'",_)$f$s) =
    85     seqcont_tr' (Const("SeqO'",_) $ f $ s) =
    86       Const("SeqContApp",dummyT)$
    86       Const("SeqContApp",dummyT) $ 
    87       (Const("SeqO",dummyT)$f)$
    87       (Const("SeqO",dummyT) $ f) $ 
    88       (seqcont_tr' s) |
    88       (seqcont_tr' s) |
    89 (*    seqcont_tr' ((a as Abs(_,_,_))$s)= 
    89 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
    90       seqcont_tr'(betapply(a,s)) | *)
    90       seqcont_tr'(betapply(a,s)) | *)
    91     seqcont_tr' (i$s) = 
    91     seqcont_tr' (i $ s) = 
    92       Const("SeqContApp",dummyT)$
    92       Const("SeqContApp",dummyT) $ 
    93       (Const("SeqId",dummyT)$i)$
    93       (Const("SeqId",dummyT) $ i) $ 
    94       (seqcont_tr' s);
    94       (seqcont_tr' s);
    95 
    95 
    96 fun seq_tr' s =
    96 fun seq_tr' s =
    97     let fun seq_itr' (Bound 0) = 
    97     let fun seq_itr' (Bound 0) = 
    98               Const("SeqEmp",dummyT) |
    98               Const("SeqEmp",dummyT) |
    99             seq_itr' (Const("SeqO'",_)$f$s) =
    99             seq_itr' (Const("SeqO'",_) $ f $ s) =
   100               Const("SeqApp",dummyT)$
   100               Const("SeqApp",dummyT) $ 
   101               (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
   101               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
   102 (*            seq_itr' ((a as Abs(_,_,_))$s) =
   102 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
   103               seq_itr'(betapply(a,s)) |    *)
   103               seq_itr'(betapply(a,s)) |    *)
   104             seq_itr' (i$s) =
   104             seq_itr' (i $ s) =
   105               Const("SeqApp",dummyT)$
   105               Const("SeqApp",dummyT) $ 
   106               (Const("SeqId",dummyT)$i)$
   106               (Const("SeqId",dummyT) $ i) $ 
   107               (seqcont_tr' s)
   107               (seqcont_tr' s)
   108     in case s of 
   108     in case s of 
   109          Abs(_,_,t) => seq_itr' t |
   109          Abs(_,_,t) => seq_itr' t |
   110          _ => s$(Bound 0)
   110          _ => s $ (Bound 0)
   111     end;
   111     end;
   112 
   112 
   113 
   113 
   114 
   114 
   115 
   115 
   116 fun single_tr c [s1,s2] =
   116 fun single_tr c [s1,s2] =
   117     Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
   117     Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
   118 
   118 
   119 fun two_seq_tr c [s1,s2] =
   119 fun two_seq_tr c [s1,s2] =
   120     Const(c,dummyT)$seq_tr s1$seq_tr s2;
   120     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
   121 
   121 
   122 fun three_seq_tr c [s1,s2,s3] =
   122 fun three_seq_tr c [s1,s2,s3] =
   123     Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
   123     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
   124 
   124 
   125 fun four_seq_tr c [s1,s2,s3,s4] =
   125 fun four_seq_tr c [s1,s2,s3,s4] =
   126     Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
   126     Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
   127 
   127 
   128 
   128 
   129 fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
   129 fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
   130     singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
   130     singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
   131 
   131 
   132 
   132 
   133 fun single_tr' c [s1, s2] =
   133 fun single_tr' c [s1, s2] =
   134 (Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); 
   134 (Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
   135 
   135 
   136 
   136 
   137 fun two_seq_tr' c [s1, s2] =
   137 fun two_seq_tr' c [s1, s2] =
   138   Const (c, dummyT)$seq_tr' s1$seq_tr' s2; 
   138   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
   139 
   139 
   140 fun three_seq_tr' c [s1, s2, s3] =
   140 fun three_seq_tr' c [s1, s2, s3] =
   141   Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; 
   141   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
   142 
   142 
   143 fun four_seq_tr' c [s1, s2, s3, s4] =
   143 fun four_seq_tr' c [s1, s2, s3, s4] =
   144   Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; 
   144   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
   145 
   145 
   146 
   146 
   147 			 
   147