0

1 
(* Title: ZF/bool.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Booleans in ZermeloFraenkel Set Theory


7 
*)


8 


9 
Bool = ZF +


10 
consts


11 
"1" :: "i" ("1")


12 
bool :: "i"


13 
cond :: "[i,i,i]=>i"


14 
not :: "i=>i"


15 
and :: "[i,i]=>i" (infixl 70)


16 
or :: "[i,i]=>i" (infixl 65)


17 
xor :: "[i,i]=>i" (infixl 65)


18 


19 
rules


20 
one_def "1 == succ(0)"


21 
bool_def "bool == {0,1}"


22 
cond_def "cond(b,c,d) == if(b=1,c,d)"


23 
not_def "not(b) == cond(b,0,1)"


24 
and_def "a and b == cond(a,b,0)"


25 
or_def "a or b == cond(a,1,b)"


26 
xor_def "a xor b == cond(a,not(b),b)"


27 
end
