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 twoelement 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
