author  wenzelm 
Mon, 20 Oct 1997 11:06:01 +0200  
changeset 3942  1f1c1f524d19 
parent 3836  f1a1817659e6 
child 6509  9f7f4fd05b1f 
permissions  rwrr 
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 FirstOrder Logic with Proofs 

7 
*) 

8 

0  9 
IFOLP = Pure + 
10 

3942  11 
global 
12 

0  13 
classes term < logic 
14 

15 
default term 

16 

283  17 
types 
18 
p 

19 
o 

0  20 

283  21 
arities 
22 
p,o :: logic 

0  23 

1477  24 
consts 
0  25 
(*** Judgements ***) 
1477  26 
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) 
27 
Proof :: "[o,p]=>prop" 

0  28 
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) 
29 

30 
(*** Logical Connectives  Type Formers ***) 

1477  31 
"=" :: "['a,'a] => o" (infixl 50) 
32 
True,False :: "o" 

2714  33 
Not :: "o => o" ("~ _" [40] 40) 
1477  34 
"&" :: "[o,o] => o" (infixr 35) 
35 
"" :: "[o,o] => o" (infixr 30) 

36 
">" :: "[o,o] => o" (infixr 25) 

37 
"<>" :: "[o,o] => o" (infixr 25) 

0  38 
(*Quantifiers*) 
1477  39 
All :: "('a => o) => o" (binder "ALL " 10) 
40 
Ex :: "('a => o) => o" (binder "EX " 10) 

41 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 

0  42 
(*Rewriting gadgets*) 
1477  43 
NORM :: "o => o" 
44 
norm :: "'a => 'a" 

0  45 

648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

46 
(*** Proof Term Formers: precedence must exceed 50 ***) 
1477  47 
tt :: "p" 
48 
contr :: "p=>p" 

49 
fst,snd :: "p=>p" 

50 
pair :: "[p,p]=>p" ("(1<_,/_>)") 

51 
split :: "[p, [p,p]=>p] =>p" 

52 
inl,inr :: "p=>p" 

53 
when :: "[p, p=>p, p=>p]=>p" 

54 
lambda :: "(p => p) => p" (binder "lam " 55) 

55 
"`" :: "[p,p]=>p" (infixl 60) 

648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

56 
alll :: "['a=>p]=>p" (binder "all " 55) 
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

57 
"^" :: "[p,'a]=>p" (infixl 55) 
1477  58 
exists :: "['a,p]=>p" ("(1[_,/_])") 
0  59 
xsplit :: "[p,['a,p]=>p]=>p" 
60 
ideq :: "'a=>p" 

61 
idpeel :: "[p,'a=>p]=>p" 

62 
nrm, NRM :: "p" 

63 

3942  64 
local 
65 

0  66 
rules 
67 

68 
(**** Propositional logic ****) 

69 

70 
(*Equality*) 

71 
(* Like Intensional Equality in MLTT  but proofs distinct from terms *) 

72 

1477  73 
ieqI "ideq(a) : a=a" 
3836  74 
ieqE "[ p : a=b; !!x. f(x) : P(x,x) ] ==> idpeel(p,f) : P(a,b)" 
0  75 

76 
(* Truth and Falsity *) 

77 

78 
TrueI "tt : True" 

79 
FalseE "a:False ==> contr(a):P" 

80 

81 
(* Conjunction *) 

82 

83 
conjI "[ a:P; b:Q ] ==> <a,b> : P&Q" 

84 
conjunct1 "p:P&Q ==> fst(p):P" 

85 
conjunct2 "p:P&Q ==> snd(p):Q" 

86 

87 
(* Disjunction *) 

88 

89 
disjI1 "a:P ==> inl(a):PQ" 

90 
disjI2 "b:Q ==> inr(b):PQ" 

3836  91 
disjE "[ a:PQ; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R 
1149  92 
] ==> when(a,f,g):R" 
0  93 

94 
(* Implication *) 

95 

3836  96 
impI "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P>Q" 
0  97 
mp "[ f:P>Q; a:P ] ==> f`a:Q" 
98 

99 
(*Quantifiers*) 

100 

3836  101 
allI "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" 
102 
spec "(f:ALL x. P(x)) ==> f^x : P(x)" 

0  103 

3836  104 
exI "p : P(x) ==> [x,p] : EX x. P(x)" 
105 
exE "[ p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R ] ==> xsplit(p,f):R" 

0  106 

107 
(**** Equality between proofs ****) 

108 

109 
prefl "a : P ==> a = a : P" 

110 
psym "a = b : P ==> b = a : P" 

111 
ptrans "[ a = b : P; b = c : P ] ==> a = c : P" 

112 

3836  113 
idpeelB "[ !!x. f(x) : P(x,x) ] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" 
0  114 

115 
fstB "a:P ==> fst(<a,b>) = a : P" 

116 
sndB "b:Q ==> snd(<a,b>) = b : Q" 

117 
pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" 

118 

3836  119 
whenBinl "[ a:P; !!x. x:P ==> f(x) : Q ] ==> when(inl(a),f,g) = f(a) : Q" 
120 
whenBinr "[ b:P; !!x. x:P ==> g(x) : Q ] ==> when(inr(b),f,g) = g(b) : Q" 

121 
plusEC "a:PQ ==> when(a,%x. inl(x),%y. inr(y)) = p : PQ" 

0  122 

3836  123 
applyB "[ a:P; !!x. x:P ==> b(x) : Q ] ==> (lam x. b(x)) ` a = b(a) : Q" 
124 
funEC "f:P ==> f = lam x. f`x : P" 

0  125 

3836  126 
specB "[ !!x. f(x) : P(x) ] ==> (all x. f(x)) ^ a = f(a) : P(a)" 
0  127 

128 

129 
(**** Definitions ****) 

130 

1477  131 
not_def "~P == P>False" 
0  132 
iff_def "P<>Q == (P>Q) & (Q>P)" 
133 

134 
(*Unique existence*) 

135 
ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 

136 

137 
(*Rewriting  special constants to flag normalized terms and formulae*) 

1477  138 
norm_eq "nrm : norm(x) = x" 
139 
NORM_iff "NRM : NORM(P) <> P" 

0  140 

141 
end 

142 

143 
ML 

144 

145 
(*show_proofs:=true displays the proof terms  they are ENORMOUS*) 

146 
val show_proofs = ref false; 

147 

148 
fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p; 

149 

150 
fun proof_tr' [P,p] = 

151 
if !show_proofs then Const("@Proof",dummyT) $ p $ P 

152 
else P (*this case discards the proof term*); 

153 

154 
val parse_translation = [("@Proof", proof_tr)]; 

155 
val print_translation = [("Proof", proof_tr')]; 

156 