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
lcp@515
     1
(*  Title: 	ZF/ex/PropLog.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     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@515
    10
PropLog = Finite + Univ +
lcp@515
    11
lcp@515
    12
(** The datatype of propositions; note mixfix syntax **)
clasohm@0
    13
consts
lcp@515
    14
  prop     :: "i"
clasohm@0
    15
lcp@515
    16
datatype
lcp@515
    17
  "prop" = Fls
lcp@515
    18
         | Var ("n: nat")	                ("#_" [100] 100)
lcp@515
    19
         | "=>" ("p: prop", "q: prop")		(infixr 90)
lcp@515
    20
lcp@515
    21
(** The proof system **)
lcp@515
    22
consts
clasohm@0
    23
  thms     :: "i => i"
clasohm@0
    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
lcp@515
    42
  prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
lcp@515
    43
  is_true  :: "[i,i] => o"
lcp@515
    44
  "|="     :: "[i,i] => o"    			(infixl 50)
lcp@515
    45
  hyps     :: "[i,i] => i"
lcp@515
    46
clasohm@0
    47
rules
clasohm@0
    48
clasohm@0
    49
  prop_rec_def
clasohm@0
    50
   "prop_rec(p,b,c,h) == \
clasohm@0
    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@0
    55
   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), \
clasohm@0
    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@0
    64
   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, \
clasohm@0
    65
\                            %p q Hp Hq. Hp Un Hq)"
clasohm@0
    66
clasohm@0
    67
end