src/ZF/bool.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/bool.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,99 @@
     1.4 +(*  Title: 	ZF/bool
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin D Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For ZF/bool.thy.  Booleans in Zermelo-Fraenkel Set Theory 
    1.10 +*)
    1.11 +
    1.12 +open Bool;
    1.13 +
    1.14 +val bool_defs = [bool_def,one_def,cond_def];
    1.15 +
    1.16 +(* Introduction rules *)
    1.17 +
    1.18 +goalw Bool.thy bool_defs "1 : bool";
    1.19 +by (rtac (consI1 RS consI2) 1);
    1.20 +val bool_1I = result();
    1.21 +
    1.22 +goalw Bool.thy bool_defs "0 : bool";
    1.23 +by (rtac consI1 1);
    1.24 +val bool_0I = result();
    1.25 +
    1.26 +goalw Bool.thy bool_defs "~ 1=0";
    1.27 +by (rtac succ_not_0 1);
    1.28 +val one_not_0 = result();
    1.29 +
    1.30 +(** 1=0 ==> R **)
    1.31 +val one_neq_0 = one_not_0 RS notE;
    1.32 +
    1.33 +val prems = goalw Bool.thy bool_defs "[| c: bool;  P(1);  P(0) |] ==> P(c)";
    1.34 +by (cut_facts_tac prems 1);
    1.35 +by (fast_tac ZF_cs 1);
    1.36 +val boolE = result();
    1.37 +
    1.38 +(** cond **)
    1.39 +
    1.40 +(*1 means true*)
    1.41 +goalw Bool.thy bool_defs "cond(1,c,d) = c";
    1.42 +by (rtac (refl RS if_P) 1);
    1.43 +val cond_1 = result();
    1.44 +
    1.45 +(*0 means false*)
    1.46 +goalw Bool.thy bool_defs "cond(0,c,d) = d";
    1.47 +by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
    1.48 +val cond_0 = result();
    1.49 +
    1.50 +val major::prems = goal Bool.thy 
    1.51 +    "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    1.52 +by (rtac (major RS boolE) 1);
    1.53 +by (rtac (cond_0 RS ssubst) 2);
    1.54 +by (resolve_tac prems 2);
    1.55 +by (rtac (cond_1 RS ssubst) 1);
    1.56 +by (resolve_tac prems 1);
    1.57 +val cond_type = result();
    1.58 +
    1.59 +val [cond_cong] = mk_congs Bool.thy ["cond"];
    1.60 +val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
    1.61 +
    1.62 +val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    1.63 +by (rewtac rew);
    1.64 +by (rtac cond_1 1);
    1.65 +val def_cond_1 = result();
    1.66 +
    1.67 +val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
    1.68 +by (rewtac rew);
    1.69 +by (rtac cond_0 1);
    1.70 +val def_cond_0 = result();
    1.71 +
    1.72 +fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
    1.73 +
    1.74 +val [not_1,not_0] = conds not_def;
    1.75 +
    1.76 +val [and_1,and_0] = conds and_def;
    1.77 +
    1.78 +val [or_1,or_0] = conds or_def;
    1.79 +
    1.80 +val [xor_1,xor_0] = conds xor_def;
    1.81 +
    1.82 +val not_type = prove_goalw Bool.thy [not_def]
    1.83 +    "a:bool ==> not(a) : bool"
    1.84 + (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    1.85 +
    1.86 +val and_type = prove_goalw Bool.thy [and_def]
    1.87 +    "[| a:bool;  b:bool |] ==> a and b : bool"
    1.88 + (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    1.89 +
    1.90 +val or_type = prove_goalw Bool.thy [or_def]
    1.91 +    "[| a:bool;  b:bool |] ==> a or b : bool"
    1.92 + (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
    1.93 +
    1.94 +val xor_type = prove_goalw Bool.thy [xor_def]
    1.95 +    "[| a:bool;  b:bool |] ==> a xor b : bool"
    1.96 + (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
    1.97 +
    1.98 +val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
    1.99 +		       or_type, xor_type]
   1.100 +
   1.101 +val bool_rews = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
   1.102 +