src/FOLP/IFOLP.thy
author wenzelm
Tue Jun 01 12:33:50 2004 +0200 (2004-06-01)
changeset 14854 61bdf2ae4dc5
parent 6509 9f7f4fd05b1f
child 17480 fd19f77dcf60
permissions -rw-r--r--
removed obsolete sort 'logic';
     1 (*  Title:      FOLP/IFOLP.thy
     2     ID:         $Id$
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Intuitionistic First-Order Logic with Proofs
     7 *)
     8 
     9 IFOLP = Pure +
    10 
    11 global
    12 
    13 classes term
    14 default term
    15 
    16 types
    17   p
    18   o
    19 
    20 consts  
    21       (*** Judgements ***)
    22  "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
    23  Proof          ::   "[o,p]=>prop"
    24  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    25         
    26       (*** Logical Connectives -- Type Formers ***)
    27  "="            ::      "['a,'a] => o"  (infixl 50)
    28  True,False     ::      "o"
    29  Not            ::      "o => o"        ("~ _" [40] 40)
    30  "&"            ::      "[o,o] => o"    (infixr 35)
    31  "|"            ::      "[o,o] => o"    (infixr 30)
    32  "-->"          ::      "[o,o] => o"    (infixr 25)
    33  "<->"          ::      "[o,o] => o"    (infixr 25)
    34       (*Quantifiers*)
    35  All            ::      "('a => o) => o"        (binder "ALL " 10)
    36  Ex             ::      "('a => o) => o"        (binder "EX " 10)
    37  Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
    38       (*Rewriting gadgets*)
    39  NORM           ::      "o => o"
    40  norm           ::      "'a => 'a"
    41 
    42       (*** Proof Term Formers: precedence must exceed 50 ***)
    43  tt             :: "p"
    44  contr          :: "p=>p"
    45  fst,snd        :: "p=>p"
    46  pair           :: "[p,p]=>p"           ("(1<_,/_>)")
    47  split          :: "[p, [p,p]=>p] =>p"
    48  inl,inr        :: "p=>p"
    49  when           :: "[p, p=>p, p=>p]=>p"
    50  lambda         :: "(p => p) => p"      (binder "lam " 55)
    51  "`"            :: "[p,p]=>p"           (infixl 60)
    52  alll           :: "['a=>p]=>p"         (binder "all " 55)
    53  "^"            :: "[p,'a]=>p"          (infixl 55)
    54  exists         :: "['a,p]=>p"          ("(1[_,/_])")
    55  xsplit         :: "[p,['a,p]=>p]=>p"
    56  ideq           :: "'a=>p"
    57  idpeel         :: "[p,'a=>p]=>p"
    58  nrm, NRM       :: "p"
    59 
    60 local
    61 
    62 rules
    63 
    64 (**** Propositional logic ****)
    65 
    66 (*Equality*)
    67 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    68 
    69 ieqI      "ideq(a) : a=a"
    70 ieqE      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    71 
    72 (* Truth and Falsity *)
    73 
    74 TrueI     "tt : True"
    75 FalseE    "a:False ==> contr(a):P"
    76 
    77 (* Conjunction *)
    78 
    79 conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
    80 conjunct1 "p:P&Q ==> fst(p):P"
    81 conjunct2 "p:P&Q ==> snd(p):Q"
    82 
    83 (* Disjunction *)
    84 
    85 disjI1    "a:P ==> inl(a):P|Q"
    86 disjI2    "b:Q ==> inr(b):P|Q"
    87 disjE     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R 
    88           |] ==> when(a,f,g):R"
    89 
    90 (* Implication *)
    91 
    92 impI      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
    93 mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
    94 
    95 (*Quantifiers*)
    96 
    97 allI      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
    98 spec      "(f:ALL x. P(x)) ==> f^x : P(x)"
    99 
   100 exI       "p : P(x) ==> [x,p] : EX x. P(x)"
   101 exE       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   102 
   103 (**** Equality between proofs ****)
   104 
   105 prefl     "a : P ==> a = a : P"
   106 psym      "a = b : P ==> b = a : P"
   107 ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
   108 
   109 idpeelB   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   110 
   111 fstB      "a:P ==> fst(<a,b>) = a : P"
   112 sndB      "b:Q ==> snd(<a,b>) = b : Q"
   113 pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   114 
   115 whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   116 whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   117 plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
   118 
   119 applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
   120 funEC      "f:P ==> f = lam x. f`x : P"
   121 
   122 specB      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
   123 
   124 
   125 (**** Definitions ****)
   126 
   127 not_def              "~P == P-->False"
   128 iff_def         "P<->Q == (P-->Q) & (Q-->P)"
   129 
   130 (*Unique existence*)
   131 ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   132 
   133 (*Rewriting -- special constants to flag normalized terms and formulae*)
   134 norm_eq "nrm : norm(x) = x"
   135 NORM_iff        "NRM : NORM(P) <-> P"
   136 
   137 end
   138 
   139 ML
   140 
   141 (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
   142 val show_proofs = ref false;
   143 
   144 fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
   145 
   146 fun proof_tr' [P,p] = 
   147     if !show_proofs then Const("@Proof",dummyT) $ p $ P 
   148     else P  (*this case discards the proof term*);
   149 
   150 val  parse_translation = [("@Proof", proof_tr)];
   151 val print_translation  = [("Proof", proof_tr')];
   152