src/ZF/bool.ML
author lcp
Mon, 15 Nov 1993 14:33:40 +0100
changeset 119 0e58da397b1d
parent 37 cebe01deba80
child 129 dc50a4b96d7b
permissions -rw-r--r--
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin D Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For ZF/bool.thy.  Booleans in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Bool;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    11
val bool_defs = [bool_def,cond_def];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(* Introduction rules *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
goalw Bool.thy bool_defs "1 : bool";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
by (rtac (consI1 RS consI2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val bool_1I = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
goalw Bool.thy bool_defs "0 : bool";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (rtac consI1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
val bool_0I = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
    23
goalw Bool.thy bool_defs "1~=0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (rtac succ_not_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
val one_not_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
(** 1=0 ==> R **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val one_neq_0 = one_not_0 RS notE;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
119
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    30
val major::prems = goalw Bool.thy bool_defs
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    31
    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    32
br (major RS consE) 1;
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    33
by (REPEAT (eresolve_tac (singletonE::prems) 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val boolE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(** cond **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(*1 means true*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
goalw Bool.thy bool_defs "cond(1,c,d) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (rtac (refl RS if_P) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val cond_1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*0 means false*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
goalw Bool.thy bool_defs "cond(0,c,d) = d";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val cond_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val major::prems = goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (rtac (major RS boolE) 1);
119
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    51
by (asm_simp_tac (ZF_ss addsimps (cond_1::prems)) 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    52
by (asm_simp_tac (ZF_ss addsimps (cond_0::prems)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val cond_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by (rtac cond_1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val def_cond_1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (rtac cond_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
val def_cond_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val [not_1,not_0] = conds not_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val [and_1,and_0] = conds and_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val [or_1,or_0] = conds or_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val [xor_1,xor_0] = conds xor_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val not_type = prove_goalw Bool.thy [not_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    "a:bool ==> not(a) : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val and_type = prove_goalw Bool.thy [and_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
    "[| a:bool;  b:bool |] ==> a and b : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
val or_type = prove_goalw Bool.thy [or_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
    "[| a:bool;  b:bool |] ==> a or b : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val xor_type = prove_goalw Bool.thy [xor_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    "[| a:bool;  b:bool |] ==> a xor b : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
		       or_type, xor_type]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
119
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    94
val bool_simps = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    95
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    96
val bool_ss0 = ZF_ss addsimps bool_simps;
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    97
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    98
fun bool0_tac i =
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
    99
    EVERY [etac boolE i, asm_simp_tac bool_ss0 (i+1), asm_simp_tac bool_ss0 i];
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   100
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   101
(*** Laws for 'not' ***)
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   102
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   103
goal Bool.thy "!!a. a:bool ==> not(not(a)) = a";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   104
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   105
val not_not = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   106
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   107
goal Bool.thy "!!a b. a:bool ==> not(a and b) = not(a) or not(b)";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   108
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   109
val not_and = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   110
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   111
goal Bool.thy "!!a b. a:bool ==> not(a or b) = not(a) and not(b)";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   112
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   113
val not_or = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   114
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   115
(*** Laws about 'and' ***)
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   116
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   117
goal Bool.thy "!!a. a: bool ==> a and a = a";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   118
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   119
val and_absorb = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   120
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   121
goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   122
be boolE 1;
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   123
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   124
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   125
val and_commute = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
119
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   127
goal Bool.thy
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   128
 "!!a. a: bool ==> (a and b) and c  =  a and (b and c)";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   129
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   130
val and_assoc = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   131
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   132
goal Bool.thy
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   133
 "!!a. [| a: bool; b:bool; c:bool |] ==> \
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   134
\      (a or b) and c  =  (a and c) or (b and c)";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   135
by (REPEAT (bool0_tac 1));
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   136
val and_or_distrib = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   137
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   138
(** binary orion **)
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   139
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   140
goal Bool.thy "!!a. a: bool ==> a or a = a";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   141
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   142
val or_absorb = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   143
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   144
goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   145
be boolE 1;
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   146
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   147
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   148
val or_commute = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   149
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   150
goal Bool.thy "!!a. a: bool ==> (a or b) or c  =  a or (b or c)";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   151
by (bool0_tac 1);
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   152
val or_assoc = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   153
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   154
goal Bool.thy
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   155
 "!!a b c. [| a: bool; b: bool; c: bool |] ==> \
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   156
\          (a and b) or c  =  (a or c) and (b or c)";
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   157
by (REPEAT (bool0_tac 1));
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   158
val or_and_distrib = result();
0e58da397b1d boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
lcp
parents: 37
diff changeset
   159