0

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 ZermeloFraenkel 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 
