# HG changeset patch
# User haftmann
# Date 1247666406 -7200
# Node ID 05d915945bc60d3c0553709bc4c493b7e7c8c7a5
# Parent  0e209ff7f236c919ba98b1a71b12695696e665c1# Parent  0a83608e21f11435d29da98e3bbe9d5205383daa
merged

diff -r 0a83608e21f1 -r 05d915945bc6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Jul 15 10:11:13 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 15 16:00:06 2009 +0200
@@ -93,6 +93,7 @@
   qed
 qed
 
+
 text{* A finite choice principle. Does not need the SOME choice operator. *}
 lemma finite_set_choice:
   "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
@@ -2122,6 +2123,18 @@
   \<Longrightarrow> x \<inter> \<Union> F = {}"
 by auto
 
+lemma finite_psubset_induct[consumes 1, case_names psubset]:
+  assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
+using assms(1)
+proof (induct A rule: measure_induct_rule[where f=card])
+  case (less A)
+  show ?case
+  proof(rule assms(2)[OF less(2)])
+    fix B assume "finite B" "B \<subset> A"
+    show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
+  qed
+qed
+
 text{* main cardinality theorem *}
 lemma card_partition [rule_format]:
   "finite C ==>
@@ -3252,13 +3265,13 @@
     by (simp add: Max fold1_antimono [folded dual_max])
 qed
 
-lemma finite_linorder_induct[consumes 1, case_names empty insert]:
+lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  "finite A \<Longrightarrow> P {} \<Longrightarrow>
   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
   \<Longrightarrow> P A"
-proof (induct A rule: measure_induct_rule[where f=card])
+proof (induct rule: finite_psubset_induct)
   fix A :: "'a set"
-  assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
+  assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
                   \<Longrightarrow> P B"
   and "finite A" and "P {}"
@@ -3271,16 +3284,17 @@
     assume "A \<noteq> {}"
     with `finite A` have "Max A : A" by auto
     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
-    note card_Diff1_less[OF `finite A` `Max A : A`]
     moreover have "finite ?B" using `finite A` by simp
     ultimately have "P ?B" using `P {}` step IH by blast
-    moreover have "\<forall>a\<in>?B. a < Max A"
-      using Max_ge [OF `finite A`] by fastsimp
-    ultimately show "P A"
-      using A insert_Diff_single step[OF `finite ?B`] by fastsimp
+    moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
+    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
   qed
 qed
 
+lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
+  "\<lbrakk>finite A; P {}; \<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
+by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
+
 end
 
 context ordered_ab_semigroup_add
diff -r 0a83608e21f1 -r 05d915945bc6 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jul 15 10:11:13 2009 +0200
+++ b/src/HOL/List.thy	Wed Jul 15 16:00:06 2009 +0200
@@ -2268,6 +2268,8 @@
 -- {* simp does not terminate! *}
 by (induct j) auto
 
+lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
+
 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
 by (subst upt_rec) simp
 
@@ -3202,6 +3204,8 @@
 lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
 by(rule upto_rec2[where 'a = int, simplified successor_int_def])
 
+lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard]
+
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
diff -r 0a83608e21f1 -r 05d915945bc6 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Jul 15 10:11:13 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jul 15 16:00:06 2009 +0200
@@ -425,7 +425,7 @@
 proof cases
   assume "finite A"
   thus "PROP ?P"
-  proof(induct A rule:finite_linorder_induct)
+  proof(induct A rule:finite_linorder_max_induct)
     case empty thus ?case by auto
   next
     case (insert A b)