src/CTT/Bool.thy

prefer infix operations;

(*  Title:      CTT/Bool.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

section \<open>The two-element type (booleans and conditionals)\<close>

theory Bool
imports CTT
begin

definition
  Bool :: "t" where
  "Bool \<equiv> T+T"

definition
  true :: "i" where
  "true \<equiv> inl(tt)"

definition
  false :: "i" where
  "false \<equiv> inr(tt)"

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

lemmas bool_defs = Bool_def true_def false_def cond_def


subsection \<open>Derivation of rules for the type Bool\<close>

(*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