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