author  wenzelm 
Sun, 18 Sep 2005 14:25:48 +0200  
changeset 17480  fd19f77dcf60 
parent 14854  61bdf2ae4dc5 
child 26322  eaf634e975fa 
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 

17480  7 
header {* Intuitionistic FirstOrder Logic with Proofs *} 
8 

9 
theory IFOLP 

10 
imports Pure 

11 
begin 

0  12 

3942  13 
global 
14 

17480  15 
classes "term" 
16 
defaultsort "term" 

0  17 

17480  18 
typedecl p 
19 
typedecl o 

0  20 

17480  21 
consts 
0  22 
(*** Judgements ***) 
1477  23 
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) 
24 
Proof :: "[o,p]=>prop" 

0  25 
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) 
17480  26 

0  27 
(*** Logical Connectives  Type Formers ***) 
1477  28 
"=" :: "['a,'a] => o" (infixl 50) 
17480  29 
True :: "o" 
30 
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" 

17480  47 
fst :: "p=>p" 
48 
snd :: "p=>p" 

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

17480  51 
inl :: "p=>p" 
52 
inr :: "p=>p" 

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

17480  62 
nrm :: p 
63 
NRM :: p 

0  64 

3942  65 
local 
66 

17480  67 
ML {* 
68 

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

70 
val show_proofs = ref false; 

71 

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

73 

74 
fun proof_tr' [P,p] = 

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

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

77 
*} 

78 

79 
parse_translation {* [("@Proof", proof_tr)] *} 

80 
print_translation {* [("Proof", proof_tr')] *} 

81 

82 
axioms 

0  83 

84 
(**** Propositional logic ****) 

85 

86 
(*Equality*) 

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

88 

17480  89 
ieqI: "ideq(a) : a=a" 
90 
ieqE: "[ p : a=b; !!x. f(x) : P(x,x) ] ==> idpeel(p,f) : P(a,b)" 

0  91 

92 
(* Truth and Falsity *) 

93 

17480  94 
TrueI: "tt : True" 
95 
FalseE: "a:False ==> contr(a):P" 

0  96 

97 
(* Conjunction *) 

98 

17480  99 
conjI: "[ a:P; b:Q ] ==> <a,b> : P&Q" 
100 
conjunct1: "p:P&Q ==> fst(p):P" 

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

0  102 

103 
(* Disjunction *) 

104 

17480  105 
disjI1: "a:P ==> inl(a):PQ" 
106 
disjI2: "b:Q ==> inr(b):PQ" 

107 
disjE: "[ a:PQ; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R 

108 
] ==> when(a,f,g):R" 

0  109 

110 
(* Implication *) 

111 

17480  112 
impI: "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P>Q" 
113 
mp: "[ f:P>Q; a:P ] ==> f`a:Q" 

0  114 

115 
(*Quantifiers*) 

116 

17480  117 
allI: "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" 
118 
spec: "(f:ALL x. P(x)) ==> f^x : P(x)" 

0  119 

17480  120 
exI: "p : P(x) ==> [x,p] : EX x. P(x)" 
121 
exE: "[ p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R ] ==> xsplit(p,f):R" 

0  122 

123 
(**** Equality between proofs ****) 

124 

17480  125 
prefl: "a : P ==> a = a : P" 
126 
psym: "a = b : P ==> b = a : P" 

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

0  128 

17480  129 
idpeelB: "[ !!x. f(x) : P(x,x) ] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" 
0  130 

17480  131 
fstB: "a:P ==> fst(<a,b>) = a : P" 
132 
sndB: "b:Q ==> snd(<a,b>) = b : Q" 

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

0  134 

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

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

0  138 

17480  139 
applyB: "[ a:P; !!x. x:P ==> b(x) : Q ] ==> (lam x. b(x)) ` a = b(a) : Q" 
140 
funEC: "f:P ==> f = lam x. f`x : P" 

0  141 

17480  142 
specB: "[ !!x. f(x) : P(x) ] ==> (all x. f(x)) ^ a = f(a) : P(a)" 
0  143 

144 

145 
(**** Definitions ****) 

146 

17480  147 
not_def: "~P == P>False" 
148 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

0  149 

150 
(*Unique existence*) 

17480  151 
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 
0  152 

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

17480  154 
norm_eq: "nrm : norm(x) = x" 
155 
NORM_iff: "NRM : NORM(P) <> P" 

156 

157 
ML {* use_legacy_bindings (the_context ()) *} 

0  158 

159 
end 

160 

161 