# HG changeset patch
# User paulson
# Date 1150386630 -7200
# Node ID 7546dafb3fc6f77b03fb7849532ebcaaaddc4f63
# Parent  e41ef99d9bb38eceb7fbcd2601c4cbbdacb93553
the enumerate operator

diff -r e41ef99d9bb3 -r 7546dafb3fc6 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Wed Jun 14 16:18:10 2006 +0200
+++ b/src/HOL/Infinite_Set.thy	Thu Jun 15 17:50:30 2006 +0200
@@ -407,6 +407,46 @@
 by (simp add: MOST_def INF_nat_le)
 
 
+subsection "Enumeration of an Infinite Set"
+
+text{*The set's element type must be wellordered (e.g. the natural numbers)*}
+consts
+  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
+
+primrec
+  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
+  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
+
+lemma enumerate_Suc':
+   "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
+by simp
+
+lemma enumerate_in_set [rule_format]: "\<forall>S. infinite S --> enumerate S n : S"
+apply (induct n) 
+ apply (force intro: LeastI dest!:infinite_imp_nonempty)
+apply (auto iff: finite_Diff_singleton) 
+done
+
+declare enumerate_0 [simp del] enumerate_Suc [simp del]
+
+lemma enumerate_step [rule_format]:
+     "\<forall>S. infinite S --> enumerate S n < enumerate S (Suc n)"
+apply (induct n, clarify) 
+ apply (rule order_le_neq_trans)
+  apply (simp add: enumerate_0 Least_le enumerate_in_set) 
+ apply (simp only: enumerate_Suc') 
+ apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
+  apply (blast intro: sym)
+ apply (simp add: enumerate_in_set del: Diff_iff) 
+apply (simp add: enumerate_Suc') 
+done
+
+lemma enumerate_mono: "[|m<n; infinite S|] ==> enumerate S m < enumerate S n"
+apply (erule less_Suc_induct) 
+apply (auto intro: enumerate_step) 
+done
+
+
 subsection "Miscellaneous"
 
 text {*