41959
|
1 |
(* Title: CTT/Bool.thy
|
1474
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
3 |
Copyright 1991 University of Cambridge
|
|
4 |
*)
|
|
5 |
|
60770
|
6 |
section \<open>The two-element type (booleans and conditionals)\<close>
|
17441
|
7 |
|
|
8 |
theory Bool
|
63505
|
9 |
imports CTT
|
17441
|
10 |
begin
|
0
|
11 |
|
63505
|
12 |
definition Bool :: "t"
|
|
13 |
where "Bool \<equiv> T+T"
|
19761
|
14 |
|
63505
|
15 |
definition true :: "i"
|
|
16 |
where "true \<equiv> inl(tt)"
|
19761
|
17 |
|
63505
|
18 |
definition false :: "i"
|
|
19 |
where "false \<equiv> inr(tt)"
|
19761
|
20 |
|
63505
|
21 |
definition cond :: "[i,i,i]\<Rightarrow>i"
|
|
22 |
where "cond(a,b,c) \<equiv> when(a, \<lambda>u. b, \<lambda>u. c)"
|
19761
|
23 |
|
|
24 |
lemmas bool_defs = Bool_def true_def false_def cond_def
|
|
25 |
|
|
26 |
|
63505
|
27 |
subsection \<open>Derivation of rules for the type \<open>Bool\<close>\<close>
|
19761
|
28 |
|
63505
|
29 |
text \<open>Formation rule.\<close>
|
19761
|
30 |
lemma boolF: "Bool type"
|
63505
|
31 |
unfolding bool_defs by typechk
|
19761
|
32 |
|
63505
|
33 |
text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>
|
19761
|
34 |
|
|
35 |
lemma boolI_true: "true : Bool"
|
63505
|
36 |
unfolding bool_defs by typechk
|
19761
|
37 |
|
|
38 |
lemma boolI_false: "false : Bool"
|
63505
|
39 |
unfolding bool_defs by typechk
|
17441
|
40 |
|
63505
|
41 |
text \<open>Elimination rule: typing of \<open>cond\<close>.\<close>
|
58977
|
42 |
lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
|
63505
|
43 |
unfolding bool_defs
|
|
44 |
apply (typechk; erule TE)
|
|
45 |
apply typechk
|
|
46 |
done
|
19761
|
47 |
|
58977
|
48 |
lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
|
|
49 |
\<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
|
63505
|
50 |
unfolding bool_defs
|
|
51 |
apply (rule PlusEL)
|
|
52 |
apply (erule asm_rl refl_elem [THEN TEL])+
|
|
53 |
done
|
19761
|
54 |
|
63505
|
55 |
text \<open>Computation rules for \<open>true\<close>, \<open>false\<close>.\<close>
|
19761
|
56 |
|
58977
|
57 |
lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
|
63505
|
58 |
unfolding bool_defs
|
|
59 |
apply (rule comp_rls)
|
|
60 |
apply typechk
|
|
61 |
apply (erule_tac [!] TE)
|
|
62 |
apply typechk
|
|
63 |
done
|
19761
|
64 |
|
58977
|
65 |
lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
|
63505
|
66 |
unfolding bool_defs
|
|
67 |
apply (rule comp_rls)
|
|
68 |
apply typechk
|
|
69 |
apply (erule_tac [!] TE)
|
|
70 |
apply typechk
|
|
71 |
done
|
17441
|
72 |
|
0
|
73 |
end
|