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