--- a/src/ZF/Bool.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Bool.thy Tue Sep 27 16:51:35 2022 +0100
@@ -9,31 +9,31 @@
abbreviation
one (\<open>1\<close>) where
- "1 == succ(0)"
+ "1 \<equiv> succ(0)"
abbreviation
two (\<open>2\<close>) where
- "2 == succ(1)"
+ "2 \<equiv> succ(1)"
text\<open>2 is equal to bool, but is used as a number rather than a type.\<close>
-definition "bool == {0,1}"
+definition "bool \<equiv> {0,1}"
-definition "cond(b,c,d) == if(b=1,c,d)"
+definition "cond(b,c,d) \<equiv> if(b=1,c,d)"
-definition "not(b) == cond(b,0,1)"
+definition "not(b) \<equiv> cond(b,0,1)"
definition
"and" :: "[i,i]=>i" (infixl \<open>and\<close> 70) where
- "a and b == cond(a,b,0)"
+ "a and b \<equiv> cond(a,b,0)"
definition
or :: "[i,i]=>i" (infixl \<open>or\<close> 65) where
- "a or b == cond(a,1,b)"
+ "a or b \<equiv> cond(a,1,b)"
definition
xor :: "[i,i]=>i" (infixl \<open>xor\<close> 65) where
- "a xor b == cond(a,not(b),b)"
+ "a xor b \<equiv> cond(a,not(b),b)"
lemmas bool_defs = bool_def cond_def
@@ -52,11 +52,11 @@
lemma one_not_0: "1\<noteq>0"
by (simp add: bool_defs )
-(** 1=0 ==> R **)
+(** 1=0 \<Longrightarrow> R **)
lemmas one_neq_0 = one_not_0 [THEN notE]
lemma boolE:
- "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P"
+ "\<lbrakk>c: bool; c=1 \<Longrightarrow> P; c=0 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (simp add: bool_defs, blast)
(** cond **)
@@ -69,17 +69,17 @@
lemma cond_0 [simp]: "cond(0,c,d) = d"
by (simp add: bool_defs )
-lemma cond_type [TC]: "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)"
+lemma cond_type [TC]: "\<lbrakk>b: bool; c: A(1); d: A(0)\<rbrakk> \<Longrightarrow> cond(b,c,d): A(b)"
by (simp add: bool_defs, blast)
(*For Simp_tac and Blast_tac*)
-lemma cond_simple_type: "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A"
+lemma cond_simple_type: "\<lbrakk>b: bool; c: A; d: A\<rbrakk> \<Longrightarrow> cond(b,c,d): A"
by (simp add: bool_defs )
-lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"
+lemma def_cond_1: "\<lbrakk>\<And>b. j(b)\<equiv>cond(b,c,d)\<rbrakk> \<Longrightarrow> j(1) = c"
by simp
-lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
+lemma def_cond_0: "\<lbrakk>\<And>b. j(b)\<equiv>cond(b,c,d)\<rbrakk> \<Longrightarrow> j(0) = d"
by simp
lemmas not_1 = not_def [THEN def_cond_1, simp]
@@ -94,16 +94,16 @@
lemmas xor_1 = xor_def [THEN def_cond_1, simp]
lemmas xor_0 = xor_def [THEN def_cond_0, simp]
-lemma not_type [TC]: "a:bool ==> not(a) \<in> bool"
+lemma not_type [TC]: "a:bool \<Longrightarrow> not(a) \<in> bool"
by (simp add: not_def)
-lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b \<in> bool"
+lemma and_type [TC]: "\<lbrakk>a:bool; b:bool\<rbrakk> \<Longrightarrow> a and b \<in> bool"
by (simp add: and_def)
-lemma or_type [TC]: "[| a:bool; b:bool |] ==> a or b \<in> bool"
+lemma or_type [TC]: "\<lbrakk>a:bool; b:bool\<rbrakk> \<Longrightarrow> a or b \<in> bool"
by (simp add: or_def)
-lemma xor_type [TC]: "[| a:bool; b:bool |] ==> a xor b \<in> bool"
+lemma xor_type [TC]: "\<lbrakk>a:bool; b:bool\<rbrakk> \<Longrightarrow> a xor b \<in> bool"
by (simp add: xor_def)
lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
@@ -111,49 +111,49 @@
subsection\<open>Laws About 'not'\<close>
-lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
+lemma not_not [simp]: "a:bool \<Longrightarrow> not(not(a)) = a"
by (elim boolE, auto)
-lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"
+lemma not_and [simp]: "a:bool \<Longrightarrow> not(a and b) = not(a) or not(b)"
by (elim boolE, auto)
-lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
+lemma not_or [simp]: "a:bool \<Longrightarrow> not(a or b) = not(a) and not(b)"
by (elim boolE, auto)
subsection\<open>Laws About 'and'\<close>
-lemma and_absorb [simp]: "a: bool ==> a and a = a"
+lemma and_absorb [simp]: "a: bool \<Longrightarrow> a and a = a"
by (elim boolE, auto)
-lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"
+lemma and_commute: "\<lbrakk>a: bool; b:bool\<rbrakk> \<Longrightarrow> a and b = b and a"
by (elim boolE, auto)
-lemma and_assoc: "a: bool ==> (a and b) and c = a and (b and c)"
+lemma and_assoc: "a: bool \<Longrightarrow> (a and b) and c = a and (b and c)"
by (elim boolE, auto)
-lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
+lemma and_or_distrib: "\<lbrakk>a: bool; b:bool; c:bool\<rbrakk> \<Longrightarrow>
(a or b) and c = (a and c) or (b and c)"
by (elim boolE, auto)
subsection\<open>Laws About 'or'\<close>
-lemma or_absorb [simp]: "a: bool ==> a or a = a"
+lemma or_absorb [simp]: "a: bool \<Longrightarrow> a or a = a"
by (elim boolE, auto)
-lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"
+lemma or_commute: "\<lbrakk>a: bool; b:bool\<rbrakk> \<Longrightarrow> a or b = b or a"
by (elim boolE, auto)
-lemma or_assoc: "a: bool ==> (a or b) or c = a or (b or c)"
+lemma or_assoc: "a: bool \<Longrightarrow> (a or b) or c = a or (b or c)"
by (elim boolE, auto)
-lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
+lemma or_and_distrib: "\<lbrakk>a: bool; b: bool; c: bool\<rbrakk> \<Longrightarrow>
(a and b) or c = (a or c) and (b or c)"
by (elim boolE, auto)
definition
bool_of_o :: "o=>i" where
- "bool_of_o(P) == (if P then 1 else 0)"
+ "bool_of_o(P) \<equiv> (if P then 1 else 0)"
lemma [simp]: "bool_of_o(True) = 1"
by (simp add: bool_of_o_def)
@@ -167,7 +167,7 @@
lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
by (simp add: bool_of_o_def)
-lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
+lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> \<not>P"
by (simp add: bool_of_o_def)
end