author | lcp |
Thu, 30 Sep 1993 10:10:21 +0100 | |
changeset 14 | 1c0926788772 |
parent 6 | 8ce8c4d13d4d |
child 37 | cebe01deba80 |
permissions | -rw-r--r-- |
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 Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
9 |
open Bool; |
|
10 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
11 |
val bool_defs = [bool_def,cond_def]; |
0 | 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 [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"; |
|
57 |
by (rewtac rew); |
|
58 |
by (rtac cond_1 1); |
|
59 |
val def_cond_1 = result(); |
|
60 |
||
61 |
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"; |
|
62 |
by (rewtac rew); |
|
63 |
by (rtac cond_0 1); |
|
64 |
val def_cond_0 = result(); |
|
65 |
||
66 |
fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)]; |
|
67 |
||
68 |
val [not_1,not_0] = conds not_def; |
|
69 |
||
70 |
val [and_1,and_0] = conds and_def; |
|
71 |
||
72 |
val [or_1,or_0] = conds or_def; |
|
73 |
||
74 |
val [xor_1,xor_0] = conds xor_def; |
|
75 |
||
76 |
val not_type = prove_goalw Bool.thy [not_def] |
|
77 |
"a:bool ==> not(a) : bool" |
|
78 |
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); |
|
79 |
||
80 |
val and_type = prove_goalw Bool.thy [and_def] |
|
81 |
"[| a:bool; b:bool |] ==> a and b : bool" |
|
82 |
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); |
|
83 |
||
84 |
val or_type = prove_goalw Bool.thy [or_def] |
|
85 |
"[| a:bool; b:bool |] ==> a or b : bool" |
|
86 |
(fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]); |
|
87 |
||
88 |
val xor_type = prove_goalw Bool.thy [xor_def] |
|
89 |
"[| a:bool; b:bool |] ==> a xor b : bool" |
|
90 |
(fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]); |
|
91 |
||
92 |
val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, |
|
93 |
or_type, xor_type] |
|
94 |
||
95 |
val bool_rews = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0]; |
|
96 |