author | oheimb |
Mon, 02 Dec 1996 12:19:56 +0100 | |
changeset 2290 | e5c08f8b483b |
parent 1477 | 4c51ab632cda |
child 2714 | b0fbdfbbad66 |
permissions | -rw-r--r-- |
1477 | 1 |
(* Title: FOLP/IFOLP.thy |
1142 | 2 |
ID: $Id$ |
1477 | 3 |
Author: Martin D Coen, Cambridge University Computer Laboratory |
1142 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
Intuitionistic First-Order Logic with Proofs |
|
7 |
*) |
|
8 |
||
0 | 9 |
IFOLP = Pure + |
10 |
||
11 |
classes term < logic |
|
12 |
||
13 |
default term |
|
14 |
||
283 | 15 |
types |
16 |
p |
|
17 |
o |
|
0 | 18 |
|
283 | 19 |
arities |
20 |
p,o :: logic |
|
0 | 21 |
|
1477 | 22 |
consts |
0 | 23 |
(*** Judgements ***) |
1477 | 24 |
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) |
25 |
Proof :: "[o,p]=>prop" |
|
0 | 26 |
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) |
27 |
||
28 |
(*** Logical Connectives -- Type Formers ***) |
|
1477 | 29 |
"=" :: "['a,'a] => o" (infixl 50) |
30 |
True,False :: "o" |
|
31 |
"Not" :: "o => o" ("~ _" [40] 40) |
|
32 |
"&" :: "[o,o] => o" (infixr 35) |
|
33 |
"|" :: "[o,o] => o" (infixr 30) |
|
34 |
"-->" :: "[o,o] => o" (infixr 25) |
|
35 |
"<->" :: "[o,o] => o" (infixr 25) |
|
0 | 36 |
(*Quantifiers*) |
1477 | 37 |
All :: "('a => o) => o" (binder "ALL " 10) |
38 |
Ex :: "('a => o) => o" (binder "EX " 10) |
|
39 |
Ex1 :: "('a => o) => o" (binder "EX! " 10) |
|
0 | 40 |
(*Rewriting gadgets*) |
1477 | 41 |
NORM :: "o => o" |
42 |
norm :: "'a => 'a" |
|
0 | 43 |
|
648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset
|
44 |
(*** Proof Term Formers: precedence must exceed 50 ***) |
1477 | 45 |
tt :: "p" |
46 |
contr :: "p=>p" |
|
47 |
fst,snd :: "p=>p" |
|
48 |
pair :: "[p,p]=>p" ("(1<_,/_>)") |
|
49 |
split :: "[p, [p,p]=>p] =>p" |
|
50 |
inl,inr :: "p=>p" |
|
51 |
when :: "[p, p=>p, p=>p]=>p" |
|
52 |
lambda :: "(p => p) => p" (binder "lam " 55) |
|
53 |
"`" :: "[p,p]=>p" (infixl 60) |
|
648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset
|
54 |
alll :: "['a=>p]=>p" (binder "all " 55) |
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset
|
55 |
"^" :: "[p,'a]=>p" (infixl 55) |
1477 | 56 |
exists :: "['a,p]=>p" ("(1[_,/_])") |
0 | 57 |
xsplit :: "[p,['a,p]=>p]=>p" |
58 |
ideq :: "'a=>p" |
|
59 |
idpeel :: "[p,'a=>p]=>p" |
|
60 |
nrm, NRM :: "p" |
|
61 |
||
62 |
rules |
|
63 |
||
64 |
(**** Propositional logic ****) |
|
65 |
||
66 |
(*Equality*) |
|
67 |
(* Like Intensional Equality in MLTT - but proofs distinct from terms *) |
|
68 |
||
1477 | 69 |
ieqI "ideq(a) : a=a" |
0 | 70 |
ieqE "[| p : a=b; !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)" |
71 |
||
72 |
(* Truth and Falsity *) |
|
73 |
||
74 |
TrueI "tt : True" |
|
75 |
FalseE "a:False ==> contr(a):P" |
|
76 |
||
77 |
(* Conjunction *) |
|
78 |
||
79 |
conjI "[| a:P; b:Q |] ==> <a,b> : P&Q" |
|
80 |
conjunct1 "p:P&Q ==> fst(p):P" |
|
81 |
conjunct2 "p:P&Q ==> snd(p):Q" |
|
82 |
||
83 |
(* Disjunction *) |
|
84 |
||
85 |
disjI1 "a:P ==> inl(a):P|Q" |
|
86 |
disjI2 "b:Q ==> inr(b):P|Q" |
|
1149 | 87 |
disjE "[| a:P|Q; !!x.x:P ==> f(x):R; !!x.x:Q ==> g(x):R |
88 |
|] ==> when(a,f,g):R" |
|
0 | 89 |
|
90 |
(* Implication *) |
|
91 |
||
92 |
impI "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q" |
|
93 |
mp "[| f:P-->Q; a:P |] ==> f`a:Q" |
|
94 |
||
95 |
(*Quantifiers*) |
|
96 |
||
1477 | 97 |
allI "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)" |
98 |
spec "(f:ALL x.P(x)) ==> f^x : P(x)" |
|
0 | 99 |
|
1477 | 100 |
exI "p : P(x) ==> [x,p] : EX x.P(x)" |
101 |
exE "[| p: EX x.P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R" |
|
0 | 102 |
|
103 |
(**** Equality between proofs ****) |
|
104 |
||
105 |
prefl "a : P ==> a = a : P" |
|
106 |
psym "a = b : P ==> b = a : P" |
|
107 |
ptrans "[| a = b : P; b = c : P |] ==> a = c : P" |
|
108 |
||
109 |
idpeelB "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" |
|
110 |
||
111 |
fstB "a:P ==> fst(<a,b>) = a : P" |
|
112 |
sndB "b:Q ==> snd(<a,b>) = b : Q" |
|
113 |
pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" |
|
114 |
||
115 |
whenBinl "[| a:P; !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" |
|
116 |
whenBinr "[| b:P; !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" |
|
117 |
plusEC "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q" |
|
118 |
||
119 |
applyB "[| a:P; !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q" |
|
120 |
funEC "f:P ==> f = lam x.f`x : P" |
|
121 |
||
122 |
specB "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)" |
|
123 |
||
124 |
||
125 |
(**** Definitions ****) |
|
126 |
||
1477 | 127 |
not_def "~P == P-->False" |
0 | 128 |
iff_def "P<->Q == (P-->Q) & (Q-->P)" |
129 |
||
130 |
(*Unique existence*) |
|
131 |
ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
|
132 |
||
133 |
(*Rewriting -- special constants to flag normalized terms and formulae*) |
|
1477 | 134 |
norm_eq "nrm : norm(x) = x" |
135 |
NORM_iff "NRM : NORM(P) <-> P" |
|
0 | 136 |
|
137 |
end |
|
138 |
||
139 |
ML |
|
140 |
||
141 |
(*show_proofs:=true displays the proof terms -- they are ENORMOUS*) |
|
142 |
val show_proofs = ref false; |
|
143 |
||
144 |
fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p; |
|
145 |
||
146 |
fun proof_tr' [P,p] = |
|
147 |
if !show_proofs then Const("@Proof",dummyT) $ p $ P |
|
148 |
else P (*this case discards the proof term*); |
|
149 |
||
150 |
val parse_translation = [("@Proof", proof_tr)]; |
|
151 |
val print_translation = [("Proof", proof_tr')]; |
|
152 |