equal
deleted
inserted
replaced
1 (* Title: CTT/Bool |
1 (* Title: CTT/Bool |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
|
6 The two-element type (booleans and conditionals) |
|
7 *) |
5 *) |
8 |
6 |
9 val bool_defs = [Bool_def,true_def,false_def,cond_def]; |
7 val bool_defs = [Bool_def,true_def,false_def,cond_def]; |
10 |
8 |
11 (*Derivation of rules for the type Bool*) |
9 (*Derivation of rules for the type Bool*) |
25 Goalw bool_defs "false : Bool"; |
23 Goalw bool_defs "false : Bool"; |
26 by (typechk_tac []) ; |
24 by (typechk_tac []) ; |
27 qed "boolI_false"; |
25 qed "boolI_false"; |
28 |
26 |
29 (*elimination rule: typing of cond*) |
27 (*elimination rule: typing of cond*) |
30 Goalw bool_defs |
28 Goalw bool_defs |
31 "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"; |
29 "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"; |
32 by (typechk_tac []); |
30 by (typechk_tac []); |
33 by (ALLGOALS (etac TE)); |
31 by (ALLGOALS (etac TE)); |
34 by (typechk_tac []) ; |
32 by (typechk_tac []) ; |
35 qed "boolE"; |
33 qed "boolE"; |
41 by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ; |
39 by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ; |
42 qed "boolEL"; |
40 qed "boolEL"; |
43 |
41 |
44 (*computation rules for true, false*) |
42 (*computation rules for true, false*) |
45 |
43 |
46 Goalw bool_defs |
44 Goalw bool_defs |
47 "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"; |
45 "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"; |
48 by (resolve_tac comp_rls 1); |
46 by (resolve_tac comp_rls 1); |
49 by (typechk_tac []); |
47 by (typechk_tac []); |
50 by (ALLGOALS (etac TE)); |
48 by (ALLGOALS (etac TE)); |
51 by (typechk_tac []) ; |
49 by (typechk_tac []) ; |
56 by (resolve_tac comp_rls 1); |
54 by (resolve_tac comp_rls 1); |
57 by (typechk_tac []); |
55 by (typechk_tac []); |
58 by (ALLGOALS (etac TE)); |
56 by (ALLGOALS (etac TE)); |
59 by (typechk_tac []) ; |
57 by (typechk_tac []) ; |
60 qed "boolC_false"; |
58 qed "boolC_false"; |
61 |
|
62 writeln"Reached end of file."; |
|
63 |
|