src/CTT/Bool.thy
 author wenzelm Tue, 11 Nov 2014 15:55:31 +0100 changeset 58977 9576b510f6a2 parent 58972 5b026cfc5f04 child 60770 240563fbf41d permissions -rw-r--r--
more symbols;
```
(*  Title:      CTT/Bool.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section {* The two-element type (booleans and conditionals) *}

theory Bool
imports CTT
begin

definition
Bool :: "t" where
"Bool == T+T"

definition
true :: "i" where
"true == inl(tt)"

definition
false :: "i" where
"false == inr(tt)"

definition
cond :: "[i,i,i]\<Rightarrow>i" where
"cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"

lemmas bool_defs = Bool_def true_def false_def cond_def

subsection {* Derivation of rules for the type Bool *}

(*formation rule*)
lemma boolF: "Bool type"
apply (unfold bool_defs)
apply typechk
done

(*introduction rules for true, false*)

lemma boolI_true: "true : Bool"
apply (unfold bool_defs)
apply typechk
done

lemma boolI_false: "false : Bool"
apply (unfold bool_defs)
apply typechk
done

(*elimination rule: typing of cond*)
lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
apply (unfold bool_defs)
apply typechk
apply (erule_tac [!] TE)
apply typechk
done

lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
\<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
apply (unfold bool_defs)
apply (rule PlusEL)
apply (erule asm_rl refl_elem [THEN TEL])+
done

(*computation rules for true, false*)

lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply typechk
apply (erule_tac [!] TE)
apply typechk
done

lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply typechk
apply (erule_tac [!] TE)
apply typechk
done

end
```