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