src/FOL/IFOL.thy
changeset 0 a5a9c433f639
child 35 d71f96f1780e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOL/IFOL.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,70 @@
     1.4 +IFOL = Pure + 
     1.5 +
     1.6 +classes term < logic
     1.7 +
     1.8 +default term
     1.9 +
    1.10 +types o 0
    1.11 +
    1.12 +arities o :: logic
    1.13 +
    1.14 +consts	
    1.15 +    Trueprop	::	"o => prop"		("(_)" [0] 5)
    1.16 +    True,False	::	"o"
    1.17 +  (*Connectives*)
    1.18 +    "="		::	"['a,'a] => o"		(infixl 50)
    1.19 +    Not		::	"o => o"		("~ _" [40] 40)
    1.20 +    "&"		::	"[o,o] => o"		(infixr 35)
    1.21 +    "|"		::	"[o,o] => o"		(infixr 30)
    1.22 +    "-->"	::	"[o,o] => o"		(infixr 25)
    1.23 +    "<->"	::	"[o,o] => o"		(infixr 25)
    1.24 +  (*Quantifiers*)
    1.25 +    All		::	"('a => o) => o"	(binder "ALL " 10)
    1.26 +    Ex		::	"('a => o) => o"	(binder "EX " 10)
    1.27 +    Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    1.28 +
    1.29 +rules
    1.30 +
    1.31 +  (*Equality*)
    1.32 +
    1.33 +refl		"a=a"
    1.34 +subst		"[| a=b;  P(a) |] ==> P(b)"
    1.35 +
    1.36 +  (*Propositional logic*)
    1.37 +
    1.38 +conjI		"[| P;  Q |] ==> P&Q"
    1.39 +conjunct1	"P&Q ==> P"
    1.40 +conjunct2	"P&Q ==> Q"
    1.41 +
    1.42 +disjI1		"P ==> P|Q"
    1.43 +disjI2		"Q ==> P|Q"
    1.44 +disjE		"[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    1.45 +
    1.46 +impI		"(P ==> Q) ==> P-->Q"
    1.47 +mp		"[| P-->Q;  P |] ==> Q"
    1.48 +
    1.49 +FalseE		"False ==> P"
    1.50 +
    1.51 +  (*Definitions*)
    1.52 +
    1.53 +True_def	"True == False-->False"
    1.54 +not_def		"~P == P-->False"
    1.55 +iff_def		"P<->Q == (P-->Q) & (Q-->P)"
    1.56 +
    1.57 +  (*Unique existence*)
    1.58 +ex1_def		"EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    1.59 +
    1.60 +  (*Quantifiers*)
    1.61 +
    1.62 +allI		"(!!x. P(x)) ==> (ALL x.P(x))"
    1.63 +spec		"(ALL x.P(x)) ==> P(x)"
    1.64 +
    1.65 +exI		"P(x) ==> (EX x.P(x))"
    1.66 +exE		"[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
    1.67 +
    1.68 +  (* Reflection *)
    1.69 +
    1.70 +eq_reflection  "(x=y)   ==> (x==y)"
    1.71 +iff_reflection "(P<->Q) ==> (P==Q)"
    1.72 +
    1.73 +end