src/FOL/IFOL.thy

ifol.thy: added ~= for "not equals"

(*  Title: 	FOL/ifol.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Intuitionistic first-order logic
*)

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)

translations
    "x ~= y"    == "~ (x=y)"

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