author | wenzelm |
Tue, 01 Jun 2004 12:33:50 +0200 | |
changeset 14854 | 61bdf2ae4dc5 |
parent 14765 | bafb24c150c1 |
child 16019 | 0e1405402d53 |
permissions | -rw-r--r-- |
7093 | 1 |
(* Title: LK/LK0 |
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 |
There may be printing problems if a seqent is in expanded normal form |
|
9 |
(eta-expanded, beta-contracted) |
|
10 |
*) |
|
11 |
||
12 |
LK0 = Sequents + |
|
13 |
||
14 |
global |
|
15 |
||
14854 | 16 |
classes term |
17 |
default term |
|
7093 | 18 |
|
19 |
consts |
|
20 |
||
21 |
Trueprop :: "two_seqi" |
|
22 |
||
23 |
True,False :: o |
|
24 |
"=" :: ['a,'a] => o (infixl 50) |
|
25 |
Not :: o => o ("~ _" [40] 40) |
|
26 |
"&" :: [o,o] => o (infixr 35) |
|
27 |
"|" :: [o,o] => o (infixr 30) |
|
28 |
"-->","<->" :: [o,o] => o (infixr 25) |
|
29 |
The :: ('a => o) => 'a (binder "THE " 10) |
|
30 |
All :: ('a => o) => o (binder "ALL " 10) |
|
31 |
Ex :: ('a => o) => o (binder "EX " 10) |
|
32 |
||
33 |
syntax |
|
14765 | 34 |
"@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
12662 | 35 |
"_not_equal" :: ['a, 'a] => o (infixl "~=" 50) |
7093 | 36 |
|
37 |
translations |
|
38 |
"x ~= y" == "~ (x = y)" |
|
39 |
||
12116 | 40 |
syntax (xsymbols) |
7093 | 41 |
Not :: o => o ("\\<not> _" [40] 40) |
42 |
"op &" :: [o, o] => o (infixr "\\<and>" 35) |
|
43 |
"op |" :: [o, o] => o (infixr "\\<or>" 30) |
|
12116 | 44 |
"op -->" :: [o, o] => o (infixr "\\<longrightarrow>" 25) |
45 |
"op <->" :: [o, o] => o (infixr "\\<longleftrightarrow>" 25) |
|
7093 | 46 |
"ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10) |
47 |
"EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10) |
|
48 |
"EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
|
12662 | 49 |
"_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
7093 | 50 |
|
51 |
syntax (HTML output) |
|
52 |
Not :: o => o ("\\<not> _" [40] 40) |
|
14565 | 53 |
"op &" :: [o, o] => o (infixr "\\<and>" 35) |
54 |
"op |" :: [o, o] => o (infixr "\\<or>" 30) |
|
55 |
"ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10) |
|
56 |
"EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10) |
|
57 |
"EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
|
58 |
"_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
|
7093 | 59 |
|
60 |
||
61 |
local |
|
62 |
||
63 |
rules |
|
64 |
||
65 |
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *) |
|
66 |
||
67 |
contRS "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" |
|
68 |
contLS "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" |
|
69 |
||
70 |
thinRS "$H |- $E, $F ==> $H |- $E, $S, $F" |
|
71 |
thinLS "$H, $G |- $E ==> $H, $S, $G |- $E" |
|
72 |
||
73 |
exchRS "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" |
|
74 |
exchLS "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" |
|
75 |
||
76 |
cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" |
|
77 |
||
78 |
(*Propositional rules*) |
|
79 |
||
80 |
basic "$H, P, $G |- $E, P, $F" |
|
81 |
||
82 |
conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" |
|
83 |
conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" |
|
84 |
||
85 |
disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" |
|
86 |
disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" |
|
87 |
||
88 |
impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" |
|
89 |
impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" |
|
90 |
||
91 |
notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F" |
|
92 |
notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E" |
|
93 |
||
94 |
FalseL "$H, False, $G |- $E" |
|
95 |
||
96 |
True_def "True == False-->False" |
|
97 |
iff_def "P<->Q == (P-->Q) & (Q-->P)" |
|
98 |
||
99 |
(*Quantifiers*) |
|
100 |
||
101 |
allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" |
|
102 |
allL "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" |
|
103 |
||
104 |
exR "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" |
|
105 |
exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" |
|
106 |
||
107 |
(*Equality*) |
|
108 |
||
109 |
refl "$H |- $E, a=a, $F" |
|
110 |
subst "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)" |
|
111 |
||
112 |
(* Reflection *) |
|
113 |
||
114 |
eq_reflection "|- x=y ==> (x==y)" |
|
115 |
iff_reflection "|- P<->Q ==> (P==Q)" |
|
116 |
||
117 |
(*Descriptions*) |
|
118 |
||
119 |
The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
|
120 |
$H |- $E, P(THE x. P(x)), $F" |
|
121 |
||
122 |
constdefs |
|
123 |
If :: [o, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10) |
|
124 |
"If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" |
|
125 |
||
126 |
||
127 |
setup |
|
128 |
Simplifier.setup |
|
129 |
||
130 |
setup |
|
131 |
prover_setup |
|
132 |
||
133 |
end |
|
134 |
||
7118
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset
|
135 |
ML |
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset
|
136 |
|
7093 | 137 |
|
7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7118
diff
changeset
|
138 |
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; |
7093 | 139 |
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; |
7118
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset
|
140 |