src/ZF/Bool.ML
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val bool_defs = [bool_def,one_def,cond_def];
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
goalw Bool.thy bool_defs "~ 1=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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val prems = goalw Bool.thy bool_defs "[| c: bool;  P(1);  P(0) |] ==> P(c)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val boolE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(** cond **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
(*1 means true*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
goalw Bool.thy bool_defs "cond(1,c,d) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
by (rtac (refl RS if_P) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val cond_1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
(*0 means false*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
goalw Bool.thy bool_defs "cond(0,c,d) = d";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val cond_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val major::prems = goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (rtac (major RS boolE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (rtac (cond_0 RS ssubst) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by (resolve_tac prems 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
by (rtac (cond_1 RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val cond_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (rtac cond_1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val def_cond_1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (rtac cond_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
val def_cond_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val [not_1,not_0] = conds not_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val [and_1,and_0] = conds and_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val [or_1,or_0] = conds or_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val [xor_1,xor_0] = conds xor_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val not_type = prove_goalw Bool.thy [not_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    "a:bool ==> not(a) : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
val and_type = prove_goalw Bool.thy [and_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
    "[| a:bool;  b:bool |] ==> a and b : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val or_type = prove_goalw Bool.thy [or_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    "[| a:bool;  b:bool |] ==> a or b : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
 (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val xor_type = prove_goalw Bool.thy [xor_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    "[| a:bool;  b:bool |] ==> a xor b : bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
 (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
		       or_type, xor_type]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val bool_rews = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96