author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1478  2b8c2a7547ab 
child 1629  b5e43a60443a 
permissions  rwrr 
1478  1 
(* Title: ZF/bool.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Booleans in ZermeloFraenkel Set Theory 

837  7 

8 
2 is equal to bool, but serves a different purpose 

0  9 
*) 
10 

124  11 
Bool = ZF + "simpdata" + 
0  12 
consts 
1478  13 
"1" :: i ("1") 
1401  14 
"2" :: i ("2") 
15 
bool :: i 

16 
cond :: [i,i,i]=>i 

1478  17 
not :: i=>i 
1401  18 
"and" :: [i,i]=>i (infixl 70) 
1478  19 
or :: [i,i]=>i (infixl 65) 
20 
xor :: [i,i]=>i (infixl 65) 

0  21 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

22 
translations 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

23 
"1" == "succ(0)" 
837  24 
"2" == "succ(1)" 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

25 

753  26 
defs 
1478  27 
bool_def "bool == {0,1}" 
28 
cond_def "cond(b,c,d) == if(b=1,c,d)" 

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

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

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

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

0  33 
end 