|
1474
|
1 |
(* Title: CTT/bool
|
|
0
|
2 |
ID: $Id$
|
|
1474
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
0
|
4 |
Copyright 1991 University of Cambridge
|
|
|
5 |
*)
|
|
|
6 |
|
|
17441
|
7 |
header {* The two-element type (booleans and conditionals) *}
|
|
|
8 |
|
|
|
9 |
theory Bool
|
|
|
10 |
imports CTT
|
|
|
11 |
begin
|
|
0
|
12 |
|
|
19762
|
13 |
definition
|
|
19761
|
14 |
Bool :: "t"
|
|
|
15 |
"Bool == T+T"
|
|
|
16 |
|
|
|
17 |
true :: "i"
|
|
|
18 |
"true == inl(tt)"
|
|
|
19 |
|
|
|
20 |
false :: "i"
|
|
|
21 |
"false == inr(tt)"
|
|
|
22 |
|
|
|
23 |
cond :: "[i,i,i]=>i"
|
|
|
24 |
"cond(a,b,c) == when(a, %u. b, %u. c)"
|
|
|
25 |
|
|
|
26 |
lemmas bool_defs = Bool_def true_def false_def cond_def
|
|
|
27 |
|
|
|
28 |
|
|
|
29 |
subsection {* Derivation of rules for the type Bool *}
|
|
|
30 |
|
|
|
31 |
(*formation rule*)
|
|
|
32 |
lemma boolF: "Bool type"
|
|
|
33 |
apply (unfold bool_defs)
|
|
|
34 |
apply (tactic "typechk_tac []")
|
|
|
35 |
done
|
|
|
36 |
|
|
|
37 |
|
|
|
38 |
(*introduction rules for true, false*)
|
|
|
39 |
|
|
|
40 |
lemma boolI_true: "true : Bool"
|
|
|
41 |
apply (unfold bool_defs)
|
|
|
42 |
apply (tactic "typechk_tac []")
|
|
|
43 |
done
|
|
|
44 |
|
|
|
45 |
lemma boolI_false: "false : Bool"
|
|
|
46 |
apply (unfold bool_defs)
|
|
|
47 |
apply (tactic "typechk_tac []")
|
|
|
48 |
done
|
|
17441
|
49 |
|
|
19761
|
50 |
(*elimination rule: typing of cond*)
|
|
|
51 |
lemma boolE:
|
|
|
52 |
"[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"
|
|
|
53 |
apply (unfold bool_defs)
|
|
|
54 |
apply (tactic "typechk_tac []")
|
|
|
55 |
apply (erule_tac [!] TE)
|
|
|
56 |
apply (tactic "typechk_tac []")
|
|
|
57 |
done
|
|
|
58 |
|
|
|
59 |
lemma boolEL:
|
|
|
60 |
"[| p = q : Bool; a = c : C(true); b = d : C(false) |]
|
|
|
61 |
==> cond(p,a,b) = cond(q,c,d) : C(p)"
|
|
|
62 |
apply (unfold bool_defs)
|
|
|
63 |
apply (rule PlusEL)
|
|
|
64 |
apply (erule asm_rl refl_elem [THEN TEL])+
|
|
|
65 |
done
|
|
|
66 |
|
|
|
67 |
(*computation rules for true, false*)
|
|
|
68 |
|
|
|
69 |
lemma boolC_true:
|
|
|
70 |
"[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"
|
|
|
71 |
apply (unfold bool_defs)
|
|
|
72 |
apply (rule comp_rls)
|
|
|
73 |
apply (tactic "typechk_tac []")
|
|
|
74 |
apply (erule_tac [!] TE)
|
|
|
75 |
apply (tactic "typechk_tac []")
|
|
|
76 |
done
|
|
|
77 |
|
|
|
78 |
lemma boolC_false:
|
|
|
79 |
"[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)"
|
|
|
80 |
apply (unfold bool_defs)
|
|
|
81 |
apply (rule comp_rls)
|
|
|
82 |
apply (tactic "typechk_tac []")
|
|
|
83 |
apply (erule_tac [!] TE)
|
|
|
84 |
apply (tactic "typechk_tac []")
|
|
|
85 |
done
|
|
17441
|
86 |
|
|
0
|
87 |
end
|