src/Sequents/Sequents.thy
 changeset 6819 433a980103b4 parent 2073 fb0655539d05 child 7098 86583034aacf
equal 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