# HG changeset patch
# User paulson
# Date 978686326 -3600
# Node ID 53547a02f2a14925c55e625e8989940d14165d4f
# Parent  27e4d90b35b50446b127a033614d9e7af4c33c71
finite_trancl: new theorem by Sidi Ehmety

diff -r 27e4d90b35b5 -r 53547a02f2a1 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jan 05 10:17:48 2001 +0100
+++ b/src/HOL/Finite.ML	Fri Jan 05 10:18:46 2001 +0100
@@ -248,6 +248,29 @@
 by Auto_tac;
 qed "bounded_nat_set_is_finite";
 
+(** Finiteness of transitive closure (thanks to Sidi Ehmety) **)
+
+(*A finite relation has a finite field ( = domain U range) *)
+Goal "finite r ==> finite (Field r)";
+by (etac finite_induct 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [Field_def, Domain_insert, Range_insert]));
+qed "finite_Field";
+
+Goal "r^+ <= Field r <*> Field r";
+by (Clarify_tac 1);
+by (etac trancl_induct 1);
+by (auto_tac (claset(), simpset() addsimps [Field_def]));  
+qed "trancl_subset_Field2";
+
+Goal "finite (r^+) = finite r";
+by Auto_tac;
+by (rtac (trancl_subset_Field2 RS finite_subset) 2);
+by (rtac finite_SigmaI 2);
+by (blast_tac (claset() addIs [r_into_trancl, finite_subset]) 1);
+by (auto_tac (claset(), simpset() addsimps [finite_Field]));  
+qed "finite_trancl";
+
 
 section "Finite cardinality -- 'card'";