src/ZF/ex/PropLog.thy

expanded tabs

(*  Title:      ZF/ex/PropLog.thy
    ID:         $Id$
    Author:     Tobias Nipkow & Lawrence C Paulson
    Copyright   1993  University of Cambridge

Datatype definition of propositional logic formulae and inductive definition
of the propositional tautologies.
*)

PropLog = Finite + Datatype +

(** The datatype of propositions; note mixfix syntax **)
consts
  prop     :: i

datatype
  "prop" = Fls
         | Var ("n: nat")                       ("#_" [100] 100)
         | "=>" ("p: prop", "q: prop")          (infixr 90)

(** The proof system **)
consts
  thms     :: i => i
  "|-"     :: [i,i] => o                        (infixl 50)

translations
  "H |- p" == "p : thms(H)"

inductive
  domains "thms(H)" <= "prop"
  intrs
    H  "[| p:H;  p:prop |] ==> H |- p"
    K  "[| p:prop;  q:prop |] ==> H |- p=>q=>p"
    S  "[| p:prop;  q:prop;  r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
    DN "p:prop ==> H |- ((p=>Fls) => Fls) => p"
    MP "[| H |- p=>q;  H |- p;  p:prop;  q:prop |] ==> H |- q"
  type_intrs "prop.intrs"


(** The semantics **)
consts
  prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
  is_true  :: [i,i] => o
  "|="     :: [i,i] => o                        (infixl 50)
  hyps     :: [i,i] => i

defs

  prop_rec_def
   "prop_rec(p,b,c,h) == 
   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"

  (** Semantics of propositional logic **)
  is_true_def
   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), 
                               %p q tp tq. if(tp=1,tq,1))         =  1"

  (*Logical consequence: for every valuation, if all elements of H are true
     then so is p*)
  logcon_def  "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"

  (** A finite set of hypotheses from t and the Vars in p **)
  hyps_def
   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, 
                            %p q Hp Hq. Hp Un Hq)"

end