# HG changeset patch
# User nipkow
# Date 1529173920 -7200
# Node ID b33803fcae2a4d4fc294903f1322b7bfe9386467
# Parent  f35aa0e7255d3629915073ce885a376824bda65d
moved lemmas from AFP

diff -r f35aa0e7255d -r b33803fcae2a src/HOL/Relation.thy
--- 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>
 
diff -r f35aa0e7255d -r b33803fcae2a src/HOL/Transitive_Closure.thy
--- 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>