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