author  wenzelm 
Fri, 10 Oct 1997 16:29:41 +0200  
changeset 3836  f1a1817659e6 
parent 2714  b0fbdfbbad66 
child 3942  1f1c1f524d19 
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 

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" 

2714  31 
Not :: "o => o" ("~ _" [40] 40) 
1477  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" 
3836  70 
ieqE "[ p : a=b; !!x. f(x) : P(x,x) ] ==> idpeel(p,f) : P(a,b)" 
0  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):PQ" 

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

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

90 
(* Implication *) 

91 

3836  92 
impI "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P>Q" 
0  93 
mp "[ f:P>Q; a:P ] ==> f`a:Q" 
94 

95 
(*Quantifiers*) 

96 

3836  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 

3836  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 

3836  109 
idpeelB "[ !!x. f(x) : P(x,x) ] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" 
0  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 

3836  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:PQ ==> when(a,%x. inl(x),%y. inr(y)) = p : PQ" 

0  118 

3836  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" 

0  121 

3836  122 
specB "[ !!x. f(x) : P(x) ] ==> (all x. f(x)) ^ a = f(a) : P(a)" 
0  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 