|
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 |
|
|
|
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
|