author | lcp |
Thu, 24 Nov 1994 10:23:41 +0100 | |
changeset 737 | 436019ca97d7 |
parent 124 | 858ab9a9b047 |
child 753 | ec86863e87c8 |
permissions | -rw-r--r-- |
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 Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
124 | 9 |
Bool = ZF + "simpdata" + |
0 | 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 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
19 |
translations |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
20 |
"1" == "succ(0)" |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
21 |
|
0 | 22 |
rules |
23 |
bool_def "bool == {0,1}" |
|
24 |
cond_def "cond(b,c,d) == if(b=1,c,d)" |
|
25 |
not_def "not(b) == cond(b,0,1)" |
|
26 |
and_def "a and b == cond(a,b,0)" |
|
27 |
or_def "a or b == cond(a,1,b)" |
|
28 |
xor_def "a xor b == cond(a,not(b),b)" |
|
29 |
end |