# HG changeset patch # User nipkow # Date 1247663373 -7200 # Node ID 0e209ff7f236c919ba98b1a71b12695696e665c1 # Parent c369417be0552fbebb647b51d719e1d482a4ceec More finite set induction rules diff -r c369417be055 -r 0e209ff7f236 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Jul 15 12:44:41 2009 +0200 +++ b/src/HOL/Finite_Set.thy Wed Jul 15 15:09:33 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 \ ALL x:A. (EX y. P x y) \ EX f. ALL x:A. P x (f x)" @@ -2122,6 +2123,18 @@ \ x \ \ F = {}" by auto +lemma finite_psubset_induct[consumes 1, case_names psubset]: + assumes "finite A" and "!!A. finite A \ (!!B. finite B \ B \ A \ P(B)) \ 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 \ A" + show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \ 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 \ P {} \ (!!A b. finite A \ ALL a:A. a < b \ P A \ P(insert b A)) \ 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 \ finite B \ P {} \ + assume IH: "!! B. finite B \ B < A \ P {} \ (!!A b. finite A \ (\a\A. a P A \ P (insert b A)) \ P B" and "finite A" and "P {}" @@ -3271,16 +3284,17 @@ assume "A \ {}" 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 "\a\?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 "\a\?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]: + "\finite A; P {}; \A b. \finite A; \a\A. b < a; P A\ \ P (insert b A)\ \ P A" +by(rule linorder.finite_linorder_max_induct[OF dual_linorder]) + end context ordered_ab_semigroup_add diff -r c369417be055 -r 0e209ff7f236 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Wed Jul 15 12:44:41 2009 +0200 +++ b/src/HOL/SetInterval.thy Wed Jul 15 15:09:33 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)