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