src/ZF/bool.thy

+(*  Title: 	ZF/bool.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Booleans in Zermelo-Fraenkel Set Theory 
+*)
+
+Bool = ZF +
+consts
+    "1"		::      "i"     	("1")
+    bool        ::      "i"
+    cond        ::      "[i,i,i]=>i"
+    not		::	"i=>i"
+    and         ::      "[i,i]=>i"      (infixl 70)
+    or		::      "[i,i]=>i"      (infixl 65)
+    xor		::      "[i,i]=>i"      (infixl 65)
+
+rules
+    one_def 	"1    == succ(0)"
+    bool_def	"bool == {0,1}"
+    cond_def	"cond(b,c,d) == if(b=1,c,d)"
+    not_def	"not(b) == cond(b,0,1)"
+    and_def	"a and b == cond(a,b,0)"
+    or_def	"a or b == cond(a,1,b)"
+    xor_def	"a xor b == cond(a,not(b),b)"
+end