src/FOLP/IFOLP.thy
changeset 17480 fd19f77dcf60
parent 14854 61bdf2ae4dc5
child 26322 eaf634e975fa
     1.1 --- a/src/FOLP/IFOLP.thy	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -2,30 +2,32 @@
     1.4      ID:         $Id$
     1.5      Author:     Martin D Coen, Cambridge University Computer Laboratory
     1.6      Copyright   1992  University of Cambridge
     1.7 -
     1.8 -Intuitionistic First-Order Logic with Proofs
     1.9  *)
    1.10  
    1.11 -IFOLP = Pure +
    1.12 +header {* Intuitionistic First-Order Logic with Proofs *}
    1.13 +
    1.14 +theory IFOLP
    1.15 +imports Pure
    1.16 +begin
    1.17  
    1.18  global
    1.19  
    1.20 -classes term
    1.21 -default term
    1.22 +classes "term"
    1.23 +defaultsort "term"
    1.24  
    1.25 -types
    1.26 -  p
    1.27 -  o
    1.28 +typedecl p
    1.29 +typedecl o
    1.30  
    1.31 -consts  
    1.32 +consts
    1.33        (*** Judgements ***)
    1.34   "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
    1.35   Proof          ::   "[o,p]=>prop"
    1.36   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    1.37 -        
    1.38 +
    1.39        (*** Logical Connectives -- Type Formers ***)
    1.40   "="            ::      "['a,'a] => o"  (infixl 50)
    1.41 - True,False     ::      "o"
    1.42 + True           ::      "o"
    1.43 + False          ::      "o"
    1.44   Not            ::      "o => o"        ("~ _" [40] 40)
    1.45   "&"            ::      "[o,o] => o"    (infixr 35)
    1.46   "|"            ::      "[o,o] => o"    (infixr 30)
    1.47 @@ -42,10 +44,12 @@
    1.48        (*** Proof Term Formers: precedence must exceed 50 ***)
    1.49   tt             :: "p"
    1.50   contr          :: "p=>p"
    1.51 - fst,snd        :: "p=>p"
    1.52 + fst            :: "p=>p"
    1.53 + snd            :: "p=>p"
    1.54   pair           :: "[p,p]=>p"           ("(1<_,/_>)")
    1.55   split          :: "[p, [p,p]=>p] =>p"
    1.56 - inl,inr        :: "p=>p"
    1.57 + inl            :: "p=>p"
    1.58 + inr            :: "p=>p"
    1.59   when           :: "[p, p=>p, p=>p]=>p"
    1.60   lambda         :: "(p => p) => p"      (binder "lam " 55)
    1.61   "`"            :: "[p,p]=>p"           (infixl 60)
    1.62 @@ -55,98 +59,103 @@
    1.63   xsplit         :: "[p,['a,p]=>p]=>p"
    1.64   ideq           :: "'a=>p"
    1.65   idpeel         :: "[p,'a=>p]=>p"
    1.66 - nrm, NRM       :: "p"
    1.67 + nrm            :: p
    1.68 + NRM            :: p
    1.69  
    1.70  local
    1.71  
    1.72 -rules
    1.73 +ML {*
    1.74 +
    1.75 +(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    1.76 +val show_proofs = ref false;
    1.77 +
    1.78 +fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
    1.79 +
    1.80 +fun proof_tr' [P,p] =
    1.81 +    if !show_proofs then Const("@Proof",dummyT) $ p $ P
    1.82 +    else P  (*this case discards the proof term*);
    1.83 +*}
    1.84 +
    1.85 +parse_translation {* [("@Proof", proof_tr)] *}
    1.86 +print_translation {* [("Proof", proof_tr')] *}
    1.87 +
    1.88 +axioms
    1.89  
    1.90  (**** Propositional logic ****)
    1.91  
    1.92  (*Equality*)
    1.93  (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    1.94  
    1.95 -ieqI      "ideq(a) : a=a"
    1.96 -ieqE      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    1.97 +ieqI:      "ideq(a) : a=a"
    1.98 +ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    1.99  
   1.100  (* Truth and Falsity *)
   1.101  
   1.102 -TrueI     "tt : True"
   1.103 -FalseE    "a:False ==> contr(a):P"
   1.104 +TrueI:     "tt : True"
   1.105 +FalseE:    "a:False ==> contr(a):P"
   1.106  
   1.107  (* Conjunction *)
   1.108  
   1.109 -conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
   1.110 -conjunct1 "p:P&Q ==> fst(p):P"
   1.111 -conjunct2 "p:P&Q ==> snd(p):Q"
   1.112 +conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
   1.113 +conjunct1: "p:P&Q ==> fst(p):P"
   1.114 +conjunct2: "p:P&Q ==> snd(p):Q"
   1.115  
   1.116  (* Disjunction *)
   1.117  
   1.118 -disjI1    "a:P ==> inl(a):P|Q"
   1.119 -disjI2    "b:Q ==> inr(b):P|Q"
   1.120 -disjE     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R 
   1.121 -          |] ==> when(a,f,g):R"
   1.122 +disjI1:    "a:P ==> inl(a):P|Q"
   1.123 +disjI2:    "b:Q ==> inr(b):P|Q"
   1.124 +disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
   1.125 +           |] ==> when(a,f,g):R"
   1.126  
   1.127  (* Implication *)
   1.128  
   1.129 -impI      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
   1.130 -mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
   1.131 +impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
   1.132 +mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
   1.133  
   1.134  (*Quantifiers*)
   1.135  
   1.136 -allI      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
   1.137 -spec      "(f:ALL x. P(x)) ==> f^x : P(x)"
   1.138 +allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
   1.139 +spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
   1.140  
   1.141 -exI       "p : P(x) ==> [x,p] : EX x. P(x)"
   1.142 -exE       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   1.143 +exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
   1.144 +exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   1.145  
   1.146  (**** Equality between proofs ****)
   1.147  
   1.148 -prefl     "a : P ==> a = a : P"
   1.149 -psym      "a = b : P ==> b = a : P"
   1.150 -ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
   1.151 +prefl:     "a : P ==> a = a : P"
   1.152 +psym:      "a = b : P ==> b = a : P"
   1.153 +ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
   1.154  
   1.155 -idpeelB   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   1.156 +idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   1.157  
   1.158 -fstB      "a:P ==> fst(<a,b>) = a : P"
   1.159 -sndB      "b:Q ==> snd(<a,b>) = b : Q"
   1.160 -pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   1.161 +fstB:      "a:P ==> fst(<a,b>) = a : P"
   1.162 +sndB:      "b:Q ==> snd(<a,b>) = b : Q"
   1.163 +pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   1.164  
   1.165 -whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   1.166 -whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   1.167 -plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
   1.168 +whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   1.169 +whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   1.170 +plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
   1.171  
   1.172 -applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
   1.173 -funEC      "f:P ==> f = lam x. f`x : P"
   1.174 +applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
   1.175 +funEC:      "f:P ==> f = lam x. f`x : P"
   1.176  
   1.177 -specB      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
   1.178 +specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
   1.179  
   1.180  
   1.181  (**** Definitions ****)
   1.182  
   1.183 -not_def              "~P == P-->False"
   1.184 -iff_def         "P<->Q == (P-->Q) & (Q-->P)"
   1.185 +not_def:              "~P == P-->False"
   1.186 +iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
   1.187  
   1.188  (*Unique existence*)
   1.189 -ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   1.190 +ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   1.191  
   1.192  (*Rewriting -- special constants to flag normalized terms and formulae*)
   1.193 -norm_eq "nrm : norm(x) = x"
   1.194 -NORM_iff        "NRM : NORM(P) <-> P"
   1.195 +norm_eq: "nrm : norm(x) = x"
   1.196 +NORM_iff:        "NRM : NORM(P) <-> P"
   1.197 +
   1.198 +ML {* use_legacy_bindings (the_context ()) *}
   1.199  
   1.200  end
   1.201  
   1.202 -ML
   1.203  
   1.204 -(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
   1.205 -val show_proofs = ref false;
   1.206 -
   1.207 -fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
   1.208 -
   1.209 -fun proof_tr' [P,p] = 
   1.210 -    if !show_proofs then Const("@Proof",dummyT) $ p $ P 
   1.211 -    else P  (*this case discards the proof term*);
   1.212 -
   1.213 -val  parse_translation = [("@Proof", proof_tr)];
   1.214 -val print_translation  = [("Proof", proof_tr')];
   1.215 -