--- a/src/CTT/Bool.thy Fri Jul 15 11:26:40 2016 +0200
+++ b/src/CTT/Bool.thy Fri Jul 15 15:19:04 2016 +0200
@@ -6,80 +6,68 @@
section \<open>The two-element type (booleans and conditionals)\<close>
theory Bool
-imports CTT
+ imports CTT
begin
-definition
- Bool :: "t" where
- "Bool \<equiv> T+T"
+definition Bool :: "t"
+ where "Bool \<equiv> T+T"
-definition
- true :: "i" where
- "true \<equiv> inl(tt)"
+definition true :: "i"
+ where "true \<equiv> inl(tt)"
-definition
- false :: "i" where
- "false \<equiv> inr(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)"
+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>
+subsection \<open>Derivation of rules for the type \<open>Bool\<close>\<close>
-(*formation rule*)
+text \<open>Formation rule.\<close>
lemma boolF: "Bool type"
-apply (unfold bool_defs)
-apply typechk
-done
+ unfolding bool_defs by typechk
-
-(*introduction rules for true, false*)
+text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>
lemma boolI_true: "true : Bool"
-apply (unfold bool_defs)
-apply typechk
-done
+ unfolding bool_defs by typechk
lemma boolI_false: "false : Bool"
-apply (unfold bool_defs)
-apply typechk
-done
+ unfolding bool_defs by typechk
-(*elimination rule: typing of cond*)
+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)"
-apply (unfold bool_defs)
-apply typechk
-apply (erule_tac [!] TE)
-apply typechk
-done
+ 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)"
-apply (unfold bool_defs)
-apply (rule PlusEL)
-apply (erule asm_rl refl_elem [THEN TEL])+
-done
+ unfolding bool_defs
+ apply (rule PlusEL)
+ apply (erule asm_rl refl_elem [THEN TEL])+
+ done
-(*computation rules for true, false*)
+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)"
-apply (unfold bool_defs)
-apply (rule comp_rls)
-apply typechk
-apply (erule_tac [!] TE)
-apply typechk
-done
+ 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)"
-apply (unfold bool_defs)
-apply (rule comp_rls)
-apply typechk
-apply (erule_tac [!] TE)
-apply typechk
-done
+ unfolding bool_defs
+ apply (rule comp_rls)
+ apply typechk
+ apply (erule_tac [!] TE)
+ apply typechk
+ done
end