--- a/src/HOL/ROOT Wed Jun 17 18:44:23 2015 +0200
+++ b/src/HOL/ROOT Fri Jun 12 10:33:02 2015 +0200
@@ -594,6 +594,9 @@
SAT_Examples
SOS
SOS_Cert
+ Ballot
+ Erdoes_Szekeres
+ Sum_of_Powers
theories [skip_proofs = false]
Meson_Test
theories [condition = ISABELLE_FULL_TEST]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Ballot.thy Fri Jun 12 10:33:02 2015 +0200
@@ -0,0 +1,593 @@
+(* Title: HOL/ex/Ballot.thy
+ Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
+*)
+
+section {* Bertrand's Ballot Theorem *}
+
+theory Ballot
+imports
+ Complex_Main
+ "~~/src/HOL/Library/FuncSet"
+begin
+
+subsection {* Preliminaries *}
+
+subsubsection {* Dedicated Simplification Setup *}
+
+declare One_nat_def[simp del]
+declare add_2_eq_Suc'[simp del]
+declare atLeastAtMost_iff[simp del]
+declare fun_upd_apply[simp del]
+
+lemma [simp]: "1 \<le> n \<Longrightarrow> n : {1..(n :: nat)}"
+by (auto simp add: atLeastAtMost_iff)
+
+lemma [simp]: "(n :: nat) + 2 \<notin> {1..n + 1}"
+by (auto simp add: atLeastAtMost_iff)
+
+subsubsection {* Additions to @{theory Set} Theory *}
+
+lemma ex1_iff_singleton: "(EX! x. x : S) \<longleftrightarrow> (EX x. S = {x})"
+proof
+ assume "EX! x. x : S"
+ from this show "EX x. S = {x}"
+ by (metis Un_empty_left Un_insert_left insertI1 insert_absorb subsetI subset_antisym)
+next
+ assume "EX x. S = {x}"
+ thus "EX! x. x : S" by (metis (full_types) singleton_iff)
+qed
+
+subsubsection {* Additions to @{theory Finite_Set} Theory *}
+
+lemma card_singleton[simp]: "card {x} = 1"
+ by simp
+
+lemma finite_bij_subset_implies_equal_sets:
+ assumes "finite T" "\<exists>f. bij_betw f S T" "S <= T"
+ shows "S = T"
+using assms by (metis (lifting) bij_betw_def bij_betw_inv endo_inj_surj)
+
+lemma singleton_iff_card_one: "(EX x. S = {x}) \<longleftrightarrow> card S = 1"
+proof
+ assume "EX x. S = {x}"
+ then show "card S = 1" by auto
+next
+ assume c: "card S = 1"
+ from this have s: "S \<noteq> {}" by (metis card_empty zero_neq_one)
+ from this obtain a where a: "a \<in> S" by auto
+ from this s obtain T where S: "S = insert a T" and a: "a \<notin> T"
+ by (metis Set.set_insert)
+ from c S a have "card T = 0"
+ by (metis One_nat_def card_infinite card_insert_disjoint old.nat.inject)
+ from this c S have "T = {}" by (metis (full_types) card_eq_0_iff finite_insert zero_neq_one)
+ from this S show "EX x. S = {x}" by auto
+qed
+
+subsubsection {* Additions to @{theory Nat} Theory *}
+
+lemma square_diff_square_factored_nat:
+ shows "(x::nat) * x - y * y = (x + y) * (x - y)"
+proof (cases "(x::nat) \<ge> y")
+ case True
+ from this show ?thesis by (simp add: algebra_simps diff_mult_distrib2)
+next
+ case False
+ from this show ?thesis by (auto intro: mult_le_mono)
+qed
+
+subsubsection {* Additions to @{theory FuncSet} Theory *}
+
+lemma extensional_constant_function_is_unique:
+ assumes c: "c : T"
+ shows "EX! f. f : S \<rightarrow>\<^sub>E T & (\<forall>x \<in> S. f x = c)"
+proof
+ def f == "(%x. if x \<in> S then c else undefined)"
+ from c show "f : S \<rightarrow>\<^sub>E T & (\<forall>x \<in> S. f x = c)" unfolding f_def by auto
+next
+ fix f
+ assume "f : S \<rightarrow>\<^sub>E T & (\<forall>x \<in> S. f x = c)"
+ from this show "f = (%x. if x \<in> S then c else undefined)" by (metis PiE_E)
+qed
+
+lemma PiE_insert_restricted_eq:
+ assumes a: "x \<notin> S"
+ shows "{f : insert x S \<rightarrow>\<^sub>E T. P f} = (\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
+proof -
+ {
+ fix f
+ assume "f : {f : insert x S \<rightarrow>\<^sub>E T. P f}"
+ from this a have "f :(\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
+ by (auto intro!: image_eqI[where x="(f x, f(x:=undefined))"])
+ (metis PiE_E fun_upd_other insertCI, metis (full_types) PiE_E fun_upd_in_PiE)
+ } moreover
+ {
+ fix f
+ assume "f :(\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
+ from this have "f : {f : insert x S \<rightarrow>\<^sub>E T. P f}"
+ by (auto elim!: PiE_fun_upd split: prod.split)
+ }
+ ultimately show ?thesis
+ by (intro set_eqI iffI) assumption+
+qed
+
+lemma card_extensional_funcset_insert:
+ assumes "x \<notin> S" "finite S" "finite T"
+ shows "card {f : insert x S \<rightarrow>\<^sub>E T. P f} = (\<Sum>y\<in>T. card {f : S \<rightarrow>\<^sub>E T. P (f(x:=y))})"
+proof -
+ from `finite S` `finite T` have finite_funcset: "finite (S \<rightarrow>\<^sub>E T)" by (rule finite_PiE)
+ have finite: "\<forall>y\<in>T. finite {f : S \<rightarrow>\<^sub>E T. P (f(x:=y))}"
+ by (auto intro: finite_subset[OF _ finite_funcset])
+ from `x \<notin> S`have inj: "inj_on (%(y, g). g(x:=y)) (UNIV \<times> (S \<rightarrow>\<^sub>E T))"
+ unfolding inj_on_def
+ by auto (metis fun_upd_same, metis PiE_E fun_upd_idem_iff fun_upd_upd fun_upd_same)
+ from `x \<notin> S` have "card {f : insert x S \<rightarrow>\<^sub>E T. P f} =
+ card ((\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))}))"
+ by (subst PiE_insert_restricted_eq) auto
+ also from subset_inj_on[OF inj, of "SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))}"]
+ have "\<dots> = card (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})" by (subst card_image) auto
+ also from `finite T` finite have "\<dots> = (\<Sum>y\<in>T. card {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
+ by (simp only: card_SigmaI)
+ finally show ?thesis .
+qed
+
+subsubsection {* Additions to @{theory Binomial} Theory *}
+
+lemma Suc_times_binomial_add:
+ "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
+proof -
+ have minus: "Suc (a + b) - a = Suc b" "Suc (a + b) - (Suc a) = b" by auto
+ from fact_fact_dvd_fact[of "Suc a" "b"] have "fact (Suc a) * fact b dvd (fact (Suc a + b) :: nat)"
+ by fast
+ from this have dvd1: "Suc a * fact a * fact b dvd fact (Suc (a + b))"
+ by (simp only: fact_Suc add_Suc[symmetric] of_nat_id)
+ have dvd2: "fact a * (Suc b * fact b) dvd fact (Suc (a + b))"
+ by (metis add_Suc_right fact_Suc fact_fact_dvd_fact of_nat_id)
+ have "Suc a * (Suc (a + b) choose Suc a) = Suc a * (fact (Suc (a + b)) div (fact (Suc a) * fact b))"
+ by (simp only: binomial_altdef_nat minus(2))
+ also have "... = Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))"
+ unfolding fact_Suc[of a] div_mult_swap[OF dvd1] of_nat_id by (simp only: algebra_simps)
+ also have "... = Suc b * fact (Suc (a + b)) div (Suc b * (fact a * fact b))"
+ by (simp only: div_mult_mult1)
+ also have "... = Suc b * (fact (Suc (a + b)) div (fact a * fact (Suc b)))"
+ unfolding fact_Suc[of b] div_mult_swap[OF dvd2] of_nat_id by (simp only: algebra_simps)
+ also have "... = Suc b * (Suc (a + b) choose a)"
+ by (simp only: binomial_altdef_nat minus(1))
+ finally show ?thesis .
+qed
+
+subsection {* Formalization of Problem Statement *}
+
+subsubsection {* Basic Definitions *}
+
+datatype vote = A | B
+
+definition
+ "all_countings a b = card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a
+ & card {x : {1 .. a + b}. f x = B} = b}"
+
+definition
+ "valid_countings a b =
+ card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a
+ & card {x : {1 .. a + b}. f x = B} = b
+ & (\<forall>m \<in> {1 .. a + b }. card {x \<in> {1..m}. f x = A} > card {x \<in> {1..m}. f x = B})}"
+
+subsubsection {* Equivalence of Alternative Definitions *}
+
+lemma definition_rewrite_generic:
+ assumes "case vote of A \<Rightarrow> count = a | B \<Rightarrow> count = b"
+ shows "{f \<in> {1..a + b} \<rightarrow>\<^sub>E {A, B}. card {x \<in> {1..a + b}. f x = A} = a \<and> card {x \<in> {1..a + b}. f x = B} = b \<and> P f}
+ = {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = vote} = count \<and> P f}"
+proof -
+ let ?other_vote = "case vote of A \<Rightarrow> B | B \<Rightarrow> A"
+ let ?other_count = "case vote of A \<Rightarrow> b | B \<Rightarrow> a"
+ {
+ fix f
+ assume "card {x : {1 .. a + b}. f x = vote} = count"
+ from this have c: "card ({1 .. a + b} - {x : {1 .. a + b}. f x = vote}) = a + b - count"
+ by (subst card_Diff_subset) auto
+ have "{1 .. a + b} - {x : {1 .. a + b}. f x = vote} = {x : {1 .. a + b}. f x ~= vote}" by auto
+ from this c have not_A:" card {x : {1 .. a + b}. f x ~= vote} = a + b - count" by auto
+ have "!x. (f x ~= vote) = (f x = ?other_vote)"
+ by (cases vote, auto) (case_tac "f x", auto)+
+ from this not_A assms have "card {x : {1 .. a + b}. f x = ?other_vote} = ?other_count"
+ by auto (cases vote, auto)
+ }
+ from this have "{f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}.
+ card {x : {1 .. a + b}. f x = vote} = count & card {x : {1 .. a + b}. f x = ?other_vote} = ?other_count & P f} =
+ {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = vote} = count & P f}"
+ by auto
+ from this assms show ?thesis by (cases vote) auto
+qed
+
+lemma all_countings_def':
+ "all_countings a b = card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a}"
+unfolding all_countings_def definition_rewrite_generic[of a a _ A "\<lambda>_. True", simplified] ..
+
+lemma all_countings_def'':
+ "all_countings a b = card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = B} = b}"
+unfolding all_countings_def definition_rewrite_generic[of b _ b B "\<lambda>_. True", simplified] ..
+
+lemma valid_countings_def':
+ "valid_countings a b =
+ card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a
+ & (\<forall>m \<in> {1 .. a + b }. card {x \<in> {1..m}. f x = A} > card {x \<in> {1..m}. f x = B})}"
+unfolding valid_countings_def definition_rewrite_generic[of a a _ A, simplified] ..
+
+subsubsection {* Cardinality of Sets of Functions *}
+
+lemma one_extensional_constant_function:
+ assumes "c : T"
+ shows "card {f : S \<rightarrow>\<^sub>E T. (\<forall>x \<in> S. f x = c)} = 1"
+using assms
+ by (auto simp only: singleton_iff_card_one[symmetric] ex1_iff_singleton[symmetric] mem_Collect_eq
+ elim!: extensional_constant_function_is_unique)
+
+lemma card_filtered_set_eq_card_set_implies_forall:
+ assumes f: "finite S"
+ assumes c: "card {x : S. P x} = card S"
+ shows "\<forall>x \<in> S. P x"
+proof -
+ from f c have "\<exists>f. bij_betw f {x : S. P x} S"
+ by (metis Collect_mem_eq finite_Collect_conjI finite_same_card_bij)
+ from f this have eq: "{x : S. P x} = S"
+ by (metis (mono_tags) finite_bij_subset_implies_equal_sets Collect_mem_eq Collect_mono)
+ from this show ?thesis by auto
+qed
+
+lemma card_filtered_set_from_n_eq_n_implies_forall:
+ shows "(card {x : {1..n}. P x} = n) = (\<forall>x \<in> {1..n}. P x)"
+proof
+ assume "card {x : {1..n}. P x} = n"
+ from this show "\<forall>x \<in> {1..n}. P x"
+ by (metis card_atLeastAtMost card_filtered_set_eq_card_set_implies_forall
+ diff_Suc_1 finite_atLeastAtMost)
+next
+ assume "\<forall>x \<in> {1..n}. P x"
+ from this have "{x : {1..n}. P x} = {1..n}" by auto
+ from this show "card {x : {1..n}. P x} = n" by simp
+qed
+
+subsubsection {* Cardinality of the Inverse Image of an Updated Function *}
+
+lemma fun_upd_not_in_Domain:
+ assumes "x' \<notin> S"
+ shows "card {x : S. (f(x' := y)) x = c} = card {x : S. f x = c}"
+using assms by (auto simp add: fun_upd_apply) metis
+
+lemma card_fun_upd_noteq_constant:
+ assumes "x' \<notin> S" "c \<noteq> d"
+ shows "card {x : insert x' S. (f(x' := d)) x = c} = card {x : S. f x = c}"
+using assms by (auto simp add: fun_upd_apply) metis
+
+lemma card_fun_upd_eq_constant:
+ assumes "x' \<notin> S" "finite S"
+ shows "card {x : insert x' S. (f(x' := c)) x = c} = card {x : S. f x = c} + 1"
+proof -
+ from `x' \<notin> S` have "{x : insert x' S. (f(x' := c)) x = c} = insert x' {x \<in> S. f x = c}"
+ by (auto simp add: fun_upd_same fun_upd_other fun_upd_apply)
+ from `x' \<notin> S` `finite S` this show ?thesis by force
+qed
+
+subsubsection {* Relevant Specializations *}
+
+lemma atLeastAtMost_plus2_conv: "{1..(n :: nat) + 2} = insert (n + 2) {1..n + 1}"
+by (auto simp add: atLeastAtMost_iff)
+
+lemma card_fun_upd_noteq_constant_plus2:
+ assumes "v' \<noteq> v"
+ shows "card {x\<in>{1..(a :: nat) + b + 2}. (f(a + b + 2 := v')) x = v} =
+ card {x \<in> {1..a + b + 1}. f x = v}"
+using assms unfolding atLeastAtMost_plus2_conv by (subst card_fun_upd_noteq_constant) auto
+
+lemma card_fun_upd_eq_constant_plus2:
+ shows "card {x\<in>{1..(a :: nat) + b + 2}. (f(a + b + 2 := v)) x = v} = card {x\<in>{1..a + b + 1}. f x = v} + 1"
+unfolding atLeastAtMost_plus2_conv by (subst card_fun_upd_eq_constant) auto
+
+lemmas card_fun_upd_simps = card_fun_upd_noteq_constant_plus2 card_fun_upd_eq_constant_plus2
+
+lemma split_into_sum:
+ "card {f : {1 .. (n :: nat) + 2} \<rightarrow>\<^sub>E {A, B}. P f} =
+ card {f : {1 .. n + 1} \<rightarrow>\<^sub>E {A, B}. P (f(n + 2 := A))} +
+ card {f : {1 .. n + 1} \<rightarrow>\<^sub>E {A, B}. P (f(n + 2 := B))}"
+by (auto simp add: atLeastAtMost_plus2_conv card_extensional_funcset_insert)
+
+subsection {* Facts About @{term all_countings} *}
+
+subsubsection {* Simple Non-Recursive Cases *}
+
+lemma all_countings_a_0:
+ "all_countings a 0 = 1"
+unfolding all_countings_def'
+by (simp add: card_filtered_set_from_n_eq_n_implies_forall one_extensional_constant_function)
+
+lemma all_countings_0_b:
+ "all_countings 0 b = 1"
+unfolding all_countings_def''
+by (simp add: card_filtered_set_from_n_eq_n_implies_forall one_extensional_constant_function)
+
+subsubsection {* Recursive Case *}
+
+lemma all_countings_Suc_Suc:
+ "all_countings (a + 1) (b + 1) = all_countings a (b + 1) + all_countings (a + 1) b"
+proof -
+ let ?intermed = "%y. card {f : {1..a + b + 1} \<rightarrow>\<^sub>E {A, B}. card {x : {1..a + b + 2}.
+ (f(a + b + 2 := y)) x = A} = a + 1 \<and> card {x : {1..a + b + 2}. (f(a + b + 2 := y)) x = B} = b + 1}"
+ have "all_countings (a + 1) (b + 1) = card {f : {1..a + b + 2} \<rightarrow>\<^sub>E {A, B}.
+ card {x : {1..a + b + 2}. f x = A} = a + 1 \<and> card {x : {1..a + b + 2}. f x = B} = b + 1}"
+ unfolding all_countings_def[of "a+1" "b+1"] by (simp add: algebra_simps One_nat_def add_2_eq_Suc')
+ also have "\<dots> = ?intermed A + ?intermed B" unfolding split_into_sum ..
+ also have "\<dots> = all_countings a (b + 1) + all_countings (a + 1) b"
+ by (simp add: card_fun_upd_simps all_countings_def) (simp add: algebra_simps)
+ finally show ?thesis .
+qed
+
+subsubsection {* Executable Definition *}
+
+declare all_countings_def [code del]
+declare all_countings_a_0 [code]
+declare all_countings_0_b [code]
+declare all_countings_Suc_Suc [unfolded One_nat_def, simplified, code]
+
+value "all_countings 1 0"
+value "all_countings 0 1"
+value "all_countings 1 1"
+value "all_countings 2 1"
+value "all_countings 1 2"
+value "all_countings 2 4"
+value "all_countings 4 2"
+
+subsubsection {* Relation to Binomial Function *}
+
+lemma all_countings:
+ "all_countings a b = (a + b) choose a"
+proof (induct a arbitrary: b)
+ case 0
+ show ?case by (simp add: all_countings_0_b)
+next
+ case (Suc a)
+ note Suc_hyps = Suc.hyps
+ show ?case
+ proof (induct b)
+ case 0
+ show ?case by (simp add: all_countings_a_0)
+ next
+ case (Suc b)
+ from Suc_hyps Suc.hyps show ?case
+ by (metis Suc_eq_plus1 Suc_funpow add_Suc_shift binomial_Suc_Suc funpow_swap1
+ all_countings_Suc_Suc)
+ qed
+qed
+
+subsection {* Facts About @{term valid_countings} *}
+
+subsubsection {* Non-Recursive Cases *}
+
+lemma valid_countings_a_0:
+ "valid_countings a 0 = 1"
+proof -
+ {
+ fix f
+ {
+ assume "card {x : {1..a}. f x = A} = a"
+ from this have a: "\<forall>x \<in> {1..a}. f x = A"
+ by (intro card_filtered_set_eq_card_set_implies_forall) auto
+ {
+ fix i m
+ assume e: "1 <= i" "i <= m" "m <= a"
+ from a e have "{x : {1..m}. f x = A} = {1 .. m}" by (auto simp add: atLeastAtMost_iff)
+ from this have "card {x : {1..m}. f x = A} = m" by auto
+ from a e this have "card {x : {1..m}. f x = A} = m \<and> card {x : {1..m}. f x = B} = 0"
+ by (auto simp add: atLeastAtMost_iff)
+ }
+ from this have "(\<forall>m \<in> {1..a}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A}) = True"
+ by (auto simp del: card_0_eq simp add: atLeastAtMost_iff)
+ }
+ from this have "((card {x : {1..a}. f x = A} = a) &
+ (\<forall>m \<in> {1..a}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A})) =
+ (card {x : {1..a}. f x = A} = a)" by blast
+ } note redundant_disjunct = this
+ show ?thesis
+ unfolding valid_countings_def'
+ by (auto simp add: redundant_disjunct all_countings_a_0[unfolded all_countings_def', simplified])
+qed
+
+lemma valid_countings_eq_zero:
+ assumes "a \<le> b" "0 < b"
+ shows "valid_countings a b = 0"
+proof -
+ from assms have is_empty: "{f \<in> {1..a + b} \<rightarrow>\<^sub>E {A, B}.
+ card {x \<in> {1..a + b}. f x = A} = a \<and>
+ card {x \<in> {1..a + b}. f x = B} = b \<and>
+ (\<forall>m \<in> {1..a + b}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A})} = {}"
+ by auto (intro bexI[of _ "a + b"], auto)
+ show ?thesis
+ unfolding valid_countings_def by (metis card_empty is_empty)
+qed
+
+subsubsection {* Recursive Cases *}
+
+lemma valid_countings_Suc_Suc_recursive:
+ assumes "b < a"
+ shows "valid_countings (a + 1) (b + 1) = valid_countings a (b + 1) + valid_countings (a + 1) b"
+proof -
+ let ?intermed = "%y. card {f : {1..a + b + 1} \<rightarrow>\<^sub>E {A, B}. card {x : {1..a + b + 2}.
+ (f(a + b + 2 := y)) x = A} = a + 1 \<and> card {x : {1..a + b + 2}. (f(a + b + 2 := y)) x = B} = b + 1
+ \<and> (\<forall>m \<in> {1..a + b + 2}. card {x : {1..m}. (f(a + b + 2 := y)) x = B} < card {x : {1 .. m}. (f(a + b + 2 := y)) x = A})}"
+ {
+ fix f
+ let ?a = "%c. card {x \<in> {1.. a + b + 1}. f x = A} = c"
+ let ?b = "%c. card {x \<in> {1.. a + b + 1}. f x = B} = c"
+ let ?c = "%c. (\<forall>m\<in>{1.. a + b + 2}. card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B}
+ < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A})"
+ let ?d = "(\<forall>m\<in>{1.. a + b + 1}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A})"
+ {
+ fix c
+ have "(\<forall>m\<in>{1.. a + b + 1}. card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B}
+ < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}) = ?d"
+ proof (rule iffI, auto)
+ fix m
+ assume 1: "\<forall>m\<in>{1..a + b + 1}.
+ card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B} < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}"
+ assume 2: "m \<in> {1..a + b + 1}"
+ from 2 have 3: "a + b + 2 \<notin> {1..m}" by (simp add: atLeastAtMost_iff)
+ from 1 2 have "card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B} < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}"
+ by auto
+ from this show "card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A}"
+ by (simp add: fun_upd_not_in_Domain[OF 3])
+ next
+ fix m
+ assume 1: "\<forall>m\<in>{1..a + b + 1}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A}"
+ assume 2: "m \<in> {1..a + b + 1}"
+ from 2 have 3: "a + b + 2 \<notin> {1..m}" by (simp add: atLeastAtMost_iff)
+ from 1 2 have "card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A}" by auto
+ from this show
+ "card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B} < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}"
+ by (simp add: fun_upd_not_in_Domain[OF 3])
+ qed
+ } note common = this
+ {
+ assume cardinalities: "?a a" "?b (b + 1)"
+ have "?c A = ?d"
+ unfolding atLeastAtMost_plus2_conv
+ by (simp add: cardinalities card_fun_upd_simps `b < a` common)
+ } moreover
+ {
+ assume cardinalities: "?a (a + 1)" "?b b"
+ have "?c B = ?d"
+ unfolding atLeastAtMost_plus2_conv
+ by (simp add: cardinalities card_fun_upd_simps `b < a` common)
+ }
+ ultimately have "(?a a & ?b (b + 1) & ?c A) = (?a a & ?b (b + 1) & ?d)"
+ "(?a (a + 1) & ?b b & ?c B) = (?a (a + 1) & ?b b & ?d)" by blast+
+ } note eq_inner = this
+ have "valid_countings (a + 1) (b + 1) = card {f : {1..a + b + 2} \<rightarrow>\<^sub>E {A, B}.
+ card {x : {1..a + b + 2}. f x = A} = a + 1 \<and> card {x : {1..a + b + 2}. f x = B} = b + 1 \<and>
+ (\<forall>m \<in> {1..a + b + 2}. card {x : {1..m}. f x = B} < card {x : {1..m}. f x = A})}"
+ unfolding valid_countings_def[of "a + 1" "b + 1"]
+ by (simp add: algebra_simps One_nat_def add_2_eq_Suc')
+ also have "\<dots> = ?intermed A + ?intermed B" unfolding split_into_sum ..
+ also have "\<dots> = valid_countings a (b + 1) + valid_countings (a + 1) b"
+ by (simp add: card_fun_upd_simps eq_inner valid_countings_def) (simp add: algebra_simps)
+ finally show ?thesis .
+qed
+
+lemma valid_countings_Suc_Suc:
+ "valid_countings (a + 1) (b + 1) =
+ (if a \<le> b then 0 else valid_countings a (b + 1) + valid_countings (a + 1) b)"
+by (auto simp add: valid_countings_eq_zero valid_countings_Suc_Suc_recursive)
+
+lemma valid_countings_0_Suc: "valid_countings 0 (Suc b) = 0"
+by (simp add: valid_countings_eq_zero)
+
+subsubsection {* Executable Definition *}
+
+declare valid_countings_def [code del]
+declare valid_countings_a_0 [code]
+declare valid_countings_0_Suc [code]
+declare valid_countings_Suc_Suc [unfolded One_nat_def, simplified, code]
+
+value "valid_countings 1 0"
+value "valid_countings 0 1"
+value "valid_countings 1 1"
+value "valid_countings 2 1"
+value "valid_countings 1 2"
+value "valid_countings 2 4"
+value "valid_countings 4 2"
+
+subsubsection {* Relation to Binomial Function *}
+
+lemma valid_countings:
+ "(a + b) * valid_countings a b = (a - b) * ((a + b) choose a)"
+proof (induct a arbitrary: b rule: nat.induct[unfolded Suc_eq_plus1])
+ case 1
+ have "b = 0 | (EX b'. b = b' + 1)" by (cases b) simp+
+ from this show ?case
+ by (auto simp : valid_countings_eq_zero valid_countings_a_0)
+next
+ case (2 a)
+ note a_hyp = "2.hyps"
+ show ?case
+ proof (induct b rule: nat.induct[unfolded Suc_eq_plus1])
+ case 1
+ show ?case by (simp add: valid_countings_a_0)
+ next
+ case (2 b)
+ note b_hyp = "2.hyps"
+ show ?case
+ proof(cases "a <= b")
+ case True
+ from this show ?thesis
+ unfolding valid_countings_Suc_Suc if_True by (simp add: algebra_simps)
+ next
+ case False
+ from this have "b < a" by simp
+ have makes_plus_2: "a + 1 + (b + 1) = a + b + 2"
+ by (metis Suc_eq_plus1 add_Suc add_Suc_right one_add_one)
+ from b_hyp have b_hyp: "(a + b + 1) * valid_countings (a + 1) b = (a + 1 - b) * (a + b + 1 choose (a + 1))"
+ by (simp add: algebra_simps)
+ from a_hyp[of "b + 1"] have a_hyp: "(a + b + 1) * valid_countings a (b + 1) = (a - (b + 1)) * (a + (b + 1) choose a)"
+ by (simp add: algebra_simps)
+ have "a - b \<le> a * a - b * b" by (simp add: square_diff_square_factored_nat)
+ from this `b < a` have "a + b * b \<le> b + a * a" by auto
+ moreover from `\<not> a \<le> b` have "b * b \<le> a + a * b" by (meson linear mult_le_mono1 trans_le_add2)
+ moreover have "1 + b + a * b \<le> a * a"
+ proof -
+ from `b < a` have "1 + b + a * b \<le> a + a * b" by simp
+ also have "\<dots> \<le> a * (b + 1)" by (simp add: algebra_simps)
+ also from `b < a` have "\<dots> \<le> a * a" by simp
+ finally show ?thesis .
+ qed
+ moreover note `b < a`
+ ultimately have rearrange: "(a + 1) * (a - (b + 1)) + (a + 1 - b) * (b + 1) = (a - b) * (a + b + 1)"
+ by (simp add: algebra_simps)
+ have rewrite1: "\<And>(A :: nat) B C D E F. A * B * ((C * D) + (E * F)) = A * ((C * (B * D)) + (E * (B * F)))"
+ by (simp add: algebra_simps)
+ have rewrite2: "\<And>(A :: nat) B C D E F. A * (B * (C * D) + E * (F * D)) = (C * B + E * F) * (A * D)"
+ by (simp only: algebra_simps)
+ have "(a + b + 2) * (a + 1) * (a + b + 1) * valid_countings (a + 1) (b + 1) =
+ (a + b + 2) * (a + 1) * ((a + b + 1) * valid_countings a (b + 1) + (a + b + 1) * valid_countings (a + 1) b)"
+ unfolding valid_countings_Suc_Suc_recursive[OF `b < a`] by (simp only: algebra_simps)
+ also have "... = (a + b + 2) * ((a - (b + 1)) * ((a + 1) * (a + b + 1 choose a)) + (a + 1 - b) * ((a + 1) * (a + b + 1 choose (a + 1))))"
+ unfolding b_hyp a_hyp rewrite1 by (simp only: add.assoc)
+ also have "... = ((a + 1) * (a - (b + 1)) + (a + 1 - b) * (b + 1)) * ((a + b + 2) * (a + 1 + b choose a))"
+ unfolding Suc_times_binomial_add[simplified Suc_eq_plus1] rewrite2 by (simp only: algebra_simps)
+ also have "... = (a - b) * (a + b + 1) * ((a + 1 + b + 1) * (a + 1 + b choose a))"
+ by (simp add: rearrange)
+ also have "... = (a - b) * (a + b + 1) * (((a + 1 + b + 1) choose (a + 1)) * (a + 1))"
+ by (subst Suc_times_binomial_eq[simplified Suc_eq_plus1, where k = "a" and n = "a + 1 + b"]) auto
+ also have "... = (a - b) * (a + 1) * (a + b + 1) * (a + 1 + (b + 1) choose (a + 1))"
+ by (auto simp add: add.assoc)
+ finally show ?thesis by (simp add: makes_plus_2)
+ qed
+ qed
+qed
+
+subsection {* Relation Between @{term valid_countings} and @{term all_countings} *}
+
+lemma main_nat: "(a + b) * valid_countings a b = (a - b) * all_countings a b"
+ unfolding valid_countings all_countings ..
+
+lemma main_real:
+ assumes "b < a"
+ shows "valid_countings a b = (a - b) / (a + b) * all_countings a b"
+using assms
+proof -
+ from main_nat[of a b] `b < a` have
+ "(real a + real b) * real (valid_countings a b) = (real a - real b) * real (all_countings a b)"
+ by (simp only: real_of_nat_add[symmetric] real_of_nat_mult[symmetric]) auto
+ from this `b < a` show ?thesis
+ by (subst mult_left_cancel[of "real a + real b", symmetric]) auto
+qed
+
+lemma
+ "valid_countings a b = (if a \<le> b then (if b = 0 then 1 else 0) else (a - b) / (a + b) * all_countings a b)"
+proof (cases "a \<le> b")
+ case False
+ from this show ?thesis by (simp add: main_real)
+next
+ case True
+ from this show ?thesis
+ by (auto simp add: valid_countings_a_0 all_countings_a_0 valid_countings_eq_zero)
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Erdoes_Szekeres.thy Fri Jun 12 10:33:02 2015 +0200
@@ -0,0 +1,164 @@
+(* Title: HOL/ex/Erdoes_Szekeres.thy
+ Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
+*)
+
+section {* The Erdoes-Szekeres Theorem *}
+
+theory Erdoes_Szekeres
+imports Main
+begin
+
+subsection {* Addition to @{theory Lattices_Big} Theory *}
+
+lemma Max_gr:
+ assumes "finite A"
+ assumes "a \<in> A" "a > x"
+ shows "x < Max A"
+using assms Max_ge less_le_trans by blast
+
+subsection {* Additions to @{theory Finite_Set} Theory *}
+
+lemma obtain_subset_with_card_n:
+ assumes "n \<le> card S"
+ obtains T where "T \<subseteq> S" "card T = n"
+proof -
+ from assms obtain n' where "card S = n + n'" by (metis le_add_diff_inverse)
+ from this that show ?thesis
+ proof (induct n' arbitrary: S)
+ case 0 from this show ?case by auto
+ next
+ case Suc from this show ?case by (simp add: card_Suc_eq) (metis subset_insertI2)
+ qed
+qed
+
+lemma exists_set_with_max_card:
+ assumes "finite S" "S \<noteq> {}"
+ shows "\<exists>s \<in> S. card s = Max (card ` S)"
+using assms
+proof (induct S rule: finite.induct)
+ case (insertI S' s')
+ show ?case
+ proof (cases "S' \<noteq> {}")
+ case True
+ from this insertI.hyps(2) obtain s where s: "s \<in> S'" "card s = Max (card ` S')" by auto
+ from this(1) have that: "(if card s \<ge> card s' then s else s') \<in> insert s' S'" by auto
+ have "card (if card s \<ge> card s' then s else s') = Max (card ` insert s' S')"
+ using insertI(1) `S' \<noteq> {}` s by auto
+ from this that show ?thesis by blast
+ qed (auto)
+qed (auto)
+
+subsection {* Definition of Monotonicity over a Carrier Set *}
+
+definition
+ "mono_on f R S = (\<forall>i\<in>S. \<forall>j\<in>S. i \<le> j \<longrightarrow> R (f i) (f j))"
+
+lemma mono_on_empty [simp]: "mono_on f R {}"
+unfolding mono_on_def by auto
+
+lemma mono_on_singleton [simp]: "reflp R \<Longrightarrow> mono_on f R {x}"
+unfolding mono_on_def reflp_def by auto
+
+lemma mono_on_subset: "T \<subseteq> S \<Longrightarrow> mono_on f R S \<Longrightarrow> mono_on f R T"
+unfolding mono_on_def by (simp add: subset_iff)
+
+lemma not_mono_on_subset: "T \<subseteq> S \<Longrightarrow> \<not> mono_on f R T \<Longrightarrow> \<not> mono_on f R S"
+unfolding mono_on_def by blast
+
+lemma [simp]:
+ "reflp (op \<le> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
+ "reflp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
+ "transp (op \<le> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
+ "transp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
+unfolding reflp_def transp_def by auto
+
+subsection {* The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument *}
+
+lemma Erdoes_Szekeres:
+ fixes f :: "_ \<Rightarrow> 'a::linorder"
+ shows "(\<exists>S. S \<subseteq> {0..m * n} \<and> card S = m + 1 \<and> mono_on f (op \<le>) S) \<or>
+ (\<exists>S. S \<subseteq> {0..m * n} \<and> card S = n + 1 \<and> mono_on f (op \<ge>) S)"
+proof (rule ccontr)
+ let ?max_subseq = "\<lambda>R k. Max (card ` {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S})"
+ def phi == "\<lambda>k. (?max_subseq (op \<le>) k, ?max_subseq (op \<ge>) k)"
+
+ have one_member: "\<And>R k. reflp R \<Longrightarrow> {k} \<in> {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S}" by auto
+
+ {
+ fix R
+ assume reflp: "reflp (R :: 'a::linorder \<Rightarrow> _)"
+ from one_member[OF this] have non_empty: "\<And>k. {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S} \<noteq> {}" by force
+ from one_member[OF reflp] have "\<And>k. card {k} \<in> card ` {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S}" by blast
+ from this have lower_bound: "\<And>k. k \<le> m * n \<Longrightarrow> ?max_subseq R k \<ge> 1"
+ by (auto intro!: Max_ge)
+
+ fix b
+ assume not_mono_at: "\<forall>S. S \<subseteq> {0..m * n} \<and> card S = b + 1 \<longrightarrow> \<not> mono_on f R S"
+
+ {
+ fix S
+ assume "S \<subseteq> {0..m * n}" "card S \<ge> b + 1"
+ moreover from `card S \<ge> b + 1` obtain T where "T \<subseteq> S \<and> card T = Suc b"
+ using obtain_subset_with_card_n by (metis Suc_eq_plus1)
+ ultimately have "\<not> mono_on f R S" using not_mono_at by (auto dest: not_mono_on_subset)
+ }
+ from this have "\<forall>S. S \<subseteq> {0..m * n} \<and> mono_on f R S \<longrightarrow> card S \<le> b"
+ by (metis Suc_eq_plus1 Suc_leI not_le)
+ from this have "\<And>k. k \<le> m * n \<Longrightarrow> \<forall>S. S \<subseteq> {0..k} \<and> mono_on f R S \<longrightarrow> card S \<le> b"
+ using order_trans by force
+ from this non_empty have upper_bound: "\<And>k. k \<le> m * n \<Longrightarrow> ?max_subseq R k \<le> b"
+ by (auto intro: Max.boundedI)
+
+ from upper_bound lower_bound have "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq R k \<and> ?max_subseq R k \<le> b"
+ by auto
+ } note bounds = this
+
+ assume contraposition: "\<not> ?thesis"
+ from contraposition bounds[of "op \<le>" "m"] bounds[of "op \<ge>" "n"]
+ have "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq (op \<le>) k \<and> ?max_subseq (op \<le>) k \<le> m"
+ and "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq (op \<ge>) k \<and> ?max_subseq (op \<ge>) k \<le> n"
+ using reflp_def by simp+
+ from this have "\<forall>i \<in> {0..m * n}. phi i \<in> {1..m} \<times> {1..n}"
+ unfolding phi_def by auto
+ from this have subseteq: "phi ` {0..m * n} \<subseteq> {1..m} \<times> {1..n}" by blast
+ have card_product: "card ({1..m} \<times> {1..n}) = m * n" by (simp add: card_cartesian_product)
+ have "finite ({1..m} \<times> {1..n})" by blast
+ from subseteq card_product this have card_le: "card (phi ` {0..m * n}) \<le> m * n" by (metis card_mono)
+
+ {
+ fix i j
+ assume "i < (j :: nat)"
+ {
+ fix R
+ assume R: "reflp (R :: 'a::linorder \<Rightarrow> _)" "transp R" "R (f i) (f j)"
+ from one_member[OF `reflp R`, of "i"] have
+ "\<exists>S \<in> {S. S \<subseteq> {0..i} \<and> mono_on f R S \<and> i \<in> S}. card S = ?max_subseq R i"
+ by (intro exists_set_with_max_card) auto
+ from this obtain S where S: "S \<subseteq> {0..i} \<and> mono_on f R S \<and> i \<in> S" "card S = ?max_subseq R i" by auto
+ from S `i < j` finite_subset have "j \<notin> S" "finite S" "insert j S \<subseteq> {0..j}" by auto
+ from S(1) R `i < j` this have "mono_on f R (insert j S)"
+ unfolding mono_on_def reflp_def transp_def
+ by (metis atLeastAtMost_iff insert_iff le_antisym subsetCE)
+ from this have d: "insert j S \<in> {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S}"
+ using `insert j S \<subseteq> {0..j}` by blast
+ from this `j \<notin> S` S(1) have "card (insert j S) \<in>
+ card ` {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S} \<and> card S < card (insert j S)"
+ by (auto intro!: imageI) (auto simp add: `finite S`)
+ from this S(2) have "?max_subseq R i < ?max_subseq R j" by (auto intro: Max_gr)
+ } note max_subseq_increase = this
+ have "?max_subseq (op \<le>) i < ?max_subseq (op \<le>) j \<or> ?max_subseq (op \<ge>) i < ?max_subseq (op \<ge>) j"
+ proof (cases "f j \<ge> f i")
+ case True
+ from this max_subseq_increase[of "op \<le>", simplified] show ?thesis by simp
+ next
+ case False
+ from this max_subseq_increase[of "op \<ge>", simplified] show ?thesis by simp
+ qed
+ from this have "phi i \<noteq> phi j" using phi_def by auto
+ }
+ from this have "inj phi" unfolding inj_on_def by (metis less_linear)
+ from this have card_eq: "card (phi ` {0..m * n}) = m * n + 1" by (simp add: card_image inj_on_def)
+ from card_le card_eq show False by simp
+qed
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Sum_of_Powers.thy Fri Jun 12 10:33:02 2015 +0200
@@ -0,0 +1,215 @@
+(* Title: HOL/ex/Sum_of_Powers.thy
+ Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
+*)
+
+section {* Sum of Powers *}
+
+theory Sum_of_Powers
+imports Complex_Main
+begin
+
+subsection {* Additions to @{theory Binomial} Theory *}
+
+lemma of_nat_binomial_eq_mult_binomial_Suc:
+ assumes "k \<le> n"
+ shows "(of_nat :: (nat \<Rightarrow> ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
+proof -
+ have "of_nat (n + 1) * (\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
+ proof -
+ have "of_nat (n + 1) * (\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1) * (\<Prod>i\<in>Suc ` {..<k}. of_nat (Suc n - i))"
+ by (auto simp add: setprod.reindex)
+ also have "... = (\<Prod>i\<le>k. of_nat (Suc n - i))"
+ proof (cases k)
+ case (Suc k')
+ have "of_nat (n + 1) * (\<Prod>i\<in>Suc ` {..<Suc k'}. of_nat (Suc n - i)) = (\<Prod>i\<in>insert 0 (Suc ` {..k'}). of_nat (Suc n - i))"
+ by (subst setprod.insert) (auto simp add: lessThan_Suc_atMost)
+ also have "... = (\<Prod>i\<le>Suc k'. of_nat (Suc n - i))" by (simp only: Iic_Suc_eq_insert_0)
+ finally show ?thesis using Suc by simp
+ qed (simp)
+ also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i<k. of_nat (Suc n - i))"
+ by (cases k) (auto simp add: atMost_Suc lessThan_Suc_atMost)
+ also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
+ by (simp only: Suc_eq_plus1)
+ finally show ?thesis .
+ qed
+ from this have "(\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i<k. of_nat (Suc n - i))"
+ by (metis le_add2 nonzero_mult_divide_cancel_left not_one_le_zero of_nat_eq_0_iff times_divide_eq_left)
+ from assms this show ?thesis
+ by (auto simp add: binomial_altdef_of_nat setprod_dividef)
+qed
+
+lemma real_binomial_eq_mult_binomial_Suc:
+ assumes "k \<le> n"
+ shows "(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)"
+proof -
+ have "real (n choose k) = of_nat (n choose k)" by auto
+ also have "... = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
+ by (simp add: assms of_nat_binomial_eq_mult_binomial_Suc)
+ also have "... = (n + 1 - k) / (n + 1) * (Suc n choose k)"
+ using real_of_nat_def by auto
+ finally show ?thesis
+ by (metis (no_types, lifting) assms le_add1 le_trans of_nat_diff real_of_nat_1 real_of_nat_add real_of_nat_def)
+qed
+
+subsection {* Preliminaries *}
+
+lemma integrals_eq:
+ assumes "f 0 = g 0"
+ assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)"
+ shows "f x = g x"
+proof -
+ show "f x = g x"
+ proof (cases "x \<noteq> 0")
+ case True
+ from assms DERIV_const_ratio_const[OF this, of "\<lambda>x. f x - g x" 0]
+ show ?thesis by auto
+ qed (simp add: assms)
+qed
+
+lemma setsum_diff: "((\<Sum>i\<le>n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0"
+by (induct n) (auto simp add: field_simps)
+
+declare One_nat_def [simp del]
+
+subsection {* Bernoulli Numbers and Bernoulli Polynomials *}
+
+declare setsum.cong [fundef_cong]
+
+fun bernoulli :: "nat \<Rightarrow> real"
+where
+ "bernoulli 0 = (1::real)"
+| "bernoulli (Suc n) = (-1 / (n + 2)) * (\<Sum>k \<le> n. ((n + 2 choose k) * bernoulli k))"
+
+declare bernoulli.simps[simp del]
+
+definition
+ "bernpoly n = (\<lambda>x. \<Sum>k \<le> n. (n choose k) * bernoulli k * x ^ (n - k))"
+
+subsection {* Basic Observations on Bernoulli Polynomials *}
+
+lemma bernpoly_0: "bernpoly n 0 = bernoulli n"
+proof (cases n)
+ case 0
+ from this show "bernpoly n 0 = bernoulli n"
+ unfolding bernpoly_def bernoulli.simps by auto
+next
+ case (Suc n')
+ have "(\<Sum>k\<le>n'. real (Suc n' choose k) * bernoulli k * 0 ^ (Suc n' - k)) = 0"
+ by (rule setsum.neutral) auto
+ with Suc show ?thesis
+ unfolding bernpoly_def by simp
+qed
+
+lemma setsum_binomial_times_bernoulli:
+ "(\<Sum>k\<le>n. ((Suc n) choose k) * bernoulli k) = (if n = 0 then 1 else 0)"
+proof (cases n)
+ case 0
+ from this show ?thesis by (simp add: bernoulli.simps)
+next
+ case Suc
+ from this show ?thesis
+ by (simp add: bernoulli.simps)
+ (simp add: field_simps add_2_eq_Suc'[symmetric] del: add_2_eq_Suc add_2_eq_Suc')
+qed
+
+subsection {* Sum of Powers with Bernoulli Polynomials *}
+
+lemma bernpoly_derivative [derivative_intros]:
+ "(bernpoly (Suc n) has_real_derivative ((n + 1) * bernpoly n x)) (at x)"
+proof -
+ have "(bernpoly (Suc n) has_real_derivative (\<Sum>k\<le>n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k))) (at x)"
+ unfolding bernpoly_def by (rule DERIV_cong) (fast intro!: derivative_intros, simp)
+ moreover have "(\<Sum>k\<le>n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k)) = (n + 1) * bernpoly n x"
+ unfolding bernpoly_def
+ by (auto intro: setsum.cong simp add: setsum_right_distrib real_binomial_eq_mult_binomial_Suc[of _ n] Suc_eq_plus1 real_of_nat_diff)
+ ultimately show ?thesis by auto
+qed
+
+lemma diff_bernpoly:
+ "bernpoly n (x + 1) - bernpoly n x = n * x ^ (n - 1)"
+proof (induct n arbitrary: x)
+ case 0
+ show ?case unfolding bernpoly_def by auto
+next
+ case (Suc n)
+ have "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = (Suc n) * 0 ^ n"
+ unfolding bernpoly_0 unfolding bernpoly_def by (simp add: setsum_binomial_times_bernoulli zero_power)
+ from this have const: "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = real (Suc n) * 0 ^ n" by (simp add: power_0_left)
+ have hyps': "\<And>x. (real n + 1) * bernpoly n (x + 1) - (real n + 1) * bernpoly n x = real n * x ^ (n - Suc 0) * real (Suc n)"
+ unfolding right_diff_distrib[symmetric] by (simp add: Suc.hyps One_nat_def)
+ note [derivative_intros] = DERIV_chain'[where f = "\<lambda>x::real. x + 1" and g = "bernpoly (Suc n)" and s="UNIV"]
+ have derivative: "\<And>x. ((%x. bernpoly (Suc n) (x + 1) - bernpoly (Suc n) x - real (Suc n) * x ^ n) has_real_derivative 0) (at x)"
+ by (rule DERIV_cong) (fast intro!: derivative_intros, simp add: hyps')
+ from integrals_eq[OF const derivative] show ?case by simp
+qed
+
+lemma sum_of_powers: "(\<Sum>k\<le>n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)"
+proof -
+ from diff_bernpoly[of "Suc m", simplified] have "(m + (1::real)) * (\<Sum>k\<le>n. (real k) ^ m) = (\<Sum>k\<le>n. bernpoly (Suc m) (real k + 1) - bernpoly (Suc m) (real k))"
+ by (auto simp add: setsum_right_distrib intro!: setsum.cong)
+ also have "... = (\<Sum>k\<le>n. bernpoly (Suc m) (real (k + 1)) - bernpoly (Suc m) (real k))"
+ by (simp only: real_of_nat_1[symmetric] real_of_nat_add[symmetric])
+ also have "... = bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0"
+ by (simp only: setsum_diff[where f="\<lambda>k. bernpoly (Suc m) (real k)"]) simp
+ finally show ?thesis by (auto simp add: field_simps intro!: eq_divide_imp)
+qed
+
+subsection {* Instances for Square And Cubic Numbers *}
+
+lemma binomial_unroll:
+ "n > 0 \<Longrightarrow> (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))"
+by (cases n) (auto simp add: binomial.simps(2))
+
+lemma setsum_unroll:
+ "(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
+by auto (metis One_nat_def Suc_pred add.commute setsum_atMost_Suc)
+
+lemma bernoulli_unroll:
+ "n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
+by (cases n) (simp add: bernoulli.simps One_nat_def)+
+
+lemmas unroll = binomial.simps(1) binomial_unroll
+ bernoulli.simps(1) bernoulli_unroll setsum_unroll bernpoly_def
+
+lemma sum_of_squares: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
+proof -
+ have "real (\<Sum>k\<le>n::nat. k ^ 2) = (\<Sum>k\<le>n::nat. (real k) ^ 2)" by simp
+ also have "... = (bernpoly 3 (real (n + 1)) - bernpoly 3 0) / real (3 :: nat)"
+ by (auto simp add: sum_of_powers)
+ also have "... = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
+ by (simp add: unroll algebra_simps power2_eq_square power3_eq_cube One_nat_def[symmetric])
+ finally show ?thesis by simp
+qed
+
+lemma sum_of_squares_nat: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6"
+proof -
+ from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
+ by (auto simp add: field_simps)
+ from this have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
+ by (simp only: real_of_nat_inject[symmetric])
+ from this show ?thesis by auto
+qed
+
+lemma sum_of_cubes: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 / 4"
+proof -
+ have two_plus_two: "2 + 2 = 4" by simp
+ have power4_eq: "\<And>x::real. x ^ 4 = x * x * x * x"
+ by (simp only: two_plus_two[symmetric] power_add power2_eq_square)
+ have "real (\<Sum>k\<le>n::nat. k ^ 3) = (\<Sum>k\<le>n::nat. (real k) ^ 3)" by simp
+ also have "... = ((bernpoly 4 (n + 1) - bernpoly 4 0)) / (real (4 :: nat))"
+ by (auto simp add: sum_of_powers)
+ also have "... = ((n ^ 2 + n) / 2) ^ 2"
+ by (simp add: unroll algebra_simps power2_eq_square power4_eq power3_eq_cube)
+ finally show ?thesis by simp
+qed
+
+lemma sum_of_cubes_nat: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
+proof -
+ from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
+ by (auto simp add: field_simps)
+ from this have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
+ by (simp only: real_of_nat_inject[symmetric])
+ from this show ?thesis by auto
+qed
+
+end