(*  Title:      ZF/Bool.thy

    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

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"

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)

definition

  bool_of_o :: "o=>i" where

   "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) \<in> 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