(* Title: ZF/bool.thy ID: $Id: Bool.thy,v 1.19 2005/06/17 14:15:09 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) header{*Booleans in Zermelo-Fraenkel Set Theory*} theory Bool imports pair begin syntax "1" :: i ("1") "2" :: i ("2") translations "1" == "succ(0)" "2" == "succ(1)" text{*2 is equal to bool, but is used as a number rather than a type.*} constdefs bool :: i "bool == {0,1}" cond :: "[i,i,i]=>i" "cond(b,c,d) == if(b=1,c,d)" not :: "i=>i" "not(b) == cond(b,0,1)" "and" :: "[i,i]=>i" (infixl "and" 70) "a and b == cond(a,b,0)" or :: "[i,i]=>i" (infixl "or" 65) "a or b == cond(a,1,b)" xor :: "[i,i]=>i" (infixl "xor" 65) "a xor b == cond(a,not(b),b)" lemmas bool_defs = bool_def cond_def lemma singleton_0: "{0} = 1" by (simp add: succ_def) (* Introduction rules *) lemma bool_1I [simp,TC]: "1 : bool" by (simp add: bool_defs ) lemma bool_0I [simp,TC]: "0 : bool" by (simp add: bool_defs) lemma one_not_0: "1~=0" by (simp add: bool_defs ) (** 1=0 ==> R **) lemmas one_neq_0 = one_not_0 [THEN notE, standard] lemma boolE: "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P" by (simp add: bool_defs, blast) (** cond **) (*1 means true*) lemma cond_1 [simp]: "cond(1,c,d) = c" by (simp add: bool_defs ) (*0 means false*) lemma cond_0 [simp]: "cond(0,c,d) = d" by (simp add: bool_defs ) lemma cond_type [TC]: "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)" by (simp add: bool_defs, blast) (*For Simp_tac and Blast_tac*) lemma cond_simple_type: "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A" by (simp add: bool_defs ) lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c" by simp lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d" by simp lemmas not_1 = not_def [THEN def_cond_1, standard, simp] lemmas not_0 = not_def [THEN def_cond_0, standard, simp] lemmas and_1 = and_def [THEN def_cond_1, standard, simp] lemmas and_0 = and_def [THEN def_cond_0, standard, simp] lemmas or_1 = or_def [THEN def_cond_1, standard, simp] lemmas or_0 = or_def [THEN def_cond_0, standard, simp] lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp] lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp] lemma not_type [TC]: "a:bool ==> not(a) : bool" by (simp add: not_def) lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b : bool" by (simp add: and_def) lemma or_type [TC]: "[| a:bool; b:bool |] ==> a or b : bool" by (simp add: or_def) lemma xor_type [TC]: "[| a:bool; b:bool |] ==> a xor b : bool" by (simp add: xor_def) lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type or_type xor_type subsection{*Laws About 'not' *} lemma not_not [simp]: "a:bool ==> not(not(a)) = a" by (elim boolE, auto) lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)" by (elim boolE, auto) lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)" by (elim boolE, auto) subsection{*Laws About 'and' *} lemma and_absorb [simp]: "a: bool ==> a and a = a" by (elim boolE, auto) lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a" by (elim boolE, auto) lemma and_assoc: "a: bool ==> (a and b) and c = a and (b and c)" by (elim boolE, auto) lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==> (a or b) and c = (a and c) or (b and c)" by (elim boolE, auto) subsection{*Laws About 'or' *} lemma or_absorb [simp]: "a: bool ==> a or a = a" by (elim boolE, auto) lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a" by (elim boolE, auto) lemma or_assoc: "a: bool ==> (a or b) or c = a or (b or c)" by (elim boolE, auto) lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==> (a and b) or c = (a or c) and (b or c)" by (elim boolE, auto) constdefs bool_of_o :: "o=>i" "bool_of_o(P) == (if P then 1 else 0)" lemma [simp]: "bool_of_o(True) = 1" by (simp add: bool_of_o_def) lemma [simp]: "bool_of_o(False) = 0" by (simp add: bool_of_o_def) lemma [simp,TC]: "bool_of_o(P) ∈ bool" by (simp add: bool_of_o_def) lemma [simp]: "(bool_of_o(P) = 1) <-> P" by (simp add: bool_of_o_def) lemma [simp]: "(bool_of_o(P) = 0) <-> ~P" by (simp add: bool_of_o_def) ML {* val bool_def = thm "bool_def"; val bool_defs = thms "bool_defs"; val singleton_0 = thm "singleton_0"; val bool_1I = thm "bool_1I"; val bool_0I = thm "bool_0I"; val one_not_0 = thm "one_not_0"; val one_neq_0 = thm "one_neq_0"; val boolE = thm "boolE"; val cond_1 = thm "cond_1"; val cond_0 = thm "cond_0"; val cond_type = thm "cond_type"; val cond_simple_type = thm "cond_simple_type"; val def_cond_1 = thm "def_cond_1"; val def_cond_0 = thm "def_cond_0"; val not_1 = thm "not_1"; val not_0 = thm "not_0"; val and_1 = thm "and_1"; val and_0 = thm "and_0"; val or_1 = thm "or_1"; val or_0 = thm "or_0"; val xor_1 = thm "xor_1"; val xor_0 = thm "xor_0"; val not_type = thm "not_type"; val and_type = thm "and_type"; val or_type = thm "or_type"; val xor_type = thm "xor_type"; val bool_typechecks = thms "bool_typechecks"; val not_not = thm "not_not"; val not_and = thm "not_and"; val not_or = thm "not_or"; val and_absorb = thm "and_absorb"; val and_commute = thm "and_commute"; val and_assoc = thm "and_assoc"; val and_or_distrib = thm "and_or_distrib"; val or_absorb = thm "or_absorb"; val or_commute = thm "or_commute"; val or_assoc = thm "or_assoc"; val or_and_distrib = thm "or_and_distrib"; *} end
lemmas bool_defs:
bool == {0, 1}
cond(b, c, d) == if b = 1 then c else d
lemmas bool_defs:
bool == {0, 1}
cond(b, c, d) == if b = 1 then c else d
lemma singleton_0:
{0} = 1
lemma bool_1I:
1 ∈ bool
lemma bool_0I:
0 ∈ bool
lemma one_not_0:
1 ≠ 0
lemmas one_neq_0:
1 = 0 ==> R
lemmas one_neq_0:
1 = 0 ==> R
lemma boolE:
[| c ∈ bool; c = 1 ==> P; c = 0 ==> P |] ==> P
lemma cond_1:
cond(1, c, d) = c
lemma cond_0:
cond(0, c, d) = d
lemma cond_type:
[| b ∈ bool; c ∈ A(1); d ∈ A(0) |] ==> cond(b, c, d) ∈ A(b)
lemma cond_simple_type:
[| b ∈ bool; c ∈ A; d ∈ A |] ==> cond(b, c, d) ∈ A
lemma def_cond_1:
(!!b. j(b) == cond(b, c, d)) ==> j(1) = c
lemma def_cond_0:
(!!b. j(b) == cond(b, c, d)) ==> j(0) = d
lemmas not_1:
not(1) = 0
lemmas not_1:
not(1) = 0
lemmas not_0:
not(0) = 1
lemmas not_0:
not(0) = 1
lemmas and_1:
1 and c = c
lemmas and_1:
1 and c = c
lemmas and_0:
0 and c = 0
lemmas and_0:
0 and c = 0
lemmas or_1:
1 or d = 1
lemmas or_1:
1 or d = 1
lemmas or_0:
0 or d = d
lemmas or_0:
0 or d = d
lemmas xor_1:
1 xor d = not(d)
lemmas xor_1:
1 xor d = not(d)
lemmas xor_0:
0 xor d = d
lemmas xor_0:
0 xor d = d
lemma not_type:
a ∈ bool ==> not(a) ∈ bool
lemma and_type:
[| a ∈ bool; b ∈ bool |] ==> a and b ∈ bool
lemma or_type:
[| a ∈ bool; b ∈ bool |] ==> a or b ∈ bool
lemma xor_type:
[| a ∈ bool; b ∈ bool |] ==> a xor b ∈ bool
lemmas bool_typechecks:
1 ∈ bool
0 ∈ bool
[| b ∈ bool; c ∈ A(1); d ∈ A(0) |] ==> cond(b, c, d) ∈ A(b)
a ∈ bool ==> not(a) ∈ bool
[| a ∈ bool; b ∈ bool |] ==> a and b ∈ bool
[| a ∈ bool; b ∈ bool |] ==> a or b ∈ bool
[| a ∈ bool; b ∈ bool |] ==> a xor b ∈ bool
lemmas bool_typechecks:
1 ∈ bool
0 ∈ bool
[| b ∈ bool; c ∈ A(1); d ∈ A(0) |] ==> cond(b, c, d) ∈ A(b)
a ∈ bool ==> not(a) ∈ bool
[| a ∈ bool; b ∈ bool |] ==> a and b ∈ bool
[| a ∈ bool; b ∈ bool |] ==> a or b ∈ bool
[| a ∈ bool; b ∈ bool |] ==> a xor b ∈ bool
lemma not_not:
a ∈ bool ==> not(not(a)) = a
lemma not_and:
a ∈ bool ==> not(a and b) = not(a) or not(b)
lemma not_or:
a ∈ bool ==> not(a or b) = not(a) and not(b)
lemma and_absorb:
a ∈ bool ==> a and a = a
lemma and_commute:
[| a ∈ bool; b ∈ bool |] ==> a and b = b and a
lemma and_assoc:
a ∈ bool ==> a and b and c = a and (b and c)
lemma and_or_distrib:
[| a ∈ bool; b ∈ bool; c ∈ bool |] ==> (a or b) and c = a and c or b and c
lemma or_absorb:
a ∈ bool ==> a or a = a
lemma or_commute:
[| a ∈ bool; b ∈ bool |] ==> a or b = b or a
lemma or_assoc:
a ∈ bool ==> a or b or c = a or (b or c)
lemma or_and_distrib:
[| a ∈ bool; b ∈ bool; c ∈ bool |] ==> a and b or c = (a or c) and (b or c)
lemma
bool_of_o(True) = 1
lemma
bool_of_o(False) = 0
lemma
bool_of_o(P) ∈ bool
lemma
bool_of_o(P) = 1 <-> P
lemma
bool_of_o(P) = 0 <-> ¬ P