--- a/src/HOL/Relation.thy Sat Jun 16 07:13:17 2018 +0200
+++ b/src/HOL/Relation.thy Sat Jun 16 20:32:00 2018 +0200
@@ -836,8 +836,22 @@
by (auto simp: total_on_def)
lemma finite_converse [iff]: "finite (r\<inverse>) = finite r"
- unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
- by (auto elim: finite_imageD simp: inj_on_def)
+unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
+by (auto elim: finite_imageD simp: inj_on_def)
+
+lemma card_inverse[simp]: "card (R\<inverse>) = card R"
+proof -
+ have *: "\<And>R. prod.swap ` R = R\<inverse>" by auto
+ {
+ assume "\<not>finite R"
+ hence ?thesis
+ by auto
+ } moreover {
+ assume "finite R"
+ with card_image_le[of R prod.swap] card_image_le[of "R\<inverse>" prod.swap]
+ have ?thesis by (auto simp: *)
+ } ultimately show ?thesis by blast
+qed
lemma conversep_noteq [simp]: "(\<noteq>)\<inverse>\<inverse> = (\<noteq>)"
by (auto simp add: fun_eq_iff)
@@ -1030,8 +1044,11 @@
\<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close>
by blast
-lemma Image_empty [simp]: "R``{} = {}"
- by blast
+lemma Image_empty1 [simp]: "{} `` X = {}"
+by auto
+
+lemma Image_empty2 [simp]: "R``{} = {}"
+by blast
lemma Image_Id [simp]: "Id `` A = A"
by blast
@@ -1090,6 +1107,9 @@
lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
by auto
+lemma finite_Image[simp]: assumes "finite R" shows "finite (R `` A)"
+by(rule finite_subset[OF _ finite_Range[OF assms]]) auto
+
subsubsection \<open>Inverse image\<close>
--- a/src/HOL/Transitive_Closure.thy Sat Jun 16 07:13:17 2018 +0200
+++ b/src/HOL/Transitive_Closure.thy Sat Jun 16 20:32:00 2018 +0200
@@ -659,6 +659,13 @@
apply (auto simp add: finite_Field)
done
+lemma finite_rtrancl_Image: assumes "finite R" "finite A" shows "finite (R\<^sup>* `` A)"
+proof (rule ccontr)
+ assume "infinite (R\<^sup>* `` A)"
+ with assms show False
+ by(simp add: rtrancl_trancl_reflcl Un_Image del: reflcl_trancl)
+qed
+
text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should
be merged with main body.\<close>