# HG changeset patch # User nipkow # Date 865532653 -7200 # Node ID 6d9e0cca6083828ddadbf03ba636998ea17aec60 # Parent c068bd2f0bbd58f0e850fa3d1bb15fe99e14f0e4 added finite_converse diff -r c068bd2f0bbd -r 6d9e0cca6083 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Thu Jun 05 17:19:05 1997 +0200 +++ b/src/HOL/Finite.ML Thu Jun 05 19:44:13 1997 +0200 @@ -174,6 +174,22 @@ qed "finite_Pow_iff"; AddIffs [finite_Pow_iff]; +goal Finite.thy "finite(converse r) = finite r"; +by(subgoal_tac "converse r = (%(x,y).(y,x))``r" 1); + by(Asm_simp_tac 1); + br iffI 1; + be (rewrite_rule [inj_onto_def] finite_imageD) 1; + by(simp_tac (!simpset setloop (split_tac[expand_split])) 1); + be finite_imageI 1; +by(simp_tac (!simpset addsimps [converse_def,image_def]) 1); +by(Auto_tac()); + br bexI 1; + ba 2; + by(Simp_tac 1); +by(split_all_tac 1); +by(Asm_full_simp_tac 1); +qed "finite_converse"; +AddIffs [finite_converse]; section "Finite cardinality -- 'card'";