|
1 (* Title: CTT/bool |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Theorems for bool.thy (booleans and conditionals) |
|
7 *) |
|
8 |
|
9 open Bool; |
|
10 |
|
11 val bool_defs = [Bool_def,true_def,false_def,cond_def]; |
|
12 |
|
13 (*Derivation of rules for the type Bool*) |
|
14 |
|
15 (*formation rule*) |
|
16 val boolF = prove_goal Bool.thy |
|
17 "Bool type" |
|
18 (fn prems=> |
|
19 [ (rewrite_goals_tac bool_defs), |
|
20 (typechk_tac[]) ]); |
|
21 |
|
22 |
|
23 (*introduction rules for true, false*) |
|
24 |
|
25 val boolI_true = prove_goal Bool.thy |
|
26 "true : Bool" |
|
27 (fn prems=> |
|
28 [ (rewrite_goals_tac bool_defs), |
|
29 (typechk_tac[]) ]); |
|
30 |
|
31 val boolI_false = prove_goal Bool.thy |
|
32 "false : Bool" |
|
33 (fn prems=> |
|
34 [ (rewrite_goals_tac bool_defs), |
|
35 (typechk_tac[]) ]); |
|
36 |
|
37 (*elimination rule: typing of cond*) |
|
38 val boolE = prove_goal Bool.thy |
|
39 "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)" |
|
40 (fn prems=> |
|
41 [ (cut_facts_tac prems 1), |
|
42 (rewrite_goals_tac bool_defs), |
|
43 (typechk_tac prems), |
|
44 (ALLGOALS (etac TE)), |
|
45 (typechk_tac prems) ]); |
|
46 |
|
47 val boolEL = prove_goal Bool.thy |
|
48 "[| p = q : Bool; a = c : C(true); b = d : C(false) |] ==> \ |
|
49 \ cond(p,a,b) = cond(q,c,d) : C(p)" |
|
50 (fn prems=> |
|
51 [ (cut_facts_tac prems 1), |
|
52 (rewrite_goals_tac bool_defs), |
|
53 (resolve_tac [PlusEL] 1), |
|
54 (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]); |
|
55 |
|
56 (*computation rules for true, false*) |
|
57 |
|
58 val boolC_true = prove_goal Bool.thy |
|
59 "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)" |
|
60 (fn prems=> |
|
61 [ (cut_facts_tac prems 1), |
|
62 (rewrite_goals_tac bool_defs), |
|
63 (resolve_tac comp_rls 1), |
|
64 (typechk_tac[]), |
|
65 (ALLGOALS (etac TE)), |
|
66 (typechk_tac prems) ]); |
|
67 |
|
68 val boolC_false = prove_goal Bool.thy |
|
69 "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)" |
|
70 (fn prems=> |
|
71 [ (cut_facts_tac prems 1), |
|
72 (rewrite_goals_tac bool_defs), |
|
73 (resolve_tac comp_rls 1), |
|
74 (typechk_tac[]), |
|
75 (ALLGOALS (etac TE)), |
|
76 (typechk_tac prems) ]); |
|
77 |
|
78 writeln"Reached end of file."; |
|
79 |