src/ZF/Bool.ML
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 5268 59ef39008514
child 6153 bff90585cce5
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
clasohm@1461
     1
(*  Title:      ZF/bool
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Martin D Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
paulson@5268
     6
Booleans in Zermelo-Fraenkel Set Theory 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Bool;
clasohm@0
    10
lcp@14
    11
val bool_defs = [bool_def,cond_def];
clasohm@0
    12
wenzelm@5067
    13
Goalw [succ_def] "{0} = 1";
paulson@2493
    14
by (rtac refl 1);
paulson@2469
    15
qed "singleton_0";
paulson@2469
    16
clasohm@0
    17
(* Introduction rules *)
clasohm@0
    18
wenzelm@5067
    19
Goalw bool_defs "1 : bool";
clasohm@0
    20
by (rtac (consI1 RS consI2) 1);
clasohm@760
    21
qed "bool_1I";
clasohm@0
    22
wenzelm@5067
    23
Goalw bool_defs "0 : bool";
clasohm@0
    24
by (rtac consI1 1);
clasohm@760
    25
qed "bool_0I";
clasohm@0
    26
paulson@6053
    27
Addsimps [bool_1I, bool_0I];
paulson@6053
    28
wenzelm@5067
    29
Goalw bool_defs "1~=0";
clasohm@0
    30
by (rtac succ_not_0 1);
clasohm@760
    31
qed "one_not_0";
clasohm@0
    32
clasohm@0
    33
(** 1=0 ==> R **)
clasohm@0
    34
val one_neq_0 = one_not_0 RS notE;
clasohm@0
    35
paulson@5268
    36
val major::prems = Goalw bool_defs
lcp@119
    37
    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
lcp@129
    38
by (rtac (major RS consE) 1);
lcp@119
    39
by (REPEAT (eresolve_tac (singletonE::prems) 1));
clasohm@760
    40
qed "boolE";
clasohm@0
    41
clasohm@0
    42
(** cond **)
clasohm@0
    43
clasohm@0
    44
(*1 means true*)
wenzelm@5067
    45
Goalw bool_defs "cond(1,c,d) = c";
clasohm@0
    46
by (rtac (refl RS if_P) 1);
clasohm@760
    47
qed "cond_1";
clasohm@0
    48
clasohm@0
    49
(*0 means false*)
wenzelm@5067
    50
Goalw bool_defs "cond(0,c,d) = d";
clasohm@0
    51
by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
clasohm@760
    52
qed "cond_0";
clasohm@0
    53
paulson@2469
    54
Addsimps [cond_1, cond_0];
paulson@2469
    55
wenzelm@4091
    56
fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
paulson@2469
    57
paulson@2469
    58
paulson@6053
    59
Goal "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
paulson@2469
    60
by (bool_tac 1);
clasohm@760
    61
qed "cond_type";
clasohm@0
    62
paulson@6053
    63
(*For Simp_tac and Blast_tac*)
paulson@6053
    64
Goal "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A";
paulson@6053
    65
by (bool_tac 1);
paulson@6053
    66
qed "cond_simple_type";
paulson@6053
    67
Addsimps [cond_simple_type];
paulson@6053
    68
paulson@5268
    69
val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
clasohm@0
    70
by (rewtac rew);
clasohm@0
    71
by (rtac cond_1 1);
clasohm@760
    72
qed "def_cond_1";
clasohm@0
    73
paulson@5268
    74
val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
clasohm@0
    75
by (rewtac rew);
clasohm@0
    76
by (rtac cond_0 1);
clasohm@760
    77
qed "def_cond_0";
clasohm@0
    78
clasohm@0
    79
fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
clasohm@0
    80
clasohm@0
    81
val [not_1,not_0] = conds not_def;
clasohm@0
    82
val [and_1,and_0] = conds and_def;
paulson@2469
    83
val [or_1,or_0]   = conds or_def;
paulson@2469
    84
val [xor_1,xor_0] = conds xor_def;
clasohm@0
    85
paulson@2469
    86
Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
clasohm@0
    87
clasohm@760
    88
qed_goalw "not_type" Bool.thy [not_def]
clasohm@0
    89
    "a:bool ==> not(a) : bool"
clasohm@0
    90
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
clasohm@0
    91
clasohm@760
    92
qed_goalw "and_type" Bool.thy [and_def]
clasohm@0
    93
    "[| a:bool;  b:bool |] ==> a and b : bool"
clasohm@0
    94
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
clasohm@0
    95
clasohm@760
    96
qed_goalw "or_type" Bool.thy [or_def]
clasohm@0
    97
    "[| a:bool;  b:bool |] ==> a or b : bool"
clasohm@0
    98
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
clasohm@0
    99
paulson@6053
   100
Addsimps [not_type, and_type, or_type];
paulson@6053
   101
clasohm@760
   102
qed_goalw "xor_type" Bool.thy [xor_def]
clasohm@0
   103
    "[| a:bool;  b:bool |] ==> a xor b : bool"
clasohm@0
   104
 (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
clasohm@0
   105
paulson@6053
   106
Addsimps [xor_type];
paulson@6053
   107
clasohm@0
   108
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
paulson@2469
   109
                       or_type, xor_type];
lcp@119
   110
lcp@119
   111
(*** Laws for 'not' ***)
lcp@119
   112
paulson@5137
   113
Goal "a:bool ==> not(not(a)) = a";
paulson@2469
   114
by (bool_tac 1);
clasohm@760
   115
qed "not_not";
lcp@119
   116
paulson@5137
   117
Goal "a:bool ==> not(a and b) = not(a) or not(b)";
paulson@2469
   118
by (bool_tac 1);
clasohm@760
   119
qed "not_and";
lcp@119
   120
paulson@5137
   121
Goal "a:bool ==> not(a or b) = not(a) and not(b)";
paulson@2469
   122
by (bool_tac 1);
clasohm@760
   123
qed "not_or";
lcp@119
   124
paulson@2469
   125
Addsimps [not_not, not_and, not_or];
paulson@2469
   126
lcp@119
   127
(*** Laws about 'and' ***)
lcp@119
   128
paulson@5137
   129
Goal "a: bool ==> a and a = a";
paulson@2469
   130
by (bool_tac 1);
clasohm@760
   131
qed "and_absorb";
lcp@119
   132
paulson@2469
   133
Addsimps [and_absorb];
paulson@2469
   134
paulson@5137
   135
Goal "[| a: bool; b:bool |] ==> a and b = b and a";
paulson@2469
   136
by (bool_tac 1);
clasohm@760
   137
qed "and_commute";
clasohm@0
   138
paulson@5137
   139
Goal "a: bool ==> (a and b) and c  =  a and (b and c)";
paulson@2469
   140
by (bool_tac 1);
clasohm@760
   141
qed "and_assoc";
lcp@119
   142
paulson@5268
   143
Goal "[| a: bool; b:bool; c:bool |] ==> \
lcp@119
   144
\      (a or b) and c  =  (a and c) or (b and c)";
paulson@2469
   145
by (bool_tac 1);
clasohm@760
   146
qed "and_or_distrib";
lcp@119
   147
lcp@119
   148
(** binary orion **)
lcp@119
   149
paulson@5137
   150
Goal "a: bool ==> a or a = a";
paulson@2469
   151
by (bool_tac 1);
clasohm@760
   152
qed "or_absorb";
lcp@119
   153
paulson@2469
   154
Addsimps [or_absorb];
paulson@2469
   155
paulson@5137
   156
Goal "[| a: bool; b:bool |] ==> a or b = b or a";
paulson@2469
   157
by (bool_tac 1);
clasohm@760
   158
qed "or_commute";
lcp@119
   159
paulson@5137
   160
Goal "a: bool ==> (a or b) or c  =  a or (b or c)";
paulson@2469
   161
by (bool_tac 1);
clasohm@760
   162
qed "or_assoc";
lcp@119
   163
paulson@5268
   164
Goal "[| a: bool; b: bool; c: bool |] ==> \
lcp@119
   165
\          (a and b) or c  =  (a or c) and (b or c)";
paulson@2469
   166
by (bool_tac 1);
clasohm@760
   167
qed "or_and_distrib";
lcp@119
   168