# Theory Bool

Up to index of Isabelle/ZF

theory Bool
imports pair
begin

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

### Laws About 'not'

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)

### Laws About 'and'

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

### Laws About 'or'

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