--- a/src/ZF/Induct/Rmap.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Induct/Rmap.thy Tue Sep 27 16:51:35 2022 +0100
@@ -15,12 +15,12 @@
intros
NilI: "<Nil,Nil> \<in> rmap(r)"
- ConsI: "[| <x,y>: r; <xs,ys> \<in> rmap(r) |]
- ==> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
+ ConsI: "\<lbrakk><x,y>: r; <xs,ys> \<in> rmap(r)\<rbrakk>
+ \<Longrightarrow> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
type_intros domainI rangeI list.intros
-lemma rmap_mono: "r \<subseteq> s ==> rmap(r) \<subseteq> rmap(s)"
+lemma rmap_mono: "r \<subseteq> s \<Longrightarrow> rmap(r) \<subseteq> rmap(s)"
apply (unfold rmap.defs)
apply (rule lfp_mono)
apply (rule rmap.bnd_mono)+
@@ -33,19 +33,19 @@
declare rmap.intros [intro]
-lemma rmap_rel_type: "r \<subseteq> A \<times> B ==> rmap(r) \<subseteq> list(A) \<times> list(B)"
+lemma rmap_rel_type: "r \<subseteq> A \<times> B \<Longrightarrow> rmap(r) \<subseteq> list(A) \<times> list(B)"
apply (rule rmap.dom_subset [THEN subset_trans])
apply (assumption |
rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
done
-lemma rmap_total: "A \<subseteq> domain(r) ==> list(A) \<subseteq> domain(rmap(r))"
+lemma rmap_total: "A \<subseteq> domain(r) \<Longrightarrow> list(A) \<subseteq> domain(rmap(r))"
apply (rule subsetI)
apply (erule list.induct)
apply blast+
done
-lemma rmap_functional: "function(r) ==> function(rmap(r))"
+lemma rmap_functional: "function(r) \<Longrightarrow> function(rmap(r))"
apply (unfold function_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule rmap.induct)
@@ -57,14 +57,14 @@
as expected.
\<close>
-lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
+lemma rmap_fun_type: "f \<in> A->B \<Longrightarrow> rmap(f): list(A)->list(B)"
by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
lemma rmap_Nil: "rmap(f)`Nil = Nil"
by (unfold apply_def) blast
-lemma rmap_Cons: "[| f \<in> A->B; x \<in> A; xs: list(A) |]
- ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
+lemma rmap_Cons: "\<lbrakk>f \<in> A->B; x \<in> A; xs: list(A)\<rbrakk>
+ \<Longrightarrow> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
end