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