src/ZF/ex/proplog.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 0 a5a9c433f639
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/prop-log.thy
     2     ID:         $Id$
     3     Author: 	Tobias Nipkow & Lawrence C Paulson
     4     Copyright   1993  University of Cambridge
     5 
     6 Inductive definition of propositional logic.
     7 *)
     8 
     9 PropLog = Prop + Fin +
    10 consts
    11   (*semantics*)
    12   prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
    13   is_true  :: "[i,i] => o"
    14   "|="     :: "[i,i] => o"    			(infixl 50)
    15   hyps     :: "[i,i] => i"
    16 
    17   (*proof theory*)
    18   thms     :: "i => i"
    19   "|-"     :: "[i,i] => o"    			(infixl 50)
    20 
    21 translations
    22   "H |- p" == "p : thms(H)"
    23 
    24 rules
    25 
    26   prop_rec_def
    27    "prop_rec(p,b,c,h) == \
    28 \   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
    29 
    30   (** Semantics of propositional logic **)
    31   is_true_def
    32    "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), \
    33 \                               %p q tp tq. if(tp=1,tq,1))         =  1"
    34 
    35   (*For every valuation, if all elements of H are true then so is p*)
    36   sat_def     "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"
    37 
    38   (** A finite set of hypotheses from t and the Vars in p **)
    39   hyps_def
    40    "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, \
    41 \                            %p q Hp Hq. Hp Un Hq)"
    42 
    43 end