src/FOLP/IFOLP.thy
changeset 17480 fd19f77dcf60
parent 14854 61bdf2ae4dc5
child 26322 eaf634e975fa
--- 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 |] ==> <a,b> : P&Q"
-conjunct1 "p:P&Q ==> fst(p):P"
-conjunct2 "p:P&Q ==> snd(p):Q"
+conjI:     "[| a:P;  b:Q |] ==> <a,b> : 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,b>) = a : P"
-sndB      "b:Q ==> snd(<a,b>) = b : Q"
-pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
+fstB:      "a:P ==> fst(<a,b>) = a : P"
+sndB:      "b:Q ==> snd(<a,b>) = b : Q"
+pairEC:    "p:P&Q ==> p = <fst(p),snd(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')];
-