# HG changeset patch
# User nipkow
# Date 1257326263 -3600
# Node ID e9de8d69c1b9f6b5ea7ec9e22bea7e09e9e35d41
# Parent  a9a002f4b71551b0510002f1b51fe112648fe516
fixed order of parameters in induction rules

diff -r a9a002f4b715 -r e9de8d69c1b9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Nov 04 09:18:46 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Nov 04 10:17:43 2009 +0100
@@ -3261,15 +3261,15 @@
 
 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))
+  (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
   \<Longrightarrow> P A"
 proof (induct rule: finite_psubset_induct)
   fix A :: "'a set"
   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))
+                 (!!b A. 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 {}"
-  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
+  and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
   show "P A"
   proof (cases "A = {}")
     assume "A = {}" thus "P A" using `P {}` by simp
@@ -3279,14 +3279,14 @@
     with `finite A` have "Max A : A" by auto
     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
     moreover have "finite ?B" using `finite A` by simp
-    ultimately have "P ?B" using `P {}` step IH by blast
+    ultimately have "P ?B" using `P {}` step IH[of ?B] 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
   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"
+ "\<lbrakk>finite A; P {}; \<And>b A. \<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
diff -r a9a002f4b715 -r e9de8d69c1b9 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Nov 04 09:18:46 2009 +0100
+++ b/src/HOL/SetInterval.thy	Wed Nov 04 10:17:43 2009 +0100
@@ -508,7 +508,7 @@
   proof(induct A rule:finite_linorder_max_induct)
     case empty thus ?case by auto
   next
-    case (insert A b)
+    case (insert b A)
     moreover hence "b ~: A" by auto
     moreover have "A <= {k..<k+card A}" and "b = k+card A"
       using `b ~: A` insert by fastsimp+