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