src/CTT/Bool.thy
 author wenzelm Tue, 24 Jul 2012 21:36:53 +0200 changeset 48487 94a9650f79fb parent 41959 b460124855b8 child 58889 5b7a9633cfa8 permissions -rw-r--r--
tuned order;
```
(*  Title:      CTT/Bool.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

header {* 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]=>i" where
"cond(a,b,c) == when(a, %u. b, %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 (tactic "typechk_tac []")
done

(*introduction rules for true, false*)

lemma boolI_true: "true : Bool"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
done

lemma boolI_false: "false : Bool"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
done

(*elimination rule: typing of cond*)
lemma boolE:
"[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
apply (unfold bool_defs)
apply (tactic "typechk_tac []")
apply (erule_tac [!] TE)
apply (tactic "typechk_tac []")
done

lemma boolEL:
"[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]
==> 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:
"[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply (tactic "typechk_tac []")
apply (erule_tac [!] TE)
apply (tactic "typechk_tac []")
done

lemma boolC_false:
"[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply (tactic "typechk_tac []")
apply (erule_tac [!] TE)
apply (tactic "typechk_tac []")
done

end
```