# HG changeset patch
# User Andreas Lochbihler
# Date 1438242583 -7200
# Node ID e9e272fa8daf97e1a75a1c76c33c0108d1cacff9
# Parent  31e08fe243f14e20b57479c744fcfc41d3ec2cdd
add coinduction rule for infinite

diff -r 31e08fe243f1 -r e9e272fa8daf src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Tue Jul 28 23:29:13 2015 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jul 30 09:49:43 2015 +0200
@@ -62,6 +62,16 @@
   with S show False by simp
 qed
 
+lemma infinite_coinduct [consumes 1, case_names infinite]:
+  assumes "X A"
+  and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
+  shows "infinite A"
+proof
+  assume "finite A"
+  then show False using \<open>X A\<close>
+    by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step)
+qed    
+
 text \<open>
   As a concrete example, we prove that the set of natural numbers is
   infinite.