diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IFOLP.thy Sun Sep 18 14:25:48 2005 +0200
@@ -2,30 +2,32 @@
ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Intuitionistic First-Order Logic with Proofs
*)
-IFOLP = Pure +
+header {* Intuitionistic First-Order Logic with Proofs *}
+
+theory IFOLP
+imports Pure
+begin
global
-classes term
-default term
+classes "term"
+defaultsort "term"
-types
- p
- o
+typedecl p
+typedecl o
-consts
+consts
(*** Judgements ***)
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5)
Proof :: "[o,p]=>prop"
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
-
+
(*** Logical Connectives -- Type Formers ***)
"=" :: "['a,'a] => o" (infixl 50)
- True,False :: "o"
+ True :: "o"
+ False :: "o"
Not :: "o => o" ("~ _" [40] 40)
"&" :: "[o,o] => o" (infixr 35)
"|" :: "[o,o] => o" (infixr 30)
@@ -42,10 +44,12 @@
(*** Proof Term Formers: precedence must exceed 50 ***)
tt :: "p"
contr :: "p=>p"
- fst,snd :: "p=>p"
+ fst :: "p=>p"
+ snd :: "p=>p"
pair :: "[p,p]=>p" ("(1<_,/_>)")
split :: "[p, [p,p]=>p] =>p"
- inl,inr :: "p=>p"
+ inl :: "p=>p"
+ inr :: "p=>p"
when :: "[p, p=>p, p=>p]=>p"
lambda :: "(p => p) => p" (binder "lam " 55)
"`" :: "[p,p]=>p" (infixl 60)
@@ -55,98 +59,103 @@
xsplit :: "[p,['a,p]=>p]=>p"
ideq :: "'a=>p"
idpeel :: "[p,'a=>p]=>p"
- nrm, NRM :: "p"
+ nrm :: p
+ NRM :: p
local
-rules
+ML {*
+
+(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
+val show_proofs = ref false;
+
+fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
+
+fun proof_tr' [P,p] =
+ if !show_proofs then Const("@Proof",dummyT) $ p $ P
+ else P (*this case discards the proof term*);
+*}
+
+parse_translation {* [("@Proof", proof_tr)] *}
+print_translation {* [("Proof", proof_tr')] *}
+
+axioms
(**** Propositional logic ****)
(*Equality*)
(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
-ieqI "ideq(a) : a=a"
-ieqE "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
+ieqI: "ideq(a) : a=a"
+ieqE: "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
(* Truth and Falsity *)
-TrueI "tt : True"
-FalseE "a:False ==> contr(a):P"
+TrueI: "tt : True"
+FalseE: "a:False ==> contr(a):P"
(* Conjunction *)
-conjI "[| a:P; b:Q |] ==> : P&Q"
-conjunct1 "p:P&Q ==> fst(p):P"
-conjunct2 "p:P&Q ==> snd(p):Q"
+conjI: "[| a:P; b:Q |] ==> : P&Q"
+conjunct1: "p:P&Q ==> fst(p):P"
+conjunct2: "p:P&Q ==> snd(p):Q"
(* Disjunction *)
-disjI1 "a:P ==> inl(a):P|Q"
-disjI2 "b:Q ==> inr(b):P|Q"
-disjE "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
- |] ==> when(a,f,g):R"
+disjI1: "a:P ==> inl(a):P|Q"
+disjI2: "b:Q ==> inr(b):P|Q"
+disjE: "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
+ |] ==> when(a,f,g):R"
(* Implication *)
-impI "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
-mp "[| f:P-->Q; a:P |] ==> f`a:Q"
+impI: "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
+mp: "[| f:P-->Q; a:P |] ==> f`a:Q"
(*Quantifiers*)
-allI "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
-spec "(f:ALL x. P(x)) ==> f^x : P(x)"
+allI: "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
+spec: "(f:ALL x. P(x)) ==> f^x : P(x)"
-exI "p : P(x) ==> [x,p] : EX x. P(x)"
-exE "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
+exI: "p : P(x) ==> [x,p] : EX x. P(x)"
+exE: "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
(**** Equality between proofs ****)
-prefl "a : P ==> a = a : P"
-psym "a = b : P ==> b = a : P"
-ptrans "[| a = b : P; b = c : P |] ==> a = c : P"
+prefl: "a : P ==> a = a : P"
+psym: "a = b : P ==> b = a : P"
+ptrans: "[| a = b : P; b = c : P |] ==> a = c : P"
-idpeelB "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
+idpeelB: "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
-fstB "a:P ==> fst() = a : P"
-sndB "b:Q ==> snd() = b : Q"
-pairEC "p:P&Q ==> p = : P&Q"
+fstB: "a:P ==> fst() = a : P"
+sndB: "b:Q ==> snd() = b : Q"
+pairEC: "p:P&Q ==> p = : P&Q"
-whenBinl "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
-whenBinr "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
-plusEC "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
+whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
+whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
+plusEC: "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
-applyB "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
-funEC "f:P ==> f = lam x. f`x : P"
+applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
+funEC: "f:P ==> f = lam x. f`x : P"
-specB "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
+specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
(**** Definitions ****)
-not_def "~P == P-->False"
-iff_def "P<->Q == (P-->Q) & (Q-->P)"
+not_def: "~P == P-->False"
+iff_def: "P<->Q == (P-->Q) & (Q-->P)"
(*Unique existence*)
-ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
(*Rewriting -- special constants to flag normalized terms and formulae*)
-norm_eq "nrm : norm(x) = x"
-NORM_iff "NRM : NORM(P) <-> P"
+norm_eq: "nrm : norm(x) = x"
+NORM_iff: "NRM : NORM(P) <-> P"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
-ML
-(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
-val show_proofs = ref false;
-
-fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
-
-fun proof_tr' [P,p] =
- if !show_proofs then Const("@Proof",dummyT) $ p $ P
- else P (*this case discards the proof term*);
-
-val parse_translation = [("@Proof", proof_tr)];
-val print_translation = [("Proof", proof_tr')];
-