src/CTT/Bool.thy
 changeset 58977 9576b510f6a2 parent 58972 5b026cfc5f04 child 60770 240563fbf41d
```--- a/src/CTT/Bool.thy	Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/Bool.thy	Tue Nov 11 15:55:31 2014 +0100
@@ -22,8 +22,8 @@
"false == inr(tt)"

definition
-  cond :: "[i,i,i]=>i" where
-  "cond(a,b,c) == when(a, %u. b, %u. c)"
+  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

@@ -50,17 +50,15 @@
done

(*elimination rule: typing of cond*)
-lemma boolE:
-    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
+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:
-    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]
-     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
+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])+
@@ -68,8 +66,7 @@

(*computation rules for true, false*)

-lemma boolC_true:
-    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+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
@@ -77,8 +74,7 @@
apply typechk
done

-lemma boolC_false:
-    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+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```