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