# HG changeset patch
# User paulson
# Date 864643016 -7200
# Node ID a886795c9dce097f8b548f0e932d476684ea5602
# Parent  cfa72a70f2b558e0c3b14f51e46da2780ad5f406
Two results suggested by Florian Kammueller

diff -r cfa72a70f2b5 -r a886795c9dce src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon May 26 12:36:16 1997 +0200
+++ b/src/HOL/Finite.ML	Mon May 26 12:36:56 1997 +0200
@@ -150,6 +150,15 @@
 by (ALLGOALS Asm_simp_tac);
 qed "finite_imageI";
 
+(*The powerset of a finite set is finite*)
+goal Finite.thy "!!A. finite A ==> finite(Pow A)";
+by (etac finite_induct 1);
+by (ALLGOALS 
+    (asm_simp_tac
+     (!simpset addsimps [finite_UnI, finite_imageI, Pow_insert])));
+qed "finite_PowI";
+AddSIs [finite_PowI];
+
 val major::prems = goalw Finite.thy [finite_def]
     "[| finite A;                                       \
 \       P(A);                                           \
@@ -310,6 +319,19 @@
 Addsimps [card_insert];
 
 
+goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
+by (etac finite_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Step_tac 1);
+bw inj_onto_def;
+by (Blast_tac 1);
+by (stac card_insert_disjoint 1);
+by (etac finite_imageI 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "card_image";
+
+
 goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
 by (etac finite_induct 1);
 by (Simp_tac 1);