summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Andreas Lochbihler |

Thu, 30 Jul 2015 09:49:43 +0200 | |

changeset 60828 | e9e272fa8daf |

parent 60827 | 31e08fe243f1 |

child 60836 | c5db501da8e4 |

add coinduction rule for infinite

--- 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.