src/ZF/Coind/Map.thy

--- a/src/ZF/Coind/Map.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Coind/Map.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -9,25 +9,25 @@
 
 definition
   TMap :: "[i,i] => i"  where
-   "TMap(A,B) == {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}"
+   "TMap(A,B) \<equiv> {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}"
 
 definition
   PMap :: "[i,i] => i"  where
-   "PMap(A,B) == TMap(A,cons(0,B))"
+   "PMap(A,B) \<equiv> TMap(A,cons(0,B))"
 
-(* Note: 0 \<in> B ==> TMap(A,B) = PMap(A,B) *)
+(* Note: 0 \<in> B \<Longrightarrow> TMap(A,B) = PMap(A,B) *)
   
 definition
   map_emp :: i  where
-   "map_emp == 0"
+   "map_emp \<equiv> 0"
 
 definition
   map_owr :: "[i,i,i]=>i"  where
-   "map_owr(m,a,b) == \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
+   "map_owr(m,a,b) \<equiv> \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
 
 definition
   map_app :: "[i,i]=>i"  where
-   "map_app(m,a) == m``{a}"
+   "map_app(m,a) \<equiv> m``{a}"
   
 lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})"
 by (unfold TMap_def, blast)
@@ -51,13 +51,13 @@
 lemma qbeta_if: "Sigma(A,B)``{a} = (if a \<in> A then B(a) else 0)"
 by auto
 
-lemma qbeta: "a \<in> A ==> Sigma(A,B)``{a} = B(a)"
+lemma qbeta: "a \<in> A \<Longrightarrow> Sigma(A,B)``{a} = B(a)"
 by fast
 
-lemma qbeta_emp: "a\<notin>A ==> Sigma(A,B)``{a} = 0"
+lemma qbeta_emp: "a\<notin>A \<Longrightarrow> Sigma(A,B)``{a} = 0"
 by fast
 
-lemma image_Sigma1: "a \<notin> A ==> Sigma(A,B)``{a}=0"
+lemma image_Sigma1: "a \<notin> A \<Longrightarrow> Sigma(A,B)``{a}=0"
 by fast
 
 
@@ -68,7 +68,7 @@
 (* Lemmas *)
 
 lemma MapQU_lemma: 
-    "A \<subseteq> univ(X) ==> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
+    "A \<subseteq> univ(X) \<Longrightarrow> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
 apply (unfold quniv_def)
 apply (rule Pow_mono)
 apply (rule subset_trans [OF Sigma_mono product_univ])
@@ -80,7 +80,7 @@
 (* Theorems *)
 
 lemma mapQU:
-  "[| m \<in> PMap(A,quniv(B)); !!x. x \<in> A ==> x \<in> univ(B) |] ==> m \<in> quniv(B)"
+  "\<lbrakk>m \<in> PMap(A,quniv(B)); \<And>x. x \<in> A \<Longrightarrow> x \<in> univ(B)\<rbrakk> \<Longrightarrow> m \<in> quniv(B)"
 apply (unfold PMap_def TMap_def)
 apply (blast intro!: MapQU_lemma [THEN subsetD]) 
 done
@@ -89,7 +89,7 @@
 (* Monotonicity                                                 *)
 (* ############################################################ *)
 
-lemma PMap_mono: "B \<subseteq> C ==> PMap(A,B)<=PMap(A,C)"
+lemma PMap_mono: "B \<subseteq> C \<Longrightarrow> PMap(A,B)<=PMap(A,C)"
 by (unfold PMap_def TMap_def, blast)
 
 
@@ -105,7 +105,7 @@
 (** map_owr **)
 
 lemma pmap_owrI: 
-  "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |]  ==> map_owr(m,a,b):PMap(A,B)"
+  "\<lbrakk>m \<in> PMap(A,B); a \<in> A; b \<in> B\<rbrakk>  \<Longrightarrow> map_owr(m,a,b):PMap(A,B)"
 apply (unfold map_owr_def PMap_def TMap_def, safe)
 apply (simp_all add: if_iff, auto)
 (*Remaining subgoal*)
@@ -118,15 +118,15 @@
 (** map_app **)
 
 lemma tmap_app_notempty: 
-  "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a) \<noteq>0"
+  "\<lbrakk>m \<in> TMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> map_app(m,a) \<noteq>0"
 by (unfold TMap_def map_app_def, blast)
 
 lemma tmap_appI: 
-  "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
+  "\<lbrakk>m \<in> TMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> map_app(m,a):B"
 by (unfold TMap_def map_app_def domain_def, blast)
 
 lemma pmap_appI: 
-  "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
+  "\<lbrakk>m \<in> PMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> map_app(m,a):B"
 apply (unfold PMap_def)
 apply (frule tmap_app_notempty, assumption)
 apply (drule tmap_appI, auto)
@@ -135,11 +135,11 @@
 (** domain **)
 
 lemma tmap_domainD: 
-  "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
+  "\<lbrakk>m \<in> TMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> a \<in> A"
 by (unfold TMap_def, blast)
 
 lemma pmap_domainD: 
-  "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
+  "\<lbrakk>m \<in> PMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> a \<in> A"
 by (unfold PMap_def TMap_def, blast)
 
 
@@ -164,7 +164,7 @@
 by (unfold map_emp_def, blast)
 
 lemma map_domain_owr: 
-  "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
+  "b \<noteq> 0 \<Longrightarrow> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
 apply (unfold map_owr_def)
 apply (auto simp add: domain_Sigma)
 done
@@ -178,7 +178,7 @@
 lemma map_app_owr1: "map_app(map_owr(f,a,b),a) = b"
 by (simp add: map_app_owr)
 
-lemma map_app_owr2: "c \<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"
+lemma map_app_owr2: "c \<noteq> a \<Longrightarrow> map_app(map_owr(f,a,b),c)= map_app(f,c)"
 by (simp add: map_app_owr)
 
 end