More finite set induction rules
authornipkow
Wed Jul 15 15:09:33 2009 +0200 (2009-07-15)
changeset 320060e209ff7f236
parent 32005 c369417be055
child 32007 a2a3685f61c3
child 32044 64a12f353c57
child 32076 05d915945bc6
More finite set induction rules
src/HOL/Finite_Set.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Jul 15 12:44:41 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Jul 15 15:09:33 2009 +0200
     1.3 @@ -93,6 +93,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +
     1.8  text{* A finite choice principle. Does not need the SOME choice operator. *}
     1.9  lemma finite_set_choice:
    1.10    "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
    1.11 @@ -2122,6 +2123,18 @@
    1.12    \<Longrightarrow> x \<inter> \<Union> F = {}"
    1.13  by auto
    1.14  
    1.15 +lemma finite_psubset_induct[consumes 1, case_names psubset]:
    1.16 +  assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
    1.17 +using assms(1)
    1.18 +proof (induct A rule: measure_induct_rule[where f=card])
    1.19 +  case (less A)
    1.20 +  show ?case
    1.21 +  proof(rule assms(2)[OF less(2)])
    1.22 +    fix B assume "finite B" "B \<subset> A"
    1.23 +    show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
    1.24 +  qed
    1.25 +qed
    1.26 +
    1.27  text{* main cardinality theorem *}
    1.28  lemma card_partition [rule_format]:
    1.29    "finite C ==>
    1.30 @@ -3252,13 +3265,13 @@
    1.31      by (simp add: Max fold1_antimono [folded dual_max])
    1.32  qed
    1.33  
    1.34 -lemma finite_linorder_induct[consumes 1, case_names empty insert]:
    1.35 +lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
    1.36   "finite A \<Longrightarrow> P {} \<Longrightarrow>
    1.37    (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
    1.38    \<Longrightarrow> P A"
    1.39 -proof (induct A rule: measure_induct_rule[where f=card])
    1.40 +proof (induct rule: finite_psubset_induct)
    1.41    fix A :: "'a set"
    1.42 -  assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
    1.43 +  assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
    1.44                   (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
    1.45                    \<Longrightarrow> P B"
    1.46    and "finite A" and "P {}"
    1.47 @@ -3271,16 +3284,17 @@
    1.48      assume "A \<noteq> {}"
    1.49      with `finite A` have "Max A : A" by auto
    1.50      hence A: "?A = A" using insert_Diff_single insert_absorb by auto
    1.51 -    note card_Diff1_less[OF `finite A` `Max A : A`]
    1.52      moreover have "finite ?B" using `finite A` by simp
    1.53      ultimately have "P ?B" using `P {}` step IH by blast
    1.54 -    moreover have "\<forall>a\<in>?B. a < Max A"
    1.55 -      using Max_ge [OF `finite A`] by fastsimp
    1.56 -    ultimately show "P A"
    1.57 -      using A insert_Diff_single step[OF `finite ?B`] by fastsimp
    1.58 +    moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
    1.59 +    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
    1.60    qed
    1.61  qed
    1.62  
    1.63 +lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
    1.64 +  "\<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.65 +by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
    1.66 +
    1.67  end
    1.68  
    1.69  context ordered_ab_semigroup_add
     2.1 --- a/src/HOL/SetInterval.thy	Wed Jul 15 12:44:41 2009 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Wed Jul 15 15:09:33 2009 +0200
     2.3 @@ -425,7 +425,7 @@
     2.4  proof cases
     2.5    assume "finite A"
     2.6    thus "PROP ?P"
     2.7 -  proof(induct A rule:finite_linorder_induct)
     2.8 +  proof(induct A rule:finite_linorder_max_induct)
     2.9      case empty thus ?case by auto
    2.10    next
    2.11      case (insert A b)