fixed order of parameters in induction rules
authornipkow
Wed Nov 04 10:17:43 2009 +0100 (2009-11-04)
changeset 33434e9de8d69c1b9
parent 33432 a9a002f4b715
child 33435 6f825ec18b49
fixed order of parameters in induction rules
src/HOL/Finite_Set.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Nov 04 09:18:46 2009 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Nov 04 10:17:43 2009 +0100
     1.3 @@ -3261,15 +3261,15 @@
     1.4  
     1.5  lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
     1.6   "finite A \<Longrightarrow> P {} \<Longrightarrow>
     1.7 -  (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
     1.8 +  (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
     1.9    \<Longrightarrow> P A"
    1.10  proof (induct rule: finite_psubset_induct)
    1.11    fix A :: "'a set"
    1.12    assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
    1.13 -                 (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
    1.14 +                 (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
    1.15                    \<Longrightarrow> P B"
    1.16    and "finite A" and "P {}"
    1.17 -  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
    1.18 +  and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
    1.19    show "P A"
    1.20    proof (cases "A = {}")
    1.21      assume "A = {}" thus "P A" using `P {}` by simp
    1.22 @@ -3279,14 +3279,14 @@
    1.23      with `finite A` have "Max A : A" by auto
    1.24      hence A: "?A = A" using insert_Diff_single insert_absorb by auto
    1.25      moreover have "finite ?B" using `finite A` by simp
    1.26 -    ultimately have "P ?B" using `P {}` step IH by blast
    1.27 +    ultimately have "P ?B" using `P {}` step IH[of ?B] by blast
    1.28      moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
    1.29      ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
    1.30    qed
    1.31  qed
    1.32  
    1.33  lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
    1.34 -  "\<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"
    1.35 + "\<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"
    1.36  by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
    1.37  
    1.38  end
     2.1 --- a/src/HOL/SetInterval.thy	Wed Nov 04 09:18:46 2009 +0100
     2.2 +++ b/src/HOL/SetInterval.thy	Wed Nov 04 10:17:43 2009 +0100
     2.3 @@ -508,7 +508,7 @@
     2.4    proof(induct A rule:finite_linorder_max_induct)
     2.5      case empty thus ?case by auto
     2.6    next
     2.7 -    case (insert A b)
     2.8 +    case (insert b A)
     2.9      moreover hence "b ~: A" by auto
    2.10      moreover have "A <= {k..<k+card A}" and "b = k+card A"
    2.11        using `b ~: A` insert by fastsimp+