src/ZF/Bool.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46821 ff6b0c1087f2
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41777
1f7cbe39d425 more precise headers;
wenzelm
parents: 39159
diff changeset
     1
(*  Title:      ZF/Bool.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1992  University of Cambridge
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     4
*)
837
778f01546669 Re-indented declarations; declared the number 2
lcp
parents: 799
diff changeset
     5
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     6
header{*Booleans in Zermelo-Fraenkel Set Theory*}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13356
diff changeset
     8
theory Bool imports pair begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    10
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    11
  one  ("1") where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    12
  "1 == succ(0)"
2539
ddd22ceee8cc turned some consts into syntax;
wenzelm
parents: 2469
diff changeset
    13
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    14
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    15
  two  ("2") where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    16
  "2 == succ(1)"
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
    17
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
    18
text{*2 is equal to bool, but is used as a number rather than a type.*}
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
    19
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    20
definition "bool == {0,1}"
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    21
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    22
definition "cond(b,c,d) == if(b=1,c,d)"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    23
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    24
definition "not(b) == cond(b,0,1)"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    26
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    27
  "and"       :: "[i,i]=>i"      (infixl "and" 70)  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    28
    "a and b == cond(a,b,0)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    29
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    30
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    31
  or          :: "[i,i]=>i"      (infixl "or" 65)  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    32
    "a or b == cond(a,1,b)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    33
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    34
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    35
  xor         :: "[i,i]=>i"      (infixl "xor" 65) where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    36
    "a xor b == cond(a,not(b),b)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    37
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    38
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    39
lemmas bool_defs = bool_def cond_def
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    40
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    41
lemma singleton_0: "{0} = 1"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    42
by (simp add: succ_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    43
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    44
(* Introduction rules *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    45
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    46
lemma bool_1I [simp,TC]: "1 \<in> bool"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    47
by (simp add: bool_defs )
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    48
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    49
lemma bool_0I [simp,TC]: "0 \<in> bool"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    50
by (simp add: bool_defs)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    51
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    52
lemma one_not_0: "1\<noteq>0"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    53
by (simp add: bool_defs )
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    54
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    55
(** 1=0 ==> R **)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    56
lemmas one_neq_0 = one_not_0 [THEN notE]
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    57
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    58
lemma boolE:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    59
    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    60
by (simp add: bool_defs, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    61
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    62
(** cond **)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    63
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    64
(*1 means true*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    65
lemma cond_1 [simp]: "cond(1,c,d) = c"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    66
by (simp add: bool_defs )
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    67
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    68
(*0 means false*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    69
lemma cond_0 [simp]: "cond(0,c,d) = d"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    70
by (simp add: bool_defs )
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    71
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    72
lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
    73
by (simp add: bool_defs, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    74
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    75
(*For Simp_tac and Blast_tac*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    76
lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    77
by (simp add: bool_defs )
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    78
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    79
lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    80
by simp
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    81
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    82
lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    83
by simp
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    84
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    85
lemmas not_1 = not_def [THEN def_cond_1, simp]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    86
lemmas not_0 = not_def [THEN def_cond_0, simp]
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    87
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    88
lemmas and_1 = and_def [THEN def_cond_1, simp]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    89
lemmas and_0 = and_def [THEN def_cond_0, simp]
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    90
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    91
lemmas or_1 = or_def [THEN def_cond_1, simp]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    92
lemmas or_0 = or_def [THEN def_cond_0, simp]
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    93
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    94
lemmas xor_1 = xor_def [THEN def_cond_1, simp]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41777
diff changeset
    95
lemmas xor_0 = xor_def [THEN def_cond_0, simp]
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    96
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    97
lemma not_type [TC]: "a:bool ==> not(a) \<in> bool"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    98
by (simp add: not_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    99
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   100
lemma and_type [TC]: "[| a:bool;  b:bool |] ==> a and b \<in> bool"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   101
by (simp add: and_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   102
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   103
lemma or_type [TC]: "[| a:bool;  b:bool |] ==> a or b \<in> bool"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   104
by (simp add: or_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   105
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   106
lemma xor_type [TC]: "[| a:bool;  b:bool |] ==> a xor b \<in> bool"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   107
by (simp add: xor_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   108
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   109
lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   110
                         or_type xor_type
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   111
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   112
subsection{*Laws About 'not' *}
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   113
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   114
lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   115
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   116
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   117
lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   118
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   119
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   120
lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   121
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   122
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   123
subsection{*Laws About 'and' *}
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   124
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   125
lemma and_absorb [simp]: "a: bool ==> a and a = a"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   126
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   127
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   128
lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   129
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   130
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   131
lemma and_assoc: "a: bool ==> (a and b) and c  =  a and (b and c)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   132
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   133
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   134
lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   135
       (a or b) and c  =  (a and c) or (b and c)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   136
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   137
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   138
subsection{*Laws About 'or' *}
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   139
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   140
lemma or_absorb [simp]: "a: bool ==> a or a = a"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   141
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   142
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   143
lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   144
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   145
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   146
lemma or_assoc: "a: bool ==> (a or b) or c  =  a or (b or c)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   147
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   148
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   149
lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   150
           (a and b) or c  =  (a or c) and (b or c)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   151
by (elim boolE, auto)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   152
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   153
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   154
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
   155
  bool_of_o :: "o=>i" where
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   156
   "bool_of_o(P) == (if P then 1 else 0)"
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   157
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   158
lemma [simp]: "bool_of_o(True) = 1"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   159
by (simp add: bool_of_o_def)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   160
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   161
lemma [simp]: "bool_of_o(False) = 0"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   162
by (simp add: bool_of_o_def)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   163
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   164
lemma [simp,TC]: "bool_of_o(P) \<in> bool"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   165
by (simp add: bool_of_o_def)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   166
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   167
lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   168
by (simp add: bool_of_o_def)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   169
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   170
lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
   171
by (simp add: bool_of_o_def)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13239
diff changeset
   172
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
end