src/ZF/Bool.thy
author wenzelm
Fri Feb 18 16:22:27 2011 +0100 (2011-02-18)
changeset 41777 1f7cbe39d425
parent 39159 0dec18004e75
child 45602 2a858377c3d2
permissions -rw-r--r--
more precise headers;
     1 (*  Title:      ZF/Bool.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 *)
     5 
     6 header{*Booleans in Zermelo-Fraenkel Set Theory*}
     7 
     8 theory Bool imports pair begin
     9 
    10 abbreviation
    11   one  ("1") where
    12   "1 == succ(0)"
    13 
    14 abbreviation
    15   two  ("2") where
    16   "2 == succ(1)"
    17 
    18 text{*2 is equal to bool, but is used as a number rather than a type.*}
    19 
    20 definition "bool == {0,1}"
    21 
    22 definition "cond(b,c,d) == if(b=1,c,d)"
    23 
    24 definition "not(b) == cond(b,0,1)"
    25 
    26 definition
    27   "and"       :: "[i,i]=>i"      (infixl "and" 70)  where
    28     "a and b == cond(a,b,0)"
    29 
    30 definition
    31   or          :: "[i,i]=>i"      (infixl "or" 65)  where
    32     "a or b == cond(a,1,b)"
    33 
    34 definition
    35   xor         :: "[i,i]=>i"      (infixl "xor" 65) where
    36     "a xor b == cond(a,not(b),b)"
    37 
    38 
    39 lemmas bool_defs = bool_def cond_def
    40 
    41 lemma singleton_0: "{0} = 1"
    42 by (simp add: succ_def)
    43 
    44 (* Introduction rules *)
    45 
    46 lemma bool_1I [simp,TC]: "1 : bool"
    47 by (simp add: bool_defs )
    48 
    49 lemma bool_0I [simp,TC]: "0 : bool"
    50 by (simp add: bool_defs)
    51 
    52 lemma one_not_0: "1~=0"
    53 by (simp add: bool_defs )
    54 
    55 (** 1=0 ==> R **)
    56 lemmas one_neq_0 = one_not_0 [THEN notE, standard]
    57 
    58 lemma boolE:
    59     "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"
    60 by (simp add: bool_defs, blast)
    61 
    62 (** cond **)
    63 
    64 (*1 means true*)
    65 lemma cond_1 [simp]: "cond(1,c,d) = c"
    66 by (simp add: bool_defs )
    67 
    68 (*0 means false*)
    69 lemma cond_0 [simp]: "cond(0,c,d) = d"
    70 by (simp add: bool_defs )
    71 
    72 lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"
    73 by (simp add: bool_defs, blast)
    74 
    75 (*For Simp_tac and Blast_tac*)
    76 lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"
    77 by (simp add: bool_defs )
    78 
    79 lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"
    80 by simp
    81 
    82 lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
    83 by simp
    84 
    85 lemmas not_1 = not_def [THEN def_cond_1, standard, simp]
    86 lemmas not_0 = not_def [THEN def_cond_0, standard, simp]
    87 
    88 lemmas and_1 = and_def [THEN def_cond_1, standard, simp]
    89 lemmas and_0 = and_def [THEN def_cond_0, standard, simp]
    90 
    91 lemmas or_1 = or_def [THEN def_cond_1, standard, simp]
    92 lemmas or_0 = or_def [THEN def_cond_0, standard, simp]
    93 
    94 lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp]
    95 lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp]
    96 
    97 lemma not_type [TC]: "a:bool ==> not(a) : bool"
    98 by (simp add: not_def)
    99 
   100 lemma and_type [TC]: "[| a:bool;  b:bool |] ==> a and b : bool"
   101 by (simp add: and_def)
   102 
   103 lemma or_type [TC]: "[| a:bool;  b:bool |] ==> a or b : bool"
   104 by (simp add: or_def)
   105 
   106 lemma xor_type [TC]: "[| a:bool;  b:bool |] ==> a xor b : bool"
   107 by (simp add: xor_def)
   108 
   109 lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
   110                          or_type xor_type
   111 
   112 subsection{*Laws About 'not' *}
   113 
   114 lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
   115 by (elim boolE, auto)
   116 
   117 lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"
   118 by (elim boolE, auto)
   119 
   120 lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
   121 by (elim boolE, auto)
   122 
   123 subsection{*Laws About 'and' *}
   124 
   125 lemma and_absorb [simp]: "a: bool ==> a and a = a"
   126 by (elim boolE, auto)
   127 
   128 lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"
   129 by (elim boolE, auto)
   130 
   131 lemma and_assoc: "a: bool ==> (a and b) and c  =  a and (b and c)"
   132 by (elim boolE, auto)
   133 
   134 lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
   135        (a or b) and c  =  (a and c) or (b and c)"
   136 by (elim boolE, auto)
   137 
   138 subsection{*Laws About 'or' *}
   139 
   140 lemma or_absorb [simp]: "a: bool ==> a or a = a"
   141 by (elim boolE, auto)
   142 
   143 lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"
   144 by (elim boolE, auto)
   145 
   146 lemma or_assoc: "a: bool ==> (a or b) or c  =  a or (b or c)"
   147 by (elim boolE, auto)
   148 
   149 lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
   150            (a and b) or c  =  (a or c) and (b or c)"
   151 by (elim boolE, auto)
   152 
   153 
   154 definition
   155   bool_of_o :: "o=>i" where
   156    "bool_of_o(P) == (if P then 1 else 0)"
   157 
   158 lemma [simp]: "bool_of_o(True) = 1"
   159 by (simp add: bool_of_o_def)
   160 
   161 lemma [simp]: "bool_of_o(False) = 0"
   162 by (simp add: bool_of_o_def)
   163 
   164 lemma [simp,TC]: "bool_of_o(P) \<in> bool"
   165 by (simp add: bool_of_o_def)
   166 
   167 lemma [simp]: "(bool_of_o(P) = 1) <-> P"
   168 by (simp add: bool_of_o_def)
   169 
   170 lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
   171 by (simp add: bool_of_o_def)
   172 
   173 ML
   174 {*
   175 val bool_def = @{thm bool_def};
   176 val bool_defs = @{thms bool_defs};
   177 val singleton_0 = @{thm singleton_0};
   178 val bool_1I = @{thm bool_1I};
   179 val bool_0I = @{thm bool_0I};
   180 val one_not_0 = @{thm one_not_0};
   181 val one_neq_0 = @{thm one_neq_0};
   182 val boolE = @{thm boolE};
   183 val cond_1 = @{thm cond_1};
   184 val cond_0 = @{thm cond_0};
   185 val cond_type = @{thm cond_type};
   186 val cond_simple_type = @{thm cond_simple_type};
   187 val def_cond_1 = @{thm def_cond_1};
   188 val def_cond_0 = @{thm def_cond_0};
   189 val not_1 = @{thm not_1};
   190 val not_0 = @{thm not_0};
   191 val and_1 = @{thm and_1};
   192 val and_0 = @{thm and_0};
   193 val or_1 = @{thm or_1};
   194 val or_0 = @{thm or_0};
   195 val xor_1 = @{thm xor_1};
   196 val xor_0 = @{thm xor_0};
   197 val not_type = @{thm not_type};
   198 val and_type = @{thm and_type};
   199 val or_type = @{thm or_type};
   200 val xor_type = @{thm xor_type};
   201 val bool_typechecks = @{thms bool_typechecks};
   202 val not_not = @{thm not_not};
   203 val not_and = @{thm not_and};
   204 val not_or = @{thm not_or};
   205 val and_absorb = @{thm and_absorb};
   206 val and_commute = @{thm and_commute};
   207 val and_assoc = @{thm and_assoc};
   208 val and_or_distrib = @{thm and_or_distrib};
   209 val or_absorb = @{thm or_absorb};
   210 val or_commute = @{thm or_commute};
   211 val or_assoc = @{thm or_assoc};
   212 val or_and_distrib = @{thm or_and_distrib};
   213 *}
   214 
   215 end