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