# HG changeset patch
# User haftmann
# Date 1365107399 -7200
# Node ID 183f30bc11dec7b75818fda6b81811818a7a9a2e
# Parent  8c0f6caba80e70dd0fd7ab48616f850deb119ac0
convenient induction rule

diff -r 8c0f6caba80e -r 183f30bc11de src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Apr 04 20:59:16 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Apr 04 22:29:59 2013 +0200
@@ -39,6 +39,17 @@
   qed
 qed
 
+lemma infinite_finite_induct [case_names infinite empty insert]:
+  assumes infinite: "\<And>A. \<not> finite A \<Longrightarrow> P A"
+  assumes empty: "P {}"
+  assumes insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
+  shows "P A"
+proof (cases "finite A")
+  case False with infinite show ?thesis .
+next
+  case True then show ?thesis by (induct A) (fact empty insert)+
+qed
+
 
 subsubsection {* Choice principles *}