src/FOL/IFOL.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 35 d71f96f1780e
permissions -rw-r--r--
Initial revision
     1 IFOL = Pure + 
     2 
     3 classes term < logic
     4 
     5 default term
     6 
     7 types o 0
     8 
     9 arities o :: logic
    10 
    11 consts	
    12     Trueprop	::	"o => prop"		("(_)" [0] 5)
    13     True,False	::	"o"
    14   (*Connectives*)
    15     "="		::	"['a,'a] => o"		(infixl 50)
    16     Not		::	"o => o"		("~ _" [40] 40)
    17     "&"		::	"[o,o] => o"		(infixr 35)
    18     "|"		::	"[o,o] => o"		(infixr 30)
    19     "-->"	::	"[o,o] => o"		(infixr 25)
    20     "<->"	::	"[o,o] => o"		(infixr 25)
    21   (*Quantifiers*)
    22     All		::	"('a => o) => o"	(binder "ALL " 10)
    23     Ex		::	"('a => o) => o"	(binder "EX " 10)
    24     Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    25 
    26 rules
    27 
    28   (*Equality*)
    29 
    30 refl		"a=a"
    31 subst		"[| a=b;  P(a) |] ==> P(b)"
    32 
    33   (*Propositional logic*)
    34 
    35 conjI		"[| P;  Q |] ==> P&Q"
    36 conjunct1	"P&Q ==> P"
    37 conjunct2	"P&Q ==> Q"
    38 
    39 disjI1		"P ==> P|Q"
    40 disjI2		"Q ==> P|Q"
    41 disjE		"[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    42 
    43 impI		"(P ==> Q) ==> P-->Q"
    44 mp		"[| P-->Q;  P |] ==> Q"
    45 
    46 FalseE		"False ==> P"
    47 
    48   (*Definitions*)
    49 
    50 True_def	"True == False-->False"
    51 not_def		"~P == P-->False"
    52 iff_def		"P<->Q == (P-->Q) & (Q-->P)"
    53 
    54   (*Unique existence*)
    55 ex1_def		"EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    56 
    57   (*Quantifiers*)
    58 
    59 allI		"(!!x. P(x)) ==> (ALL x.P(x))"
    60 spec		"(ALL x.P(x)) ==> P(x)"
    61 
    62 exI		"P(x) ==> (EX x.P(x))"
    63 exE		"[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
    64 
    65   (* Reflection *)
    66 
    67 eq_reflection  "(x=y)   ==> (x==y)"
    68 iff_reflection "(P<->Q) ==> (P==Q)"
    69 
    70 end