src/ZF/Bool.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (21 months ago)
changeset 67006 b1278ed3cd46
parent 60770 240563fbf41d
child 69587 53982d5ec0bb
permissions -rw-r--r--
prefer main entry points of HOL;
wenzelm@41777
     1
(*  Title:      ZF/Bool.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1992  University of Cambridge
paulson@13328
     4
*)
lcp@837
     5
wenzelm@60770
     6
section\<open>Booleans in Zermelo-Fraenkel Set Theory\<close>
clasohm@0
     7
haftmann@16417
     8
theory Bool imports pair begin
clasohm@0
     9
wenzelm@24892
    10
abbreviation
wenzelm@24892
    11
  one  ("1") where
wenzelm@24892
    12
  "1 == succ(0)"
wenzelm@2539
    13
wenzelm@24892
    14
abbreviation
wenzelm@24892
    15
  two  ("2") where
wenzelm@24892
    16
  "2 == succ(1)"
lcp@14
    17
wenzelm@60770
    18
text\<open>2 is equal to bool, but is used as a number rather than a type.\<close>
paulson@13328
    19
wenzelm@24893
    20
definition "bool == {0,1}"
wenzelm@24893
    21
wenzelm@24893
    22
definition "cond(b,c,d) == if(b=1,c,d)"
paulson@13239
    23
wenzelm@24893
    24
definition "not(b) == cond(b,0,1)"
paulson@13239
    25
wenzelm@24893
    26
definition
wenzelm@24893
    27
  "and"       :: "[i,i]=>i"      (infixl "and" 70)  where
paulson@13239
    28
    "a and b == cond(a,b,0)"
paulson@13239
    29
wenzelm@24893
    30
definition
wenzelm@24893
    31
  or          :: "[i,i]=>i"      (infixl "or" 65)  where
paulson@13239
    32
    "a or b == cond(a,1,b)"
paulson@13239
    33
wenzelm@24893
    34
definition
wenzelm@24893
    35
  xor         :: "[i,i]=>i"      (infixl "xor" 65) where
paulson@13239
    36
    "a xor b == cond(a,not(b),b)"
paulson@13239
    37
paulson@13239
    38
paulson@13239
    39
lemmas bool_defs = bool_def cond_def
paulson@13239
    40
paulson@13239
    41
lemma singleton_0: "{0} = 1"
paulson@13239
    42
by (simp add: succ_def)
paulson@13239
    43
paulson@13239
    44
(* Introduction rules *)
paulson@13239
    45
paulson@46820
    46
lemma bool_1I [simp,TC]: "1 \<in> bool"
paulson@13239
    47
by (simp add: bool_defs )
paulson@13239
    48
paulson@46820
    49
lemma bool_0I [simp,TC]: "0 \<in> bool"
paulson@13239
    50
by (simp add: bool_defs)
paulson@13239
    51
paulson@46820
    52
lemma one_not_0: "1\<noteq>0"
paulson@13239
    53
by (simp add: bool_defs )
paulson@13239
    54
paulson@13239
    55
(** 1=0 ==> R **)
wenzelm@45602
    56
lemmas one_neq_0 = one_not_0 [THEN notE]
paulson@13239
    57
paulson@13239
    58
lemma boolE:
paulson@13239
    59
    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"
wenzelm@24892
    60
by (simp add: bool_defs, blast)
paulson@13239
    61
paulson@13239
    62
(** cond **)
paulson@13239
    63
paulson@13239
    64
(*1 means true*)
paulson@13239
    65
lemma cond_1 [simp]: "cond(1,c,d) = c"
paulson@13239
    66
by (simp add: bool_defs )
paulson@13239
    67
paulson@13239
    68
(*0 means false*)
paulson@13239
    69
lemma cond_0 [simp]: "cond(0,c,d) = d"
paulson@13239
    70
by (simp add: bool_defs )
paulson@13239
    71
paulson@13239
    72
lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"
paulson@13269
    73
by (simp add: bool_defs, blast)
paulson@13239
    74
paulson@13239
    75
(*For Simp_tac and Blast_tac*)
paulson@13239
    76
lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"
paulson@13239
    77
by (simp add: bool_defs )
paulson@13239
    78
paulson@13239
    79
lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"
paulson@13239
    80
by simp
paulson@13239
    81
paulson@13239
    82
lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
paulson@13239
    83
by simp
paulson@13239
    84
wenzelm@45602
    85
lemmas not_1 = not_def [THEN def_cond_1, simp]
wenzelm@45602
    86
lemmas not_0 = not_def [THEN def_cond_0, simp]
paulson@13239
    87
wenzelm@45602
    88
lemmas and_1 = and_def [THEN def_cond_1, simp]
wenzelm@45602
    89
lemmas and_0 = and_def [THEN def_cond_0, simp]
paulson@13239
    90
wenzelm@45602
    91
lemmas or_1 = or_def [THEN def_cond_1, simp]
wenzelm@45602
    92
lemmas or_0 = or_def [THEN def_cond_0, simp]
paulson@13239
    93
wenzelm@45602
    94
lemmas xor_1 = xor_def [THEN def_cond_1, simp]
wenzelm@45602
    95
lemmas xor_0 = xor_def [THEN def_cond_0, simp]
paulson@13239
    96
paulson@46820
    97
lemma not_type [TC]: "a:bool ==> not(a) \<in> bool"
paulson@13239
    98
by (simp add: not_def)
paulson@13239
    99
paulson@46820
   100
lemma and_type [TC]: "[| a:bool;  b:bool |] ==> a and b \<in> bool"
paulson@13239
   101
by (simp add: and_def)
paulson@13239
   102
paulson@46820
   103
lemma or_type [TC]: "[| a:bool;  b:bool |] ==> a or b \<in> bool"
paulson@13239
   104
by (simp add: or_def)
paulson@13239
   105
paulson@46820
   106
lemma xor_type [TC]: "[| a:bool;  b:bool |] ==> a xor b \<in> bool"
paulson@13239
   107
by (simp add: xor_def)
paulson@13239
   108
paulson@13239
   109
lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
paulson@13239
   110
                         or_type xor_type
paulson@13239
   111
wenzelm@60770
   112
subsection\<open>Laws About 'not'\<close>
paulson@13239
   113
paulson@13239
   114
lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
paulson@13239
   115
by (elim boolE, auto)
paulson@13239
   116
paulson@13239
   117
lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"
paulson@13239
   118
by (elim boolE, auto)
paulson@13239
   119
paulson@13239
   120
lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
paulson@13239
   121
by (elim boolE, auto)
paulson@13239
   122
wenzelm@60770
   123
subsection\<open>Laws About 'and'\<close>
paulson@13239
   124
paulson@13239
   125
lemma and_absorb [simp]: "a: bool ==> a and a = a"
paulson@13239
   126
by (elim boolE, auto)
paulson@13239
   127
paulson@13239
   128
lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"
paulson@13239
   129
by (elim boolE, auto)
paulson@13239
   130
paulson@13239
   131
lemma and_assoc: "a: bool ==> (a and b) and c  =  a and (b and c)"
paulson@13239
   132
by (elim boolE, auto)
paulson@13239
   133
wenzelm@24892
   134
lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
paulson@13239
   135
       (a or b) and c  =  (a and c) or (b and c)"
paulson@13239
   136
by (elim boolE, auto)
paulson@13239
   137
wenzelm@60770
   138
subsection\<open>Laws About 'or'\<close>
paulson@13239
   139
paulson@13239
   140
lemma or_absorb [simp]: "a: bool ==> a or a = a"
paulson@13239
   141
by (elim boolE, auto)
paulson@13239
   142
paulson@13239
   143
lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"
paulson@13239
   144
by (elim boolE, auto)
paulson@13239
   145
paulson@13239
   146
lemma or_assoc: "a: bool ==> (a or b) or c  =  a or (b or c)"
paulson@13239
   147
by (elim boolE, auto)
paulson@13239
   148
wenzelm@24892
   149
lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
paulson@13239
   150
           (a and b) or c  =  (a or c) and (b or c)"
paulson@13239
   151
by (elim boolE, auto)
paulson@13239
   152
paulson@13269
   153
wenzelm@24893
   154
definition
wenzelm@24893
   155
  bool_of_o :: "o=>i" where
paulson@13269
   156
   "bool_of_o(P) == (if P then 1 else 0)"
paulson@13269
   157
paulson@13269
   158
lemma [simp]: "bool_of_o(True) = 1"
wenzelm@24892
   159
by (simp add: bool_of_o_def)
paulson@13269
   160
paulson@13269
   161
lemma [simp]: "bool_of_o(False) = 0"
wenzelm@24892
   162
by (simp add: bool_of_o_def)
paulson@13269
   163
paulson@13269
   164
lemma [simp,TC]: "bool_of_o(P) \<in> bool"
wenzelm@24892
   165
by (simp add: bool_of_o_def)
paulson@13269
   166
paulson@46821
   167
lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
wenzelm@24892
   168
by (simp add: bool_of_o_def)
paulson@13269
   169
paulson@46821
   170
lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
wenzelm@24892
   171
by (simp add: bool_of_o_def)
paulson@13269
   172
clasohm@0
   173
end