src/ZF/Bool.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     1 (*  Title: 	ZF/bool
       
     2     ID:         $Id$
       
     3     Author: 	Martin D Coen, Cambridge University Computer Laboratory
       
     4     Copyright   1992  University of Cambridge
       
     5 
       
     6 For ZF/bool.thy.  Booleans in Zermelo-Fraenkel Set Theory 
       
     7 *)
       
     8 
       
     9 open Bool;
       
    10 
       
    11 val bool_defs = [bool_def,one_def,cond_def];
       
    12 
       
    13 (* Introduction rules *)
       
    14 
       
    15 goalw Bool.thy bool_defs "1 : bool";
       
    16 by (rtac (consI1 RS consI2) 1);
       
    17 val bool_1I = result();
       
    18 
       
    19 goalw Bool.thy bool_defs "0 : bool";
       
    20 by (rtac consI1 1);
       
    21 val bool_0I = result();
       
    22 
       
    23 goalw Bool.thy bool_defs "~ 1=0";
       
    24 by (rtac succ_not_0 1);
       
    25 val one_not_0 = result();
       
    26 
       
    27 (** 1=0 ==> R **)
       
    28 val one_neq_0 = one_not_0 RS notE;
       
    29 
       
    30 val prems = goalw Bool.thy bool_defs "[| c: bool;  P(1);  P(0) |] ==> P(c)";
       
    31 by (cut_facts_tac prems 1);
       
    32 by (fast_tac ZF_cs 1);
       
    33 val boolE = result();
       
    34 
       
    35 (** cond **)
       
    36 
       
    37 (*1 means true*)
       
    38 goalw Bool.thy bool_defs "cond(1,c,d) = c";
       
    39 by (rtac (refl RS if_P) 1);
       
    40 val cond_1 = result();
       
    41 
       
    42 (*0 means false*)
       
    43 goalw Bool.thy bool_defs "cond(0,c,d) = d";
       
    44 by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
       
    45 val cond_0 = result();
       
    46 
       
    47 val major::prems = goal Bool.thy 
       
    48     "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
       
    49 by (rtac (major RS boolE) 1);
       
    50 by (rtac (cond_0 RS ssubst) 2);
       
    51 by (resolve_tac prems 2);
       
    52 by (rtac (cond_1 RS ssubst) 1);
       
    53 by (resolve_tac prems 1);
       
    54 val cond_type = result();
       
    55 
       
    56 val [cond_cong] = mk_congs Bool.thy ["cond"];
       
    57 val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
       
    58 
       
    59 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
       
    60 by (rewtac rew);
       
    61 by (rtac cond_1 1);
       
    62 val def_cond_1 = result();
       
    63 
       
    64 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
       
    65 by (rewtac rew);
       
    66 by (rtac cond_0 1);
       
    67 val def_cond_0 = result();
       
    68 
       
    69 fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
       
    70 
       
    71 val [not_1,not_0] = conds not_def;
       
    72 
       
    73 val [and_1,and_0] = conds and_def;
       
    74 
       
    75 val [or_1,or_0] = conds or_def;
       
    76 
       
    77 val [xor_1,xor_0] = conds xor_def;
       
    78 
       
    79 val not_type = prove_goalw Bool.thy [not_def]
       
    80     "a:bool ==> not(a) : bool"
       
    81  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
       
    82 
       
    83 val and_type = prove_goalw Bool.thy [and_def]
       
    84     "[| a:bool;  b:bool |] ==> a and b : bool"
       
    85  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
       
    86 
       
    87 val or_type = prove_goalw Bool.thy [or_def]
       
    88     "[| a:bool;  b:bool |] ==> a or b : bool"
       
    89  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
       
    90 
       
    91 val xor_type = prove_goalw Bool.thy [xor_def]
       
    92     "[| a:bool;  b:bool |] ==> a xor b : bool"
       
    93  (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
       
    94 
       
    95 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
       
    96 		       or_type, xor_type]
       
    97 
       
    98 val bool_rews = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
       
    99