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