src/ZF/ex/PropLog.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 753 ec86863e87c8
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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 + Univ +
    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 rules
    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