# Theory Bool

Up to index of Isabelle/ZF

theory Bool
imports pair
(*  Title:      ZF/Bool.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)

theory Bool imports pair begin

abbreviation
one ("1") where
"1 == succ(0)"

abbreviation
two ("2") where
"2 == succ(1)"

text{*2 is equal to bool, but is used as a number rather than a type.*}

definition "bool == {0,1}"

definition "cond(b,c,d) == if(b=1,c,d)"

definition "not(b) == cond(b,0,1)"

definition
"and" :: "[i,i]=>i" (infixl "and" 70) where
"a and b == cond(a,b,0)"

definition
or :: "[i,i]=>i" (infixl "or" 65) where
"a or b == cond(a,1,b)"

definition
xor :: "[i,i]=>i" (infixl "xor" 65) where
"a xor b == cond(a,not(b),b)"

lemmas bool_defs = bool_def cond_def

lemma singleton_0: "{0} = 1"

(* Introduction rules *)

lemma bool_1I [simp,TC]: "1 ∈ bool"

lemma bool_0I [simp,TC]: "0 ∈ bool"

lemma one_not_0: "1≠0"

(** 1=0 ==> R **)
lemmas one_neq_0 = one_not_0 [THEN notE]

lemma boolE:
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P"

(** cond **)

(*1 means true*)
lemma cond_1 [simp]: "cond(1,c,d) = c"

(*0 means false*)
lemma cond_0 [simp]: "cond(0,c,d) = d"

lemma cond_type [TC]: "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)"

(*For Simp_tac and Blast_tac*)
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"
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, simp]
lemmas not_0 = not_def [THEN def_cond_0, simp]

lemmas and_1 = and_def [THEN def_cond_1, simp]
lemmas and_0 = and_def [THEN def_cond_0, simp]

lemmas or_1 = or_def [THEN def_cond_1, simp]
lemmas or_0 = or_def [THEN def_cond_0, simp]

lemmas xor_1 = xor_def [THEN def_cond_1, simp]
lemmas xor_0 = xor_def [THEN def_cond_0, simp]

lemma not_type [TC]: "a:bool ==> not(a) ∈ bool"

lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b ∈ bool"

lemma or_type [TC]: "[| a:bool; b:bool |] ==> a or b ∈ bool"

lemma xor_type [TC]: "[| a:bool; b:bool |] ==> a xor b ∈ bool"

lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
or_type xor_type

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)

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)

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)

definition
bool_of_o :: "o=>i" where
"bool_of_o(P) == (if P then 1 else 0)"

lemma [simp]: "bool_of_o(True) = 1"

lemma [simp]: "bool_of_o(False) = 0"