src/FOL/ifol.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ifol.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,70 @@
+IFOL = Pure + 
+
+classes term < logic
+
+default term
+
+types o 0
+
+arities o :: logic
+
+consts	
+    Trueprop	::	"o => prop"		("(_)" [0] 5)
+    True,False	::	"o"
+  (*Connectives*)
+    "="		::	"['a,'a] => o"		(infixl 50)
+    Not		::	"o => o"		("~ _" [40] 40)
+    "&"		::	"[o,o] => o"		(infixr 35)
+    "|"		::	"[o,o] => o"		(infixr 30)
+    "-->"	::	"[o,o] => o"		(infixr 25)
+    "<->"	::	"[o,o] => o"		(infixr 25)
+  (*Quantifiers*)
+    All		::	"('a => o) => o"	(binder "ALL " 10)
+    Ex		::	"('a => o) => o"	(binder "EX " 10)
+    Ex1		::	"('a => o) => o"	(binder "EX! " 10)
+
+rules
+
+  (*Equality*)
+
+refl		"a=a"
+subst		"[| a=b;  P(a) |] ==> P(b)"
+
+  (*Propositional logic*)
+
+conjI		"[| P;  Q |] ==> P&Q"
+conjunct1	"P&Q ==> P"
+conjunct2	"P&Q ==> Q"
+
+disjI1		"P ==> P|Q"
+disjI2		"Q ==> P|Q"
+disjE		"[| P|Q;  P ==> R;  Q ==> R |] ==> R"
+
+impI		"(P ==> Q) ==> P-->Q"
+mp		"[| P-->Q;  P |] ==> Q"
+
+FalseE		"False ==> P"
+
+  (*Definitions*)
+
+True_def	"True == False-->False"
+not_def		"~P == P-->False"
+iff_def		"P<->Q == (P-->Q) & (Q-->P)"
+
+  (*Unique existence*)
+ex1_def		"EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+
+  (*Quantifiers*)
+
+allI		"(!!x. P(x)) ==> (ALL x.P(x))"
+spec		"(ALL x.P(x)) ==> P(x)"
+
+exI		"P(x) ==> (EX x.P(x))"
+exE		"[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
+
+  (* Reflection *)
+
+eq_reflection  "(x=y)   ==> (x==y)"
+iff_reflection "(P<->Q) ==> (P==Q)"
+
+end