# HG changeset patch # User Christian Urban # Date 1270631111 -7200 # Node ID fa0e354e6a39fd2bcdb5d4ca44a16263460b263c # Parent 59f6773a7d1d8700adb9dfd9fc078dee6d3c4588 simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle diff -r 59f6773a7d1d -r fa0e354e6a39 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Tue Apr 06 11:00:57 2010 +0200 +++ b/src/HOL/Big_Operators.thy Wed Apr 07 11:05:11 2010 +0200 @@ -1676,27 +1676,31 @@ qed lemma finite_linorder_max_induct[consumes 1, case_names empty insert]: - "finite A \ P {} \ - (!!b A. finite A \ ALL a:A. a < b \ P A \ P(insert b A)) - \ P A" + assumes fin: "finite A" + and empty: "P {}" + and insert: "(!!b A. finite A \ ALL a:A. a < b \ P A \ P(insert b A))" + shows "P A" +using fin empty insert proof (induct rule: finite_psubset_induct) - fix A :: "'a set" - assume IH: "!! B. finite B \ B < A \ P {} \ - (!!b A. finite A \ (\a\A. a P A \ P (insert b A)) - \ P B" - and "finite A" and "P {}" - and step: "!!b A. \finite A; \a\A. a < b; P A\ \ P (insert b A)" + case (psubset A) + have IH: "\B. \B < A; P {}; (\A b. \finite A; \a\A. a \ P (insert b A))\ \ P B" by fact + have fin: "finite A" by fact + have empty: "P {}" by fact + have step: "\b A. \finite A; \a\A. a < b; P A\ \ P (insert b A)" by fact show "P A" proof (cases "A = {}") - assume "A = {}" thus "P A" using `P {}` by simp + assume "A = {}" + then show "P A" using `P {}` by simp next - let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B" + let ?B = "A - {Max A}" + let ?A = "insert (Max A) ?B" + have "finite ?B" using `finite A` by simp assume "A \ {}" 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[of ?B] by blast - moreover have "\a\?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp + then have A: "?A = A" using insert_Diff_single insert_absorb by auto + then have "P ?B" using `P {}` step IH[of ?B] 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 qed qed diff -r 59f6773a7d1d -r fa0e354e6a39 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Apr 06 11:00:57 2010 +0200 +++ b/src/HOL/Finite_Set.thy Wed Apr 07 11:05:11 2010 +0200 @@ -2045,15 +2045,24 @@ 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]) + assumes fin: "finite A" + and major: "\A. finite A \ (\B. B \ A \ P B) \ P A" + shows "P A" +using fin +proof (induct A taking: card rule: measure_induct_rule) 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 + have fin: "finite A" by fact + have ih: "\B. \card B < card A; finite B\ \ P B" by fact + { fix B + assume asm: "B \ A" + from asm have "card B < card A" using psubset_card_mono fin by blast + moreover + from asm have "B \ A" by auto + then have "finite B" using fin finite_subset by blast + ultimately + have "P B" using ih by simp + } + with fin show "P A" using major by blast qed text{* main cardinality theorem *}