# Theory IFOLP

Up to index of Isabelle/FOLP

theory IFOLP
imports Pure
uses [IFOLP.ML]
begin

    (*  Title:      FOLP/IFOLP.thy
        ID:         $Id: IFOLP.thy,v 1.12 2005/09/18 12:25:48 wenzelm Exp $
        Author:     Martin D Coen, Cambridge University Computer Laboratory
        Copyright   1992  University of Cambridge
    *)

    header {* Intuitionistic First-Order Logic with Proofs *}

    theory IFOLP
    imports Pure
    begin

    global

    classes "term"
    defaultsort "term"

    typedecl p
    typedecl o

    consts
          (*** Judgements ***)
     "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
     Proof          ::   "[o,p]=>prop"
     EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)

          (*** Logical Connectives -- Type Formers ***)
     "="            ::      "['a,'a] => o"  (infixl 50)
     True           ::      "o"
     False          ::      "o"
     Not            ::      "o => o"        ("~ _" [40] 40)
     "&"            ::      "[o,o] => o"    (infixr 35)
     "|"            ::      "[o,o] => o"    (infixr 30)
     "-->"          ::      "[o,o] => o"    (infixr 25)
     "<->"          ::      "[o,o] => o"    (infixr 25)
          (*Quantifiers*)
     All            ::      "('a => o) => o"        (binder "ALL " 10)
     Ex             ::      "('a => o) => o"        (binder "EX " 10)
     Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
          (*Rewriting gadgets*)
     NORM           ::      "o => o"
     norm           ::      "'a => 'a"

          (*** Proof Term Formers: precedence must exceed 50 ***)
     tt             :: "p"
     contr          :: "p=>p"
     fst            :: "p=>p"
     snd            :: "p=>p"
     pair           :: "[p,p]=>p"           ("(1<_,/_>)")
     split          :: "[p, [p,p]=>p] =>p"
     inl            :: "p=>p"
     inr            :: "p=>p"
     when           :: "[p, p=>p, p=>p]=>p"
     lambda         :: "(p => p) => p"      (binder "lam " 55)
     "`"            :: "[p,p]=>p"           (infixl 60)
     alll           :: "['a=>p]=>p"         (binder "all " 55)
     "^"            :: "[p,'a]=>p"          (infixl 55)
     exists         :: "['a,p]=>p"          ("(1[_,/_])")
     xsplit         :: "[p,['a,p]=>p]=>p"
     ideq           :: "'a=>p"
     idpeel         :: "[p,'a=>p]=>p"
     nrm            :: p
     NRM            :: p

    local

    ML {*

    (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    val show_proofs = ref false;

    fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;

    fun proof_tr' [P,p] =
        if !show_proofs then Const("@Proof",dummyT) $ p $ P
        else P  (*this case discards the proof term*);
    *}

    parse_translation {* [("@Proof", proof_tr)] *}
    print_translation {* [("Proof", proof_tr')] *}

    axioms

    (**** Propositional logic ****)

    (*Equality*)
    (* Like Intensional Equality in MLTT - but proofs distinct from terms *)

    ieqI:      "ideq(a) : a=a"
    ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"

    (* Truth and Falsity *)

    TrueI:     "tt : True"
    FalseE:    "a:False ==> contr(a):P"

    (* Conjunction *)

    conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
    conjunct1: "p:P&Q ==> fst(p):P"
    conjunct2: "p:P&Q ==> snd(p):Q"

    (* Disjunction *)

    disjI1:    "a:P ==> inl(a):P|Q"
    disjI2:    "b:Q ==> inr(b):P|Q"
    disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
               |] ==> when(a,f,g):R"

    (* Implication *)

    impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
    mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"

    (*Quantifiers*)

    allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
    spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"

    exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
    exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"

    (**** Equality between proofs ****)

    prefl:     "a : P ==> a = a : P"
    psym:      "a = b : P ==> b = a : P"
    ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"

    idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"

    fstB:      "a:P ==> fst(<a,b>) = a : P"
    sndB:      "b:Q ==> snd(<a,b>) = b : Q"
    pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"

    whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
    whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
    plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"

    applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
    funEC:      "f:P ==> f = lam x. f`x : P"

    specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"

    (**** Definitions ****)

    not_def:              "~P == P-->False"
    iff_def:         "P<->Q == (P-->Q) & (Q-->P)"

    (*Unique existence*)
    ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"

    (*Rewriting -- special constants to flag normalized terms and formulae*)
    norm_eq: "nrm : norm(x) = x"
    NORM_iff:        "NRM : NORM(P) <-> P"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem conjE:

      [| P & Q; !!x y. [| P; Q |] ==> R |] ==> R

theorem impE:

      [| P --> Q; P; !!x. Q ==> R |] ==> R

theorem allE:

      [| ALL x. P(x); !!y. P(x) ==> R |] ==> R

theorem all_dupE:

      [| ALL x. P(x); !!y z. [| P(x); ALL x. P(x) |] ==> R |] ==> R

theorem not_to_imp:

      [| ~ P; !!x. P --> False ==> Q |] ==> Q

theorem rev_mp:

      [| P; P --> Q |] ==> Q

theorem contrapos:

      [| ~ Q; !!y. P ==> Q |] ==> ~ P

theorem iff_refl:

      P <-> P

theorem iff_sym:

      Q <-> P ==> P <-> Q

theorem iff_trans:

      [| P <-> Q; Q <-> R |] ==> P <-> R

theorem ex1I:

      [| P(a); !!x u. P(x) ==> x = a |] ==> EX! x. P(x)

theorem ex1E:

      [| EX! x. P(x); !!x u v. [| P(x); ALL y. P(y) --> y = x |] ==> R |] ==> R

theorem sym:

      a = b ==> b = a

theorem trans:

      [| a = b; b = c |] ==> a = c

theorem not_sym:

      ~ b = a ==> ~ a = b

theorem ex1_equalsE:

      [| EX! x. P(x); P(a); P(b) |] ==> a = b

theorem subst_context:

      a = b ==> t(a) = t(b)

theorem subst_context2:

      [| a = b; c = d |] ==> t(a, c) = t(b, d)

theorem subst_context3:

      [| a = b; c = d; e = f |] ==> t(a, c, e) = t(b, d, f)

theorem box_equals:

      [| a = b; a = c; b = d |] ==> c = d

theorem simp_equals:

      [| a = c; b = d; c = d |] ==> a = b

theorem pred1_cong:

      a = a' ==> P(a) <-> P(a')

theorem pred2_cong:

      [| a = a'; b = b' |] ==> P(a, b) <-> P(a', b')

theorem pred3_cong:

      [| a = a'; b = b'; c = c' |] ==> P(a, b, c) <-> P(a', b', c')

theorem conj_impE:

      [| P & Q --> S; !!x. P --> Q --> S ==> R |] ==> R

theorem disj_impE:

      [| P | Q --> S; !!x y. [| P --> S; Q --> S |] ==> R |] ==> R

theorem imp_impE:

      [| (P --> Q) --> S; !!x y. [| P; Q --> S |] ==> Q; !!x. S ==> R |] ==> R

theorem not_impE:

      [| ~ P --> S; !!y. P ==> False; !!y. S ==> R |] ==> R

theorem iff_impE:

      [| (P <-> Q) --> S; !!x y. [| P; Q --> S |] ==> Q;
         !!x y. [| Q; P --> S |] ==> P; !!x. S ==> R |]
      ==> R

theorem all_impE:

      [| (ALL x. P(x)) --> S; !!x. P(x); !!y. S ==> R |] ==> R

theorem ex_impE:

      [| (EX x. P(x)) --> S; !!y. P(a) --> S ==> R |] ==> R