src/CTT/Bool.thy

misc tuning;

(*  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>_. b, \<lambda>_. c)"

lemmas bool_defs = Bool_def true_def false_def cond_def


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

text \<open>Formation rule.\<close>
lemma boolF: "Bool type"
  unfolding bool_defs by typechk

text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>

lemma boolI_true: "true : Bool"
  unfolding bool_defs by typechk

lemma boolI_false: "false : Bool"
  unfolding bool_defs by typechk

text \<open>Elimination rule: typing of \<open>cond\<close>.\<close>
lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
  unfolding bool_defs
  apply (typechk; erule 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)"
  unfolding bool_defs
  apply (rule PlusEL)
    apply (erule asm_rl refl_elem [THEN TEL])+
  done

text \<open>Computation rules for \<open>true\<close>, \<open>false\<close>.\<close>

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

end