add examples from Freek's top 100 theorems (thms 30, 73, 77)
authorbulwahn
Fri Jun 12 10:33:02 2015 +0200 (2015-06-12)
changeset 6060309ecbd791d4a
parent 60602 37588fbe39f9
child 60604 dd4253d5dd82
add examples from Freek's top 100 theorems (thms 30, 73, 77)
src/HOL/ROOT
src/HOL/ex/Ballot.thy
src/HOL/ex/Erdoes_Szekeres.thy
src/HOL/ex/Sum_of_Powers.thy
     1.1 --- a/src/HOL/ROOT	Wed Jun 17 18:44:23 2015 +0200
     1.2 +++ b/src/HOL/ROOT	Fri Jun 12 10:33:02 2015 +0200
     1.3 @@ -594,6 +594,9 @@
     1.4      SAT_Examples
     1.5      SOS
     1.6      SOS_Cert
     1.7 +    Ballot
     1.8 +    Erdoes_Szekeres
     1.9 +    Sum_of_Powers
    1.10    theories [skip_proofs = false]
    1.11      Meson_Test
    1.12    theories [condition = ISABELLE_FULL_TEST]
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Ballot.thy	Fri Jun 12 10:33:02 2015 +0200
     2.3 @@ -0,0 +1,593 @@
     2.4 +(*   Title: HOL/ex/Ballot.thy
     2.5 +     Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
     2.6 +*)
     2.7 +
     2.8 +section {* Bertrand's Ballot Theorem *}
     2.9 +
    2.10 +theory Ballot
    2.11 +imports
    2.12 +  Complex_Main
    2.13 +  "~~/src/HOL/Library/FuncSet"
    2.14 +begin
    2.15 +
    2.16 +subsection {* Preliminaries *}
    2.17 +
    2.18 +subsubsection {* Dedicated Simplification Setup *}
    2.19 +
    2.20 +declare One_nat_def[simp del]
    2.21 +declare add_2_eq_Suc'[simp del]
    2.22 +declare atLeastAtMost_iff[simp del]
    2.23 +declare fun_upd_apply[simp del]
    2.24 +
    2.25 +lemma [simp]: "1 \<le> n \<Longrightarrow> n : {1..(n :: nat)}"
    2.26 +by (auto simp add: atLeastAtMost_iff)
    2.27 +
    2.28 +lemma [simp]: "(n :: nat) + 2 \<notin> {1..n + 1}"
    2.29 +by (auto simp add: atLeastAtMost_iff)
    2.30 +
    2.31 +subsubsection {* Additions to @{theory Set} Theory *}
    2.32 +
    2.33 +lemma ex1_iff_singleton: "(EX! x. x : S) \<longleftrightarrow> (EX x. S = {x})"
    2.34 +proof
    2.35 +  assume "EX! x. x : S"
    2.36 +  from this show "EX x. S = {x}"
    2.37 +    by (metis Un_empty_left Un_insert_left insertI1 insert_absorb subsetI subset_antisym)
    2.38 +next
    2.39 +  assume "EX x. S = {x}"
    2.40 +  thus "EX! x. x : S" by (metis (full_types) singleton_iff)
    2.41 +qed
    2.42 +
    2.43 +subsubsection {* Additions to @{theory Finite_Set} Theory *}
    2.44 +
    2.45 +lemma card_singleton[simp]: "card {x} = 1"
    2.46 +  by simp
    2.47 +
    2.48 +lemma finite_bij_subset_implies_equal_sets:
    2.49 +  assumes "finite T" "\<exists>f. bij_betw f S T" "S <= T"
    2.50 +  shows "S = T"
    2.51 +using assms by (metis (lifting) bij_betw_def bij_betw_inv endo_inj_surj)
    2.52 +
    2.53 +lemma singleton_iff_card_one: "(EX x. S = {x}) \<longleftrightarrow> card S = 1"
    2.54 +proof
    2.55 +  assume "EX x. S = {x}"
    2.56 +  then show "card S = 1" by auto
    2.57 +next
    2.58 +  assume c: "card S = 1"
    2.59 +  from this have s: "S \<noteq> {}" by (metis card_empty zero_neq_one)
    2.60 +  from this obtain a where a: "a \<in> S" by auto
    2.61 +  from this s obtain T where S: "S = insert a T" and a: "a \<notin> T"
    2.62 +    by (metis Set.set_insert)
    2.63 +  from c S a have "card T = 0"
    2.64 +    by (metis One_nat_def card_infinite card_insert_disjoint old.nat.inject)
    2.65 +  from this c S have "T = {}" by (metis (full_types) card_eq_0_iff finite_insert zero_neq_one)
    2.66 +  from this S show "EX x. S = {x}" by auto
    2.67 +qed
    2.68 +
    2.69 +subsubsection {* Additions to @{theory Nat} Theory *}
    2.70 +
    2.71 +lemma square_diff_square_factored_nat:
    2.72 +  shows "(x::nat) * x - y * y = (x + y) * (x - y)"
    2.73 +proof (cases "(x::nat) \<ge> y")
    2.74 +  case True
    2.75 +  from this show ?thesis by (simp add: algebra_simps diff_mult_distrib2)
    2.76 +next
    2.77 +  case False
    2.78 +  from this show ?thesis by (auto intro: mult_le_mono)
    2.79 +qed
    2.80 +
    2.81 +subsubsection {* Additions to @{theory FuncSet} Theory *}
    2.82 +
    2.83 +lemma extensional_constant_function_is_unique:
    2.84 +  assumes c: "c : T"
    2.85 +  shows "EX! f. f : S \<rightarrow>\<^sub>E T & (\<forall>x \<in> S. f x = c)"
    2.86 +proof
    2.87 +  def f == "(%x. if x \<in> S then c else undefined)"
    2.88 +  from c show "f : S \<rightarrow>\<^sub>E T & (\<forall>x \<in> S. f x = c)" unfolding f_def by auto
    2.89 +next
    2.90 +  fix f
    2.91 +  assume "f : S \<rightarrow>\<^sub>E T & (\<forall>x \<in> S. f x = c)"
    2.92 +  from this show "f = (%x. if x \<in> S then c else undefined)" by (metis PiE_E)
    2.93 +qed
    2.94 +
    2.95 +lemma PiE_insert_restricted_eq:
    2.96 +  assumes a: "x \<notin> S"
    2.97 +  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))})"
    2.98 +proof -
    2.99 +  {
   2.100 +    fix f
   2.101 +    assume "f : {f : insert x S \<rightarrow>\<^sub>E T. P f}"
   2.102 +    from this a have "f :(\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
   2.103 +    by (auto intro!: image_eqI[where x="(f x, f(x:=undefined))"])
   2.104 +      (metis PiE_E fun_upd_other insertCI, metis (full_types) PiE_E fun_upd_in_PiE)
   2.105 +  } moreover
   2.106 +  {
   2.107 +    fix f
   2.108 +    assume "f :(\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
   2.109 +    from this have "f : {f : insert x S \<rightarrow>\<^sub>E T. P f}"
   2.110 +      by (auto elim!: PiE_fun_upd split: prod.split)
   2.111 +  }
   2.112 +  ultimately show ?thesis
   2.113 +    by (intro set_eqI iffI) assumption+
   2.114 +qed
   2.115 +
   2.116 +lemma card_extensional_funcset_insert:
   2.117 +  assumes "x \<notin> S" "finite S" "finite T"
   2.118 +  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))})"
   2.119 +proof -
   2.120 +  from `finite S` `finite T` have finite_funcset: "finite (S \<rightarrow>\<^sub>E T)" by (rule finite_PiE)
   2.121 +  have finite: "\<forall>y\<in>T. finite {f : S \<rightarrow>\<^sub>E T. P (f(x:=y))}"
   2.122 +    by (auto intro: finite_subset[OF _ finite_funcset])
   2.123 +  from `x \<notin> S`have inj: "inj_on (%(y, g). g(x:=y)) (UNIV \<times> (S \<rightarrow>\<^sub>E T))"
   2.124 +  unfolding inj_on_def
   2.125 +  by auto (metis fun_upd_same, metis PiE_E fun_upd_idem_iff fun_upd_upd fun_upd_same)
   2.126 +  from `x \<notin> S` have "card {f : insert x S \<rightarrow>\<^sub>E T. P f} =
   2.127 +    card ((\<lambda>(y, g). g(x:=y)) ` (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))}))"
   2.128 +    by (subst PiE_insert_restricted_eq) auto
   2.129 +  also from subset_inj_on[OF inj, of "SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))}"]
   2.130 +  have "\<dots> = card (SIGMA y:T. {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})" by (subst card_image) auto
   2.131 +  also from `finite T` finite have "\<dots> = (\<Sum>y\<in>T. card {f : S \<rightarrow>\<^sub>E T. P (f(x := y))})"
   2.132 +    by (simp only: card_SigmaI)
   2.133 +  finally show ?thesis .
   2.134 +qed
   2.135 +
   2.136 +subsubsection {* Additions to @{theory Binomial} Theory *}
   2.137 +
   2.138 +lemma Suc_times_binomial_add:
   2.139 +  "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
   2.140 +proof -
   2.141 +  have minus: "Suc (a + b) - a = Suc b" "Suc (a + b) - (Suc a) = b" by auto
   2.142 +  from fact_fact_dvd_fact[of "Suc a" "b"] have "fact (Suc a) * fact b dvd (fact (Suc a + b) :: nat)"
   2.143 +    by fast
   2.144 +  from this have dvd1: "Suc a * fact a * fact b dvd fact (Suc (a + b))"  
   2.145 +    by (simp only: fact_Suc add_Suc[symmetric] of_nat_id)
   2.146 +  have dvd2: "fact a * (Suc b * fact b) dvd fact (Suc (a + b))"
   2.147 +    by (metis add_Suc_right fact_Suc fact_fact_dvd_fact of_nat_id)
   2.148 +  have "Suc a * (Suc (a + b) choose Suc a) = Suc a * (fact (Suc (a + b)) div (fact (Suc a) * fact b))"
   2.149 +    by (simp only: binomial_altdef_nat minus(2))
   2.150 +  also have "... = Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))"
   2.151 +   unfolding fact_Suc[of a] div_mult_swap[OF dvd1] of_nat_id by (simp only: algebra_simps)
   2.152 +  also have "... = Suc b * fact (Suc (a + b)) div (Suc b * (fact a * fact b))"
   2.153 +    by (simp only: div_mult_mult1)
   2.154 +  also have "... = Suc b * (fact (Suc (a + b)) div (fact a * fact (Suc b)))"
   2.155 +    unfolding fact_Suc[of b] div_mult_swap[OF dvd2] of_nat_id by (simp only: algebra_simps)
   2.156 +  also have "... = Suc b * (Suc (a + b) choose a)"
   2.157 +    by (simp only: binomial_altdef_nat minus(1))
   2.158 +  finally show ?thesis .
   2.159 +qed
   2.160 +
   2.161 +subsection {* Formalization of Problem Statement *}
   2.162 +
   2.163 +subsubsection {* Basic Definitions *}
   2.164 +
   2.165 +datatype vote = A | B
   2.166 +
   2.167 +definition
   2.168 +  "all_countings a b = card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a
   2.169 +    & card {x : {1 .. a + b}. f x = B} = b}"
   2.170 +
   2.171 +definition
   2.172 +  "valid_countings a b =
   2.173 +    card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a
   2.174 +    & card {x : {1 .. a + b}. f x = B} = b
   2.175 +    & (\<forall>m \<in> {1 .. a + b }. card {x \<in> {1..m}. f x = A} > card {x \<in> {1..m}. f x = B})}"
   2.176 +
   2.177 +subsubsection {* Equivalence of Alternative Definitions *}
   2.178 +
   2.179 +lemma definition_rewrite_generic:
   2.180 +  assumes "case vote of A \<Rightarrow> count = a | B \<Rightarrow> count = b"
   2.181 +  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}
   2.182 +   = {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = vote} = count \<and> P f}"
   2.183 +proof -
   2.184 +  let ?other_vote = "case vote of A \<Rightarrow> B | B \<Rightarrow> A"
   2.185 +  let ?other_count = "case vote of A \<Rightarrow> b | B \<Rightarrow> a" 
   2.186 +  {
   2.187 +    fix f
   2.188 +    assume "card {x : {1 .. a + b}. f x = vote} = count"
   2.189 +    from this have c: "card ({1 .. a + b} - {x : {1 .. a + b}. f x = vote}) = a + b - count"
   2.190 +      by (subst card_Diff_subset) auto
   2.191 +    have "{1 .. a + b} - {x : {1 .. a + b}. f x = vote} = {x : {1 .. a + b}. f x ~= vote}" by auto
   2.192 +    from this c have not_A:" card {x : {1 .. a + b}. f x ~= vote} = a + b - count" by auto
   2.193 +    have "!x. (f x ~= vote) = (f x = ?other_vote)"
   2.194 +      by (cases vote, auto) (case_tac "f x", auto)+
   2.195 +    from this not_A assms have "card {x : {1 .. a + b}. f x = ?other_vote} = ?other_count"
   2.196 +      by auto (cases vote, auto)
   2.197 +  }
   2.198 +  from this have "{f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}.
   2.199 +    card {x : {1 .. a + b}. f x = vote} = count & card {x : {1 .. a + b}. f x = ?other_vote} = ?other_count & P f} =
   2.200 +    {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = vote} = count & P f}"
   2.201 +    by auto
   2.202 +  from this assms show ?thesis by (cases vote) auto
   2.203 +qed
   2.204 +
   2.205 +lemma all_countings_def':
   2.206 +  "all_countings a b = card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a}"
   2.207 +unfolding all_countings_def definition_rewrite_generic[of a a _ A "\<lambda>_. True", simplified] ..
   2.208 +
   2.209 +lemma all_countings_def'':
   2.210 +  "all_countings a b = card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = B} = b}"
   2.211 +unfolding all_countings_def definition_rewrite_generic[of b _ b B  "\<lambda>_. True", simplified] ..
   2.212 +
   2.213 +lemma valid_countings_def':
   2.214 +  "valid_countings a b =
   2.215 +    card {f : {1 .. a + b} \<rightarrow>\<^sub>E {A, B}. card {x : {1 .. a + b}. f x = A} = a
   2.216 +    & (\<forall>m \<in> {1 .. a + b }. card {x \<in> {1..m}. f x = A} > card {x \<in> {1..m}. f x = B})}"
   2.217 +unfolding valid_countings_def definition_rewrite_generic[of a a _ A, simplified] ..
   2.218 +
   2.219 +subsubsection {* Cardinality of Sets of Functions *}
   2.220 +
   2.221 +lemma one_extensional_constant_function:
   2.222 +  assumes "c : T"
   2.223 +  shows "card {f : S \<rightarrow>\<^sub>E T. (\<forall>x \<in> S. f x = c)} = 1"
   2.224 +using assms
   2.225 +  by (auto simp only: singleton_iff_card_one[symmetric] ex1_iff_singleton[symmetric] mem_Collect_eq
   2.226 +    elim!: extensional_constant_function_is_unique)
   2.227 +
   2.228 +lemma card_filtered_set_eq_card_set_implies_forall:
   2.229 +  assumes f: "finite S"
   2.230 +  assumes c: "card {x : S. P x} = card S"
   2.231 +  shows "\<forall>x \<in> S. P x"
   2.232 +proof -
   2.233 +  from f c have "\<exists>f. bij_betw f {x : S. P x} S"
   2.234 +    by (metis Collect_mem_eq finite_Collect_conjI finite_same_card_bij)
   2.235 +  from f this have eq: "{x : S. P x} = S"
   2.236 +    by (metis (mono_tags) finite_bij_subset_implies_equal_sets Collect_mem_eq Collect_mono)
   2.237 +  from this show ?thesis by auto
   2.238 +qed
   2.239 +
   2.240 +lemma card_filtered_set_from_n_eq_n_implies_forall:
   2.241 +  shows "(card {x : {1..n}. P x} = n) = (\<forall>x \<in> {1..n}. P x)"
   2.242 +proof
   2.243 +  assume "card {x : {1..n}. P x} = n"
   2.244 +  from this show "\<forall>x \<in> {1..n}. P x"
   2.245 +    by (metis card_atLeastAtMost card_filtered_set_eq_card_set_implies_forall
   2.246 +     diff_Suc_1 finite_atLeastAtMost)
   2.247 +next
   2.248 +  assume "\<forall>x \<in> {1..n}. P x"
   2.249 +  from this have "{x : {1..n}. P x} = {1..n}" by auto
   2.250 +  from this show "card {x : {1..n}. P x} = n" by simp
   2.251 +qed
   2.252 +
   2.253 +subsubsection {* Cardinality of the Inverse Image of an Updated Function *}
   2.254 +
   2.255 +lemma fun_upd_not_in_Domain:
   2.256 +  assumes "x' \<notin> S"
   2.257 +  shows "card {x : S. (f(x' := y)) x = c} = card {x : S. f x = c}"
   2.258 +using assms by (auto simp add: fun_upd_apply) metis
   2.259 +
   2.260 +lemma card_fun_upd_noteq_constant:
   2.261 +  assumes "x' \<notin> S" "c \<noteq> d"
   2.262 +  shows "card {x : insert x' S. (f(x' := d)) x = c} = card {x : S. f x = c}"
   2.263 +using assms by (auto simp add: fun_upd_apply) metis
   2.264 +
   2.265 +lemma card_fun_upd_eq_constant:
   2.266 +  assumes "x' \<notin> S" "finite S"
   2.267 +  shows "card {x : insert x' S. (f(x' := c)) x = c} = card {x : S. f x = c} + 1"
   2.268 +proof -
   2.269 +  from `x' \<notin> S` have "{x : insert x' S. (f(x' := c)) x = c} = insert x' {x \<in> S. f x = c}"
   2.270 +    by (auto simp add: fun_upd_same fun_upd_other fun_upd_apply)
   2.271 +  from `x' \<notin> S` `finite S` this show ?thesis by force
   2.272 +qed
   2.273 +
   2.274 +subsubsection {* Relevant Specializations *}
   2.275 +
   2.276 +lemma atLeastAtMost_plus2_conv: "{1..(n :: nat) + 2} = insert (n + 2) {1..n + 1}" 
   2.277 +by (auto simp add: atLeastAtMost_iff)
   2.278 +
   2.279 +lemma card_fun_upd_noteq_constant_plus2:
   2.280 +  assumes "v' \<noteq> v"
   2.281 +  shows "card {x\<in>{1..(a :: nat) + b + 2}. (f(a + b + 2 := v')) x = v} =
   2.282 +    card {x \<in> {1..a + b + 1}. f x = v}"
   2.283 +using assms unfolding atLeastAtMost_plus2_conv by (subst card_fun_upd_noteq_constant) auto
   2.284 +
   2.285 +lemma card_fun_upd_eq_constant_plus2:
   2.286 +  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"
   2.287 +unfolding atLeastAtMost_plus2_conv by (subst card_fun_upd_eq_constant) auto
   2.288 +
   2.289 +lemmas card_fun_upd_simps = card_fun_upd_noteq_constant_plus2 card_fun_upd_eq_constant_plus2
   2.290 +
   2.291 +lemma split_into_sum:
   2.292 +  "card {f : {1 .. (n :: nat) + 2} \<rightarrow>\<^sub>E {A, B}. P f} =
   2.293 +   card {f : {1 .. n + 1} \<rightarrow>\<^sub>E {A, B}. P (f(n + 2 := A))} +
   2.294 +   card {f : {1 .. n + 1} \<rightarrow>\<^sub>E {A, B}. P (f(n + 2 := B))}"
   2.295 +by (auto simp add: atLeastAtMost_plus2_conv card_extensional_funcset_insert)
   2.296 +
   2.297 +subsection {* Facts About @{term all_countings} *}
   2.298 +
   2.299 +subsubsection {* Simple Non-Recursive Cases *}
   2.300 +
   2.301 +lemma all_countings_a_0:
   2.302 +  "all_countings a 0 = 1"
   2.303 +unfolding all_countings_def'
   2.304 +by (simp add: card_filtered_set_from_n_eq_n_implies_forall one_extensional_constant_function)
   2.305 +
   2.306 +lemma all_countings_0_b:
   2.307 +  "all_countings 0 b = 1"
   2.308 +unfolding all_countings_def''
   2.309 +by (simp add: card_filtered_set_from_n_eq_n_implies_forall one_extensional_constant_function)
   2.310 +
   2.311 +subsubsection {* Recursive Case *}
   2.312 +
   2.313 +lemma all_countings_Suc_Suc:
   2.314 +  "all_countings (a + 1) (b + 1) = all_countings a (b + 1) + all_countings (a + 1) b"
   2.315 +proof -
   2.316 +  let ?intermed = "%y. card {f : {1..a + b + 1} \<rightarrow>\<^sub>E {A, B}. card {x : {1..a + b + 2}.
   2.317 +    (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}"
   2.318 +  have "all_countings (a + 1) (b + 1) = card {f : {1..a + b + 2} \<rightarrow>\<^sub>E {A, B}.
   2.319 +          card {x : {1..a + b + 2}. f x = A} = a + 1 \<and> card {x : {1..a + b + 2}. f x = B} = b + 1}"
   2.320 +    unfolding all_countings_def[of "a+1" "b+1"] by (simp add: algebra_simps One_nat_def add_2_eq_Suc')
   2.321 +  also have "\<dots> = ?intermed A + ?intermed B" unfolding split_into_sum ..
   2.322 +  also have "\<dots> = all_countings a (b + 1) + all_countings (a + 1) b"
   2.323 +    by (simp add: card_fun_upd_simps all_countings_def) (simp add: algebra_simps)
   2.324 +  finally show ?thesis .
   2.325 +qed
   2.326 +
   2.327 +subsubsection {* Executable Definition *}
   2.328 +
   2.329 +declare all_countings_def [code del]
   2.330 +declare all_countings_a_0 [code]
   2.331 +declare all_countings_0_b [code]
   2.332 +declare all_countings_Suc_Suc [unfolded One_nat_def, simplified, code]
   2.333 +
   2.334 +value "all_countings 1 0"
   2.335 +value "all_countings 0 1"
   2.336 +value "all_countings 1 1"
   2.337 +value "all_countings 2 1"
   2.338 +value "all_countings 1 2"
   2.339 +value "all_countings 2 4"
   2.340 +value "all_countings 4 2"
   2.341 +
   2.342 +subsubsection {* Relation to Binomial Function *}
   2.343 +
   2.344 +lemma all_countings:
   2.345 +  "all_countings a b = (a + b) choose a"
   2.346 +proof (induct a arbitrary: b)
   2.347 +  case 0
   2.348 +  show ?case by (simp add: all_countings_0_b)
   2.349 +next
   2.350 +  case (Suc a)
   2.351 +  note Suc_hyps = Suc.hyps
   2.352 +  show ?case
   2.353 +  proof (induct b)
   2.354 +    case 0
   2.355 +    show ?case by (simp add: all_countings_a_0)
   2.356 +  next
   2.357 +    case (Suc b)
   2.358 +    from Suc_hyps Suc.hyps show ?case
   2.359 +      by (metis Suc_eq_plus1 Suc_funpow add_Suc_shift binomial_Suc_Suc funpow_swap1
   2.360 +          all_countings_Suc_Suc)
   2.361 +  qed
   2.362 +qed
   2.363 +
   2.364 +subsection {* Facts About @{term valid_countings} *}
   2.365 +
   2.366 +subsubsection {* Non-Recursive Cases *}
   2.367 +
   2.368 +lemma valid_countings_a_0:
   2.369 +  "valid_countings a 0 = 1"
   2.370 +proof -
   2.371 +  {
   2.372 +    fix f
   2.373 +    {
   2.374 +      assume "card {x : {1..a}. f x = A} = a"
   2.375 +      from this have a: "\<forall>x \<in> {1..a}. f x = A"
   2.376 +        by (intro card_filtered_set_eq_card_set_implies_forall) auto
   2.377 +      {
   2.378 +        fix i m
   2.379 +        assume e: "1 <= i"  "i <= m" "m <= a"
   2.380 +        from a e have "{x : {1..m}. f x = A} = {1 .. m}" by (auto simp add: atLeastAtMost_iff)
   2.381 +        from this have "card {x : {1..m}. f x = A} = m" by auto
   2.382 +        from a e this have "card {x : {1..m}. f x = A} = m \<and> card {x : {1..m}. f x = B} = 0"
   2.383 +          by (auto simp add: atLeastAtMost_iff)
   2.384 +      }
   2.385 +      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"
   2.386 +        by (auto simp del: card_0_eq simp add: atLeastAtMost_iff)
   2.387 +    }
   2.388 +    from this have "((card {x : {1..a}. f x = A} = a) &
   2.389 +      (\<forall>m \<in> {1..a}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A})) =
   2.390 +      (card {x : {1..a}. f x = A} = a)" by blast
   2.391 +  } note redundant_disjunct = this
   2.392 +  show ?thesis
   2.393 +    unfolding valid_countings_def'
   2.394 +    by (auto simp add: redundant_disjunct all_countings_a_0[unfolded all_countings_def', simplified])
   2.395 +qed
   2.396 +
   2.397 +lemma valid_countings_eq_zero:
   2.398 +  assumes "a \<le> b" "0 < b"
   2.399 +  shows "valid_countings a b = 0"
   2.400 +proof -
   2.401 +  from assms have is_empty: "{f \<in> {1..a + b} \<rightarrow>\<^sub>E {A, B}. 
   2.402 +    card {x \<in> {1..a + b}. f x = A} = a \<and>
   2.403 +    card {x \<in> {1..a + b}. f x = B} = b \<and>
   2.404 +    (\<forall>m \<in> {1..a + b}. card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A})} = {}"
   2.405 +  by auto (intro bexI[of _ "a + b"], auto)
   2.406 +  show ?thesis
   2.407 +    unfolding valid_countings_def by (metis card_empty is_empty)
   2.408 +qed
   2.409 +
   2.410 +subsubsection {* Recursive Cases *}
   2.411 +
   2.412 +lemma valid_countings_Suc_Suc_recursive:
   2.413 +  assumes "b < a"
   2.414 +  shows "valid_countings (a + 1) (b + 1) = valid_countings a (b + 1) + valid_countings (a + 1) b"
   2.415 +proof -
   2.416 +  let ?intermed = "%y. card {f : {1..a + b + 1} \<rightarrow>\<^sub>E {A, B}. card {x : {1..a + b + 2}.
   2.417 +    (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
   2.418 +    \<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})}"
   2.419 +  {
   2.420 +    fix f
   2.421 +    let ?a = "%c. card {x \<in> {1.. a + b + 1}. f x = A} = c"
   2.422 +    let ?b = "%c. card {x \<in> {1.. a + b + 1}. f x = B} = c"
   2.423 +    let ?c = "%c. (\<forall>m\<in>{1.. a + b + 2}. card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B}
   2.424 +        < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A})"
   2.425 +    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})"
   2.426 +    {
   2.427 +      fix c
   2.428 +      have "(\<forall>m\<in>{1.. a + b + 1}. card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B}
   2.429 +        < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}) = ?d"
   2.430 +      proof (rule iffI, auto)
   2.431 +        fix m
   2.432 +        assume 1: "\<forall>m\<in>{1..a + b + 1}.
   2.433 +          card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B} < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}"
   2.434 +        assume 2: "m \<in> {1..a + b + 1}"
   2.435 +        from 2 have 3: "a + b + 2 \<notin> {1..m}" by (simp add: atLeastAtMost_iff)
   2.436 +        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}"
   2.437 +          by auto
   2.438 +        from this show "card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A}"
   2.439 +          by (simp add: fun_upd_not_in_Domain[OF 3])
   2.440 +      next
   2.441 +        fix m
   2.442 +        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}"
   2.443 +        assume 2: "m \<in> {1..a + b + 1}"
   2.444 +        from 2 have 3: "a + b + 2 \<notin> {1..m}" by (simp add: atLeastAtMost_iff)
   2.445 +        from 1 2 have "card {x \<in> {1..m}. f x = B} < card {x \<in> {1..m}. f x = A}" by auto
   2.446 +        from this show
   2.447 +          "card {x \<in> {1..m}. (f(a + b + 2 := c)) x = B} < card {x \<in> {1..m}. (f(a + b + 2 := c)) x = A}"
   2.448 +          by (simp add: fun_upd_not_in_Domain[OF 3])
   2.449 +      qed
   2.450 +    } note common = this
   2.451 +    {
   2.452 +      assume cardinalities: "?a a" "?b (b + 1)"
   2.453 +      have "?c A = ?d"
   2.454 +        unfolding atLeastAtMost_plus2_conv
   2.455 +        by (simp add: cardinalities card_fun_upd_simps `b < a` common)
   2.456 +    } moreover
   2.457 +    {
   2.458 +      assume cardinalities: "?a (a + 1)" "?b b"
   2.459 +      have "?c B = ?d"
   2.460 +        unfolding atLeastAtMost_plus2_conv
   2.461 +        by (simp add: cardinalities card_fun_upd_simps `b < a` common)
   2.462 +    } 
   2.463 +    ultimately have "(?a a & ?b (b + 1) & ?c A) = (?a a & ?b (b + 1) & ?d)"
   2.464 +      "(?a (a + 1) & ?b b & ?c B) = (?a (a + 1) & ?b b & ?d)" by blast+
   2.465 +  } note eq_inner = this  
   2.466 +  have "valid_countings (a + 1) (b + 1) = card {f : {1..a + b + 2} \<rightarrow>\<^sub>E {A, B}.
   2.467 +    card {x : {1..a + b + 2}. f x = A} = a + 1 \<and> card {x : {1..a + b + 2}. f x = B} = b + 1 \<and>
   2.468 +    (\<forall>m \<in> {1..a + b + 2}. card {x : {1..m}. f x = B} < card {x : {1..m}. f x = A})}"
   2.469 +    unfolding valid_countings_def[of "a + 1" "b + 1"]
   2.470 +    by (simp add: algebra_simps One_nat_def add_2_eq_Suc')
   2.471 +  also have "\<dots> = ?intermed A + ?intermed B" unfolding split_into_sum .. 
   2.472 +  also have "\<dots> = valid_countings a (b + 1) + valid_countings (a + 1) b"
   2.473 +    by (simp add: card_fun_upd_simps eq_inner valid_countings_def) (simp add: algebra_simps)
   2.474 +  finally show ?thesis .
   2.475 +qed
   2.476 +
   2.477 +lemma valid_countings_Suc_Suc:
   2.478 +  "valid_countings (a + 1) (b + 1) =
   2.479 +    (if a \<le> b then 0 else valid_countings a (b + 1) + valid_countings (a + 1) b)"
   2.480 +by (auto simp add: valid_countings_eq_zero valid_countings_Suc_Suc_recursive)
   2.481 +
   2.482 +lemma valid_countings_0_Suc: "valid_countings 0 (Suc b) = 0"
   2.483 +by (simp add: valid_countings_eq_zero)
   2.484 +
   2.485 +subsubsection {* Executable Definition *}
   2.486 +
   2.487 +declare valid_countings_def [code del]
   2.488 +declare valid_countings_a_0 [code]
   2.489 +declare valid_countings_0_Suc [code]       
   2.490 +declare valid_countings_Suc_Suc [unfolded One_nat_def, simplified, code]
   2.491 +
   2.492 +value "valid_countings 1 0"
   2.493 +value "valid_countings 0 1"
   2.494 +value "valid_countings 1 1"
   2.495 +value "valid_countings 2 1"
   2.496 +value "valid_countings 1 2"
   2.497 +value "valid_countings 2 4"
   2.498 +value "valid_countings 4 2"
   2.499 +
   2.500 +subsubsection {* Relation to Binomial Function *}
   2.501 +
   2.502 +lemma valid_countings:
   2.503 +  "(a + b) * valid_countings a b = (a - b) * ((a + b) choose a)"
   2.504 +proof (induct a arbitrary: b rule: nat.induct[unfolded Suc_eq_plus1])
   2.505 +  case 1
   2.506 +  have "b = 0 | (EX b'. b = b' + 1)" by (cases b) simp+
   2.507 +  from this show ?case
   2.508 +    by (auto simp : valid_countings_eq_zero valid_countings_a_0)
   2.509 +next
   2.510 +  case (2 a)
   2.511 +  note a_hyp = "2.hyps"
   2.512 +  show ?case
   2.513 +  proof (induct b rule: nat.induct[unfolded Suc_eq_plus1])
   2.514 +    case 1
   2.515 +    show ?case by (simp add: valid_countings_a_0)
   2.516 +  next
   2.517 +    case (2 b)
   2.518 +    note b_hyp = "2.hyps"
   2.519 +    show ?case
   2.520 +    proof(cases "a <= b")
   2.521 +      case True
   2.522 +      from this show ?thesis
   2.523 +        unfolding valid_countings_Suc_Suc if_True by (simp add: algebra_simps)
   2.524 +    next
   2.525 +      case False
   2.526 +      from this have "b < a" by simp
   2.527 +      have makes_plus_2: "a + 1 + (b + 1) = a + b + 2"
   2.528 +        by (metis Suc_eq_plus1 add_Suc add_Suc_right one_add_one)
   2.529 +      from b_hyp have b_hyp: "(a + b + 1) * valid_countings (a + 1) b = (a + 1 - b) * (a + b + 1 choose (a + 1))"
   2.530 +        by (simp add: algebra_simps)
   2.531 +      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)"
   2.532 +        by (simp add: algebra_simps)
   2.533 +      have "a - b \<le> a * a - b * b" by (simp add: square_diff_square_factored_nat)
   2.534 +      from this `b < a` have "a + b * b \<le> b + a * a" by auto      
   2.535 +      moreover from `\<not> a \<le> b` have "b * b \<le> a + a * b" by (meson linear mult_le_mono1 trans_le_add2)
   2.536 +      moreover have "1 + b + a * b \<le> a * a"
   2.537 +      proof -
   2.538 +         from `b < a` have "1 + b + a * b \<le> a + a * b" by simp
   2.539 +         also have "\<dots> \<le> a * (b + 1)" by (simp add: algebra_simps)
   2.540 +         also from `b < a` have "\<dots> \<le> a * a" by simp
   2.541 +         finally show ?thesis .
   2.542 +      qed
   2.543 +      moreover note `b < a`
   2.544 +      ultimately have rearrange: "(a + 1) * (a - (b + 1)) + (a + 1 - b) * (b + 1) = (a - b) * (a + b + 1)"
   2.545 +        by (simp add: algebra_simps)
   2.546 +      have rewrite1: "\<And>(A :: nat) B C D E F. A * B * ((C * D) + (E * F)) = A * ((C * (B * D)) + (E * (B * F)))"
   2.547 +        by (simp add: algebra_simps)
   2.548 +      have rewrite2: "\<And>(A :: nat) B C D E F. A * (B * (C * D) + E * (F * D)) = (C * B + E * F) * (A * D)"
   2.549 +        by (simp only: algebra_simps)
   2.550 +      have "(a + b + 2) * (a + 1) * (a + b + 1) * valid_countings (a + 1) (b + 1) =
   2.551 +        (a + b + 2) * (a + 1) * ((a + b + 1) * valid_countings a (b + 1) + (a + b + 1) * valid_countings (a + 1) b)"
   2.552 +        unfolding valid_countings_Suc_Suc_recursive[OF `b < a`] by (simp only: algebra_simps)
   2.553 +      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))))"
   2.554 +        unfolding b_hyp a_hyp rewrite1 by (simp only: add.assoc)
   2.555 +      also have "... = ((a + 1) * (a - (b + 1)) + (a + 1 - b) * (b + 1)) * ((a + b + 2) * (a + 1 + b choose a))"
   2.556 +        unfolding Suc_times_binomial_add[simplified Suc_eq_plus1] rewrite2 by (simp only: algebra_simps)
   2.557 +      also have "... = (a - b) * (a + b + 1) * ((a + 1 + b + 1) * (a + 1 + b choose a))"
   2.558 +        by (simp add: rearrange)
   2.559 +      also have "... = (a - b) * (a + b + 1) * (((a + 1 + b + 1) choose (a + 1)) * (a + 1))"
   2.560 +        by (subst Suc_times_binomial_eq[simplified Suc_eq_plus1, where k = "a" and n = "a + 1 + b"]) auto
   2.561 +      also have "... = (a - b) * (a + 1) * (a + b + 1) * (a + 1 + (b + 1) choose (a + 1))"
   2.562 +        by (auto simp add: add.assoc)
   2.563 +      finally show ?thesis by (simp add: makes_plus_2)
   2.564 +    qed
   2.565 +  qed
   2.566 +qed
   2.567 +
   2.568 +subsection {* Relation Between @{term valid_countings} and @{term all_countings} *}
   2.569 +
   2.570 +lemma main_nat: "(a + b) * valid_countings a b = (a - b) * all_countings a b"
   2.571 +  unfolding valid_countings all_countings ..
   2.572 +
   2.573 +lemma main_real:
   2.574 +  assumes "b < a"
   2.575 +  shows "valid_countings a b = (a - b) / (a + b) * all_countings a b"
   2.576 +using assms
   2.577 +proof -
   2.578 +  from main_nat[of a b] `b < a` have
   2.579 +    "(real a + real b) * real (valid_countings a b) = (real a - real b) * real (all_countings a b)"
   2.580 +    by (simp only: real_of_nat_add[symmetric] real_of_nat_mult[symmetric]) auto
   2.581 +  from this `b < a` show ?thesis
   2.582 +    by (subst mult_left_cancel[of "real a + real b", symmetric]) auto
   2.583 +qed
   2.584 +
   2.585 +lemma
   2.586 +  "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)"
   2.587 +proof (cases "a \<le> b")
   2.588 +  case False
   2.589 +    from this show ?thesis by (simp add: main_real)
   2.590 +next
   2.591 +  case True
   2.592 +    from this show ?thesis
   2.593 +      by (auto simp add: valid_countings_a_0 all_countings_a_0 valid_countings_eq_zero)
   2.594 +qed
   2.595 +
   2.596 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Erdoes_Szekeres.thy	Fri Jun 12 10:33:02 2015 +0200
     3.3 @@ -0,0 +1,164 @@
     3.4 +(*   Title: HOL/ex/Erdoes_Szekeres.thy
     3.5 +     Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
     3.6 +*)
     3.7 +
     3.8 +section {* The Erdoes-Szekeres Theorem *}
     3.9 +
    3.10 +theory Erdoes_Szekeres
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +subsection {* Addition to @{theory Lattices_Big} Theory *}
    3.15 +
    3.16 +lemma Max_gr:
    3.17 +  assumes "finite A"
    3.18 +  assumes "a \<in> A" "a > x"
    3.19 +  shows "x < Max A"
    3.20 +using assms Max_ge less_le_trans by blast
    3.21 +
    3.22 +subsection {* Additions to @{theory Finite_Set} Theory *}
    3.23 +
    3.24 +lemma obtain_subset_with_card_n:
    3.25 +  assumes "n \<le> card S"
    3.26 +  obtains T where "T \<subseteq> S" "card T = n"
    3.27 +proof -
    3.28 +  from assms obtain n' where "card S = n + n'" by (metis le_add_diff_inverse)
    3.29 +  from this that show ?thesis
    3.30 +  proof (induct n' arbitrary: S)
    3.31 +    case 0 from this show ?case by auto
    3.32 +  next
    3.33 +    case Suc from this show ?case by (simp add: card_Suc_eq) (metis subset_insertI2)
    3.34 +  qed
    3.35 +qed
    3.36 +
    3.37 +lemma exists_set_with_max_card:
    3.38 +  assumes "finite S" "S \<noteq> {}"
    3.39 +  shows "\<exists>s \<in> S. card s = Max (card ` S)"
    3.40 +using assms
    3.41 +proof (induct S rule: finite.induct)
    3.42 +  case (insertI S' s')
    3.43 +  show ?case
    3.44 +  proof (cases "S' \<noteq> {}")
    3.45 +    case True
    3.46 +    from this insertI.hyps(2) obtain s where s: "s \<in> S'" "card s = Max (card ` S')" by auto
    3.47 +    from this(1) have that: "(if card s \<ge> card s' then s else s') \<in> insert s' S'" by auto
    3.48 +    have "card (if card s \<ge> card s' then s else s') = Max (card ` insert s' S')"
    3.49 +      using insertI(1) `S' \<noteq> {}` s by auto
    3.50 +    from this that show ?thesis by blast
    3.51 +  qed (auto)
    3.52 +qed (auto)
    3.53 +
    3.54 +subsection {* Definition of Monotonicity over a Carrier Set *}
    3.55 +
    3.56 +definition
    3.57 +  "mono_on f R S = (\<forall>i\<in>S. \<forall>j\<in>S. i \<le> j \<longrightarrow> R (f i) (f j))"
    3.58 +
    3.59 +lemma mono_on_empty [simp]: "mono_on f R {}"
    3.60 +unfolding mono_on_def by auto
    3.61 +
    3.62 +lemma mono_on_singleton [simp]: "reflp R \<Longrightarrow> mono_on f R {x}"
    3.63 +unfolding mono_on_def reflp_def by auto
    3.64 +
    3.65 +lemma mono_on_subset: "T \<subseteq> S \<Longrightarrow> mono_on f R S \<Longrightarrow> mono_on f R T"
    3.66 +unfolding mono_on_def by (simp add: subset_iff)
    3.67 +
    3.68 +lemma not_mono_on_subset: "T \<subseteq> S \<Longrightarrow> \<not> mono_on f R T \<Longrightarrow> \<not> mono_on f R S"
    3.69 +unfolding mono_on_def by blast
    3.70 +
    3.71 +lemma [simp]:
    3.72 +  "reflp (op \<le> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
    3.73 +  "reflp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
    3.74 +  "transp (op \<le> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
    3.75 +  "transp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
    3.76 +unfolding reflp_def transp_def by auto
    3.77 +
    3.78 +subsection {* The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument *}
    3.79 +
    3.80 +lemma Erdoes_Szekeres:
    3.81 +  fixes f :: "_ \<Rightarrow> 'a::linorder"
    3.82 +  shows "(\<exists>S. S \<subseteq> {0..m * n} \<and> card S = m + 1 \<and> mono_on f (op \<le>) S) \<or>
    3.83 +         (\<exists>S. S \<subseteq> {0..m * n} \<and> card S = n + 1 \<and> mono_on f (op \<ge>) S)"
    3.84 +proof (rule ccontr)
    3.85 +  let ?max_subseq = "\<lambda>R k. Max (card ` {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S})"
    3.86 +  def phi == "\<lambda>k. (?max_subseq (op \<le>) k, ?max_subseq (op \<ge>) k)"
    3.87 +
    3.88 +  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
    3.89 +
    3.90 +  {
    3.91 +    fix R
    3.92 +    assume reflp: "reflp (R :: 'a::linorder \<Rightarrow> _)"
    3.93 +    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
    3.94 +    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
    3.95 +    from this have lower_bound: "\<And>k. k \<le> m * n \<Longrightarrow> ?max_subseq R k \<ge> 1"
    3.96 +      by (auto intro!: Max_ge)
    3.97 +
    3.98 +    fix b
    3.99 +    assume not_mono_at: "\<forall>S. S \<subseteq> {0..m * n} \<and> card S = b + 1 \<longrightarrow> \<not> mono_on f R S"
   3.100 +
   3.101 +    {
   3.102 +      fix S
   3.103 +      assume "S \<subseteq> {0..m * n}" "card S \<ge> b + 1"
   3.104 +      moreover from `card S \<ge> b + 1` obtain T where "T \<subseteq> S \<and> card T = Suc b"
   3.105 +        using obtain_subset_with_card_n by (metis Suc_eq_plus1)
   3.106 +      ultimately have "\<not> mono_on f R S" using not_mono_at by (auto dest: not_mono_on_subset)
   3.107 +    }
   3.108 +    from this have "\<forall>S. S \<subseteq> {0..m * n} \<and> mono_on f R S \<longrightarrow> card S \<le> b"
   3.109 +      by (metis Suc_eq_plus1 Suc_leI not_le)
   3.110 +    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"
   3.111 +      using order_trans by force
   3.112 +    from this non_empty have upper_bound: "\<And>k. k \<le> m * n \<Longrightarrow> ?max_subseq R k \<le> b"
   3.113 +      by (auto intro: Max.boundedI)
   3.114 +
   3.115 +    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"
   3.116 +      by auto
   3.117 +  } note bounds = this
   3.118 +
   3.119 +  assume contraposition: "\<not> ?thesis"
   3.120 +  from contraposition bounds[of "op \<le>" "m"] bounds[of "op \<ge>" "n"]
   3.121 +    have "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq (op \<le>) k \<and> ?max_subseq (op \<le>) k \<le> m"
   3.122 +    and  "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq (op \<ge>) k \<and> ?max_subseq (op \<ge>) k \<le> n"
   3.123 +    using reflp_def by simp+
   3.124 +  from this have "\<forall>i \<in> {0..m * n}. phi i \<in> {1..m} \<times> {1..n}"
   3.125 +    unfolding phi_def by auto
   3.126 +  from this have subseteq: "phi ` {0..m * n} \<subseteq> {1..m} \<times> {1..n}" by blast
   3.127 +  have card_product: "card ({1..m} \<times> {1..n}) = m * n" by (simp add: card_cartesian_product)
   3.128 +  have "finite ({1..m} \<times> {1..n})" by blast
   3.129 +  from subseteq card_product this have card_le: "card (phi ` {0..m * n}) \<le> m * n" by (metis card_mono)
   3.130 +
   3.131 +  {
   3.132 +    fix i j
   3.133 +    assume "i < (j :: nat)"
   3.134 +    {
   3.135 +      fix R
   3.136 +      assume R: "reflp (R :: 'a::linorder \<Rightarrow> _)" "transp R" "R (f i) (f j)"
   3.137 +      from one_member[OF `reflp R`, of "i"] have
   3.138 +        "\<exists>S \<in> {S. S \<subseteq> {0..i} \<and> mono_on f R S \<and> i \<in> S}. card S = ?max_subseq R i"
   3.139 +        by (intro exists_set_with_max_card) auto
   3.140 +      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
   3.141 +      from S `i < j` finite_subset have "j \<notin> S" "finite S" "insert j S \<subseteq> {0..j}" by auto
   3.142 +      from S(1) R `i < j` this have "mono_on f R (insert j S)"
   3.143 +        unfolding mono_on_def reflp_def transp_def
   3.144 +        by (metis atLeastAtMost_iff insert_iff le_antisym subsetCE)
   3.145 +      from this have d: "insert j S \<in> {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S}"
   3.146 +        using `insert j S \<subseteq> {0..j}` by blast
   3.147 +      from this `j \<notin> S` S(1) have "card (insert j S) \<in>
   3.148 +        card ` {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S} \<and> card S < card (insert j S)"
   3.149 +        by (auto intro!: imageI) (auto simp add: `finite S`)
   3.150 +      from this S(2) have "?max_subseq R i < ?max_subseq R j" by (auto intro: Max_gr)
   3.151 +    } note max_subseq_increase = this
   3.152 +    have "?max_subseq (op \<le>) i < ?max_subseq (op \<le>) j \<or> ?max_subseq (op \<ge>) i < ?max_subseq (op \<ge>) j"
   3.153 +    proof (cases "f j \<ge> f i")
   3.154 +      case True
   3.155 +      from this max_subseq_increase[of "op \<le>", simplified] show ?thesis by simp
   3.156 +    next
   3.157 +      case False
   3.158 +      from this max_subseq_increase[of "op \<ge>", simplified] show ?thesis by simp
   3.159 +    qed
   3.160 +    from this have "phi i \<noteq> phi j" using phi_def by auto
   3.161 +  }
   3.162 +  from this have "inj phi" unfolding inj_on_def by (metis less_linear)
   3.163 +  from this have card_eq: "card (phi ` {0..m * n}) = m * n + 1" by (simp add: card_image inj_on_def)
   3.164 +  from card_le card_eq show False by simp
   3.165 +qed
   3.166 +
   3.167 +end
   3.168 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/Sum_of_Powers.thy	Fri Jun 12 10:33:02 2015 +0200
     4.3 @@ -0,0 +1,215 @@
     4.4 +(*  Title:      HOL/ex/Sum_of_Powers.thy
     4.5 +    Author:     Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
     4.6 +*)
     4.7 +
     4.8 +section {* Sum of Powers *}
     4.9 +
    4.10 +theory Sum_of_Powers
    4.11 +imports Complex_Main
    4.12 +begin
    4.13 +
    4.14 +subsection {* Additions to @{theory Binomial} Theory *}
    4.15 +
    4.16 +lemma of_nat_binomial_eq_mult_binomial_Suc:
    4.17 +  assumes "k \<le> n"
    4.18 +  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)"
    4.19 +proof -
    4.20 +  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))"
    4.21 +  proof -
    4.22 +    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))"
    4.23 +      by (auto simp add: setprod.reindex)
    4.24 +    also have "... = (\<Prod>i\<le>k. of_nat (Suc n - i))"
    4.25 +    proof (cases k)
    4.26 +      case (Suc k')
    4.27 +      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))"
    4.28 +        by (subst setprod.insert) (auto simp add: lessThan_Suc_atMost)
    4.29 +      also have "... = (\<Prod>i\<le>Suc k'. of_nat (Suc n - i))" by (simp only: Iic_Suc_eq_insert_0)
    4.30 +      finally show ?thesis using Suc by simp
    4.31 +    qed (simp)
    4.32 +    also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i<k. of_nat (Suc n - i))"
    4.33 +      by (cases k) (auto simp add: atMost_Suc lessThan_Suc_atMost)
    4.34 +    also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
    4.35 +      by (simp only: Suc_eq_plus1)
    4.36 +    finally show ?thesis .
    4.37 +  qed
    4.38 +  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))"
    4.39 +    by (metis le_add2 nonzero_mult_divide_cancel_left not_one_le_zero of_nat_eq_0_iff times_divide_eq_left)
    4.40 +  from assms this show ?thesis
    4.41 +    by (auto simp add: binomial_altdef_of_nat setprod_dividef)
    4.42 +qed
    4.43 +
    4.44 +lemma real_binomial_eq_mult_binomial_Suc:
    4.45 +  assumes "k \<le> n"
    4.46 +  shows "(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)"
    4.47 +proof -
    4.48 +  have "real (n choose k) = of_nat (n choose k)" by auto
    4.49 +  also have "... = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
    4.50 +    by (simp add: assms of_nat_binomial_eq_mult_binomial_Suc)
    4.51 +  also have "... = (n + 1 - k) / (n + 1) * (Suc n choose k)"
    4.52 +    using real_of_nat_def by auto
    4.53 +  finally show ?thesis
    4.54 +    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)
    4.55 +qed
    4.56 +
    4.57 +subsection {* Preliminaries *}
    4.58 +
    4.59 +lemma integrals_eq:
    4.60 +  assumes "f 0 = g 0"
    4.61 +  assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)"
    4.62 +  shows "f x = g x"
    4.63 +proof -
    4.64 +  show "f x = g x"
    4.65 +  proof (cases "x \<noteq> 0")
    4.66 +    case True
    4.67 +    from assms DERIV_const_ratio_const[OF this, of "\<lambda>x. f x - g x" 0]
    4.68 +    show ?thesis by auto
    4.69 +  qed (simp add: assms)
    4.70 +qed
    4.71 +
    4.72 +lemma setsum_diff: "((\<Sum>i\<le>n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0"
    4.73 +by (induct n) (auto simp add: field_simps)
    4.74 +
    4.75 +declare One_nat_def [simp del]
    4.76 +
    4.77 +subsection {* Bernoulli Numbers and Bernoulli Polynomials  *}
    4.78 +
    4.79 +declare setsum.cong [fundef_cong]
    4.80 +
    4.81 +fun bernoulli :: "nat \<Rightarrow> real"
    4.82 +where
    4.83 +  "bernoulli 0 = (1::real)"
    4.84 +| "bernoulli (Suc n) =  (-1 / (n + 2)) * (\<Sum>k \<le> n. ((n + 2 choose k) * bernoulli k))"
    4.85 +
    4.86 +declare bernoulli.simps[simp del]
    4.87 +
    4.88 +definition
    4.89 +  "bernpoly n = (\<lambda>x. \<Sum>k \<le> n. (n choose k) * bernoulli k * x ^ (n - k))"
    4.90 +
    4.91 +subsection {* Basic Observations on Bernoulli Polynomials *}
    4.92 +
    4.93 +lemma bernpoly_0: "bernpoly n 0 = bernoulli n"
    4.94 +proof (cases n)
    4.95 +  case 0
    4.96 +  from this show "bernpoly n 0 = bernoulli n"
    4.97 +    unfolding bernpoly_def bernoulli.simps by auto
    4.98 +next
    4.99 +  case (Suc n')
   4.100 +  have "(\<Sum>k\<le>n'. real (Suc n' choose k) * bernoulli k * 0 ^ (Suc n' - k)) = 0"
   4.101 +    by (rule setsum.neutral) auto
   4.102 +  with Suc show ?thesis
   4.103 +    unfolding bernpoly_def by simp
   4.104 +qed
   4.105 +
   4.106 +lemma setsum_binomial_times_bernoulli:
   4.107 +  "(\<Sum>k\<le>n. ((Suc n) choose k) * bernoulli k) = (if n = 0 then 1 else 0)"
   4.108 +proof (cases n)
   4.109 +  case 0
   4.110 +  from this show ?thesis by (simp add: bernoulli.simps)
   4.111 +next
   4.112 +  case Suc
   4.113 +  from this show ?thesis
   4.114 +  by (simp add: bernoulli.simps)
   4.115 +    (simp add: field_simps add_2_eq_Suc'[symmetric] del: add_2_eq_Suc add_2_eq_Suc')
   4.116 +qed
   4.117 +
   4.118 +subsection {* Sum of Powers with Bernoulli Polynomials *}
   4.119 +
   4.120 +lemma bernpoly_derivative [derivative_intros]:
   4.121 +  "(bernpoly (Suc n) has_real_derivative ((n + 1) * bernpoly n x)) (at x)"
   4.122 +proof -
   4.123 +  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)"
   4.124 +    unfolding bernpoly_def by (rule DERIV_cong) (fast intro!: derivative_intros, simp)
   4.125 +  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"
   4.126 +    unfolding bernpoly_def
   4.127 +    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)
   4.128 +  ultimately show ?thesis by auto
   4.129 +qed
   4.130 +
   4.131 +lemma diff_bernpoly:
   4.132 +  "bernpoly n (x + 1) - bernpoly n x = n * x ^ (n - 1)"
   4.133 +proof (induct n arbitrary: x)
   4.134 +  case 0
   4.135 +  show ?case unfolding bernpoly_def by auto
   4.136 +next
   4.137 +  case (Suc n)
   4.138 +  have "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = (Suc n) * 0 ^ n"
   4.139 +    unfolding bernpoly_0 unfolding bernpoly_def by (simp add: setsum_binomial_times_bernoulli zero_power)
   4.140 +  from this have const: "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = real (Suc n) * 0 ^ n" by (simp add: power_0_left)
   4.141 +  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)"
   4.142 +    unfolding right_diff_distrib[symmetric] by (simp add: Suc.hyps One_nat_def)
   4.143 +  note [derivative_intros] = DERIV_chain'[where f = "\<lambda>x::real. x + 1" and g = "bernpoly (Suc n)" and s="UNIV"]
   4.144 +  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)"
   4.145 +    by (rule DERIV_cong) (fast intro!: derivative_intros, simp add: hyps')
   4.146 +  from integrals_eq[OF const derivative] show ?case by simp
   4.147 +qed
   4.148 +
   4.149 +lemma sum_of_powers: "(\<Sum>k\<le>n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)"
   4.150 +proof -
   4.151 +  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))"
   4.152 +    by (auto simp add: setsum_right_distrib intro!: setsum.cong)
   4.153 +  also have "... = (\<Sum>k\<le>n. bernpoly (Suc m) (real (k + 1)) - bernpoly (Suc m) (real k))"
   4.154 +    by (simp only: real_of_nat_1[symmetric] real_of_nat_add[symmetric])
   4.155 +  also have "... = bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0"
   4.156 +    by (simp only: setsum_diff[where f="\<lambda>k. bernpoly (Suc m) (real k)"]) simp
   4.157 +  finally show ?thesis by (auto simp add: field_simps intro!: eq_divide_imp)
   4.158 +qed
   4.159 +
   4.160 +subsection {* Instances for Square And Cubic Numbers *}
   4.161 +
   4.162 +lemma binomial_unroll:
   4.163 +  "n > 0 \<Longrightarrow> (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))"
   4.164 +by (cases n) (auto simp add: binomial.simps(2))
   4.165 +
   4.166 +lemma setsum_unroll:
   4.167 +  "(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
   4.168 +by auto (metis One_nat_def Suc_pred add.commute setsum_atMost_Suc)
   4.169 +
   4.170 +lemma bernoulli_unroll:
   4.171 +  "n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
   4.172 +by (cases n) (simp add: bernoulli.simps One_nat_def)+
   4.173 +
   4.174 +lemmas unroll = binomial.simps(1) binomial_unroll
   4.175 +  bernoulli.simps(1) bernoulli_unroll setsum_unroll bernpoly_def
   4.176 +
   4.177 +lemma sum_of_squares: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
   4.178 +proof -
   4.179 +  have "real (\<Sum>k\<le>n::nat. k ^ 2) = (\<Sum>k\<le>n::nat. (real k) ^ 2)" by simp
   4.180 +  also have "... = (bernpoly 3 (real (n + 1)) - bernpoly 3 0) / real (3 :: nat)"
   4.181 +    by (auto simp add: sum_of_powers)
   4.182 +  also have "... = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
   4.183 +    by (simp add: unroll algebra_simps power2_eq_square power3_eq_cube One_nat_def[symmetric])
   4.184 +  finally show ?thesis by simp
   4.185 +qed
   4.186 +
   4.187 +lemma sum_of_squares_nat: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6"
   4.188 +proof -
   4.189 +  from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
   4.190 +    by (auto simp add: field_simps)
   4.191 +  from this have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
   4.192 +    by (simp only: real_of_nat_inject[symmetric])
   4.193 +  from this show ?thesis by auto
   4.194 +qed
   4.195 +
   4.196 +lemma sum_of_cubes: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 / 4"
   4.197 +proof -
   4.198 +  have two_plus_two: "2 + 2 = 4" by simp
   4.199 +  have power4_eq: "\<And>x::real. x ^ 4 = x * x * x * x"
   4.200 +    by (simp only: two_plus_two[symmetric] power_add power2_eq_square)
   4.201 +  have "real (\<Sum>k\<le>n::nat. k ^ 3) = (\<Sum>k\<le>n::nat. (real k) ^ 3)" by simp
   4.202 +  also have "... = ((bernpoly 4 (n + 1) - bernpoly 4 0)) / (real (4 :: nat))"
   4.203 +    by (auto simp add: sum_of_powers)
   4.204 +  also have "... = ((n ^ 2 + n) / 2) ^ 2"
   4.205 +    by (simp add: unroll algebra_simps power2_eq_square power4_eq power3_eq_cube)
   4.206 +  finally show ?thesis by simp
   4.207 +qed
   4.208 +
   4.209 +lemma sum_of_cubes_nat: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
   4.210 +proof -
   4.211 +  from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
   4.212 +    by (auto simp add: field_simps)
   4.213 +  from this have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
   4.214 +    by (simp only: real_of_nat_inject[symmetric])
   4.215 +  from this show ?thesis by auto
   4.216 +qed
   4.217 +
   4.218 +end