src/ZF/ex/PropLog.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/ex/PropLog.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Tobias Nipkow & Lawrence C Paulson
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
lcp@515
     6
Datatype definition of propositional logic formulae and inductive definition
lcp@515
     7
of the propositional tautologies.
clasohm@0
     8
*)
clasohm@0
     9
lcp@935
    10
PropLog = Finite + Datatype +
lcp@515
    11
lcp@515
    12
(** The datatype of propositions; note mixfix syntax **)
clasohm@0
    13
consts
clasohm@1401
    14
  prop     :: i
clasohm@0
    15
lcp@515
    16
datatype
lcp@515
    17
  "prop" = Fls
clasohm@1478
    18
         | Var ("n: nat")                       ("#_" [100] 100)
clasohm@1478
    19
         | "=>" ("p: prop", "q: prop")          (infixr 90)
lcp@515
    20
lcp@515
    21
(** The proof system **)
lcp@515
    22
consts
clasohm@1401
    23
  thms     :: i => i
clasohm@1478
    24
  "|-"     :: [i,i] => o                        (infixl 50)
clasohm@0
    25
clasohm@0
    26
translations
clasohm@0
    27
  "H |- p" == "p : thms(H)"
clasohm@0
    28
lcp@515
    29
inductive
lcp@515
    30
  domains "thms(H)" <= "prop"
lcp@515
    31
  intrs
lcp@515
    32
    H  "[| p:H;  p:prop |] ==> H |- p"
lcp@515
    33
    K  "[| p:prop;  q:prop |] ==> H |- p=>q=>p"
lcp@515
    34
    S  "[| p:prop;  q:prop;  r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
lcp@515
    35
    DN "p:prop ==> H |- ((p=>Fls) => Fls) => p"
lcp@515
    36
    MP "[| H |- p=>q;  H |- p;  p:prop;  q:prop |] ==> H |- q"
lcp@515
    37
  type_intrs "prop.intrs"
lcp@515
    38
lcp@515
    39
lcp@515
    40
(** The semantics **)
lcp@515
    41
consts
clasohm@1401
    42
  prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
clasohm@1401
    43
  is_true  :: [i,i] => o
clasohm@1478
    44
  "|="     :: [i,i] => o                        (infixl 50)
clasohm@1401
    45
  hyps     :: [i,i] => i
lcp@515
    46
lcp@753
    47
defs
clasohm@0
    48
clasohm@0
    49
  prop_rec_def
clasohm@1155
    50
   "prop_rec(p,b,c,h) == 
clasohm@1155
    51
   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
clasohm@0
    52
clasohm@0
    53
  (** Semantics of propositional logic **)
clasohm@0
    54
  is_true_def
clasohm@1155
    55
   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), 
clasohm@1155
    56
                               %p q tp tq. if(tp=1,tq,1))         =  1"
clasohm@0
    57
lcp@501
    58
  (*Logical consequence: for every valuation, if all elements of H are true
lcp@501
    59
     then so is p*)
lcp@501
    60
  logcon_def  "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"
clasohm@0
    61
clasohm@0
    62
  (** A finite set of hypotheses from t and the Vars in p **)
clasohm@0
    63
  hyps_def
clasohm@1155
    64
   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, 
clasohm@1155
    65
                            %p q Hp Hq. Hp Un Hq)"
clasohm@0
    66
clasohm@0
    67
end