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')]; -