--- a/src/HOL/Binomial.thy Fri Jun 12 10:33:02 2015 +0200
+++ b/src/HOL/Binomial.thy Tue Jun 16 11:31:22 2015 +0200
@@ -1029,4 +1029,24 @@
qed
qed
+
+lemma Suc_times_binomial_add: -- \<open>by Lukas Bulwahn\<close>
+ "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
+proof -
+ have dvd: "Suc a * (fact a * fact b) dvd fact (Suc (a + b))" for a b
+ using fact_fact_dvd_fact[of "Suc a" "b", where 'a=nat]
+ by (simp only: fact_Suc add_Suc[symmetric] of_nat_id mult.assoc)
+
+ have "Suc a * (fact (Suc (a + b)) div (Suc a * fact a * fact b)) =
+ Suc a * fact (Suc (a + b)) div (Suc a * (fact a * fact b))"
+ by (subst div_mult_swap[symmetric]; simp only: mult.assoc dvd)
+ also have "\<dots> = Suc b * fact (Suc (a + b)) div (Suc b * (fact a * fact b))"
+ by (simp only: div_mult_mult1)
+ also have "\<dots> = Suc b * (fact (Suc (a + b)) div (Suc b * (fact a * fact b)))"
+ using dvd[of b a] by (subst div_mult_swap[symmetric]; simp only: ac_simps dvd)
+ finally show ?thesis
+ by (subst (1 2) binomial_altdef_nat)
+ (simp_all only: ac_simps diff_Suc_Suc Suc_diff_le diff_add_inverse fact_Suc of_nat_id)
+qed
+
end
--- a/src/HOL/ex/Ballot.thy Fri Jun 12 10:33:02 2015 +0200
+++ b/src/HOL/ex/Ballot.thy Tue Jun 16 11:31:22 2015 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/ex/Ballot.thy
Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
+ Author: Johannes Hölzl <hoelzl@in.tum.de>
*)
section {* Bertrand's Ballot Theorem *}
@@ -12,148 +13,14 @@
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
+lemma card_bij':
+ assumes "f \<in> A \<rightarrow> B" "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
+ and "g \<in> B \<rightarrow> A" "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
+ shows "card A = card B"
+ apply (rule bij_betw_same_card)
+ apply (rule bij_betwI)
+ apply fact+
+ done
subsection {* Formalization of Problem Statement *}
@@ -162,406 +29,231 @@
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}"
+ "all_countings a b = card {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}"
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})}"
+ card {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 = A} > card {x\<in>{1..m}. f x = B})}"
+
+subsubsection {* Equivalence with Set Cardinality *}
-subsubsection {* Equivalence of Alternative Definitions *}
+lemma Collect_on_transfer:
+ assumes "rel_set R X Y"
+ shows "rel_fun (rel_fun R op =) (rel_set R) (\<lambda>P. {x\<in>X. P x}) (\<lambda>P. {y\<in>Y. P y})"
+ using assms unfolding rel_fun_def rel_set_def by fast
+
+lemma rel_fun_trans:
+ "rel_fun P Q g g' \<Longrightarrow> rel_fun R P f f' \<Longrightarrow> rel_fun R Q (\<lambda>x. g (f x)) (\<lambda>y. g' (f' y))"
+ by (auto simp: rel_fun_def)
-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 rel_fun_trans2:
+ "rel_fun P1 (rel_fun P2 Q) g g' \<Longrightarrow> rel_fun R P1 f1 f1' \<Longrightarrow> rel_fun R P2 f2 f2' \<Longrightarrow>
+ rel_fun R Q (\<lambda>x. g (f1 x) (f2 x)) (\<lambda>y. g' (f1' y) (f2' y))"
+ by (auto simp: rel_fun_def)
+
+lemma rel_fun_trans2':
+ "rel_fun R (op =) f1 f1' \<Longrightarrow> rel_fun R (op =) f2 f2' \<Longrightarrow>
+ rel_fun R (op =) (\<lambda>x. g (f1 x) (f2 x)) (\<lambda>y. g (f1' y) (f2' y))"
+ by (auto simp: rel_fun_def)
-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 rel_fun_const: "rel_fun R (op =) (\<lambda>x. a) (\<lambda>y. a)"
+ by auto
+
+lemma rel_fun_conj:
+ "rel_fun R (op =) f f' \<Longrightarrow> rel_fun R (op =) g g' \<Longrightarrow> rel_fun R (op =) (\<lambda>x. f x \<and> g x) (\<lambda>y. f' y \<and> g' y)"
+ by (auto simp: rel_fun_def)
+
+lemma rel_fun_ball:
+ "(\<And>i. i \<in> I \<Longrightarrow> rel_fun R (op =) (f i) (f' i)) \<Longrightarrow> rel_fun R (op =) (\<lambda>x. \<forall>i\<in>I. f i x) (\<lambda>y. \<forall>i\<in>I. f' i y)"
+ by (auto simp: rel_fun_def rel_set_def)
-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
+ shows all_countings_set: "all_countings a b = card {V\<in>Pow {0..<a+b}. card V = a}"
+ (is "_ = card ?A")
+ and valid_countings_set: "valid_countings a b =
+ card {V\<in>Pow {0..<a+b}. card V = a \<and> (\<forall>m\<in>{1..a+b}. card ({0..<m} \<inter> V) > m - card ({0..<m} \<inter> V))}"
+ (is "_ = card ?V")
+proof -
+ def P \<equiv> "\<lambda>j i. i < a + b \<and> j = Suc i"
+ have unique_P: "bi_unique P" and total_P: "\<And>m. m \<le> a + b \<Longrightarrow> rel_set P {1..m} {0..<m}"
+ by (auto simp add: bi_unique_def rel_set_def P_def Suc_le_eq gr0_conv_Suc)
+ have rel_fun_P: "\<And>R f g. (\<And>i. i < a+b \<Longrightarrow> R (f (Suc i)) (g i)) \<Longrightarrow> rel_fun P R f g"
+ by (simp add: rel_fun_def P_def)
+
+ def R \<equiv> "\<lambda>f V. V \<subseteq> {0..<a+b} \<and> f \<in> extensional {1..a+b} \<and> (\<forall>i<a+b. i \<in> V \<longleftrightarrow> f (Suc i) = A)"
+ { fix f g :: "nat \<Rightarrow> vote" assume "f \<in> extensional {1..a + b}" "g \<in> extensional {1..a + b}"
+ moreover assume "\<forall>i<a + b. (f (Suc i) = A) = (g (Suc i) = A)"
+ then have "\<forall>i<a + b. f (Suc i) = g (Suc i)"
+ by (metis vote.nchotomy)
+ ultimately have "f i = g i" for i
+ by (cases "i \<in> {1..a+b}") (auto simp: extensional_def Suc_le_eq gr0_conv_Suc) }
+ then have unique_R: "bi_unique R"
+ by (auto simp: bi_unique_def R_def)
-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)
+ have "f \<in> extensional {1..a + b} \<Longrightarrow> \<exists>V\<in>Pow {0..<a + b}. R f V" for f
+ by (intro bexI[of _ "{i. i < a+b \<and> f (Suc i) = A}"]) (auto simp add: R_def PiE_def)
+ moreover have "V \<in> Pow {0..<a + b} \<Longrightarrow> \<exists>f\<in>extensional {1..a+b}. R f V" for V
+ by (intro bexI[of _ "\<lambda>i\<in>{1..a+b}. if i - 1 \<in> V then A else B"]) (auto simp add: R_def PiE_def)
+ ultimately have total_R: "rel_set R (extensional {1..a+b}) (Pow {0..<a+b})"
+ by (auto simp: rel_set_def)
-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
+ have P: "rel_fun R (rel_fun P op =) (\<lambda>f x. f x = A) (\<lambda>V y. y \<in> V)"
+ by (auto simp: P_def R_def Suc_le_eq gr0_conv_Suc rel_fun_def)
+
+ have eq_B: "x = B \<longleftrightarrow> x \<noteq> A" for x
+ by (cases x; simp)
+
+ { fix f and m :: nat
+ have "card {x\<in>{1..m}. f x = B} = card ({1..m} - {x\<in>{1..m}. f x = A})"
+ by (simp add: eq_B set_diff_eq cong: conj_cong)
+ also have "\<dots> = m - card {x\<in>{1..m}. f x = A}"
+ by (subst card_Diff_subset) auto
+ finally have "card {x\<in>{1..m}. f x = B} = m - card {x\<in>{1..m}. f x = A}" . }
+ note card_B = this
-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
+ note transfers = rel_fun_const card_transfer[THEN rel_funD, OF unique_R] rel_fun_conj rel_fun_ball
+ Collect_on_transfer[THEN rel_funD, OF total_R] Collect_on_transfer[THEN rel_funD, OF total_P]
+ rel_fun_trans[OF card_transfer, OF unique_P] rel_fun_trans[OF Collect_on_transfer[OF total_P]]
+ rel_fun_trans2'[where g="op ="] rel_fun_trans2'[where g="op <"] rel_fun_trans2'[where g="op -"]
+
+ have "all_countings a b = card {f \<in> extensional {1..a + b}. card {x \<in> {1..a + b}. f x = A} = a}"
+ using card_B by (simp add: all_countings_def PiE_iff vote.nchotomy cong: conj_cong)
+ also have "\<dots> = card {V\<in>Pow {0..<a+b}. card ({x\<in>{0 ..< a + b}. x \<in> V}) = a}"
+ by (intro P order_refl transfers)
+ finally show "all_countings a b = card ?A"
+ unfolding Int_def[symmetric] by (simp add: Int_absorb1 cong: conj_cong)
+
+ have "valid_countings a b = card {f\<in>extensional {1..a+b}.
+ card {x\<in>{1..a+b}. f x = A} = a \<and> (\<forall>m\<in>{1..a+b}. card {x\<in>{1..m}. f x = A} > m - card {x\<in>{1..m}. f x = A})}"
+ using card_B by (simp add: valid_countings_def PiE_iff vote.nchotomy cong: conj_cong)
+ also have "\<dots> = card {V\<in>Pow {0..<a+b}. card {x\<in>{0..<a+b}. x\<in>V} = a \<and>
+ (\<forall>m\<in>{1..a+b}. card {x\<in>{0..<m}. x\<in>V} > m - card {x\<in>{0..<m}. x\<in>V})}"
+ by (intro P order_refl transfers) auto
+ finally show "valid_countings a b = card ?V"
+ unfolding Int_def[symmetric] by (simp add: Int_absorb1 cong: conj_cong)
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
+lemma all_countings: "all_countings a b = (a + b) choose a"
+ unfolding all_countings_set by (simp add: n_subsets)
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 card_V_eq_a: "V \<subseteq> {0..<a} \<Longrightarrow> card V = a \<longleftrightarrow> V = {0..<a}"
+ using card_subset_eq[of "{0..<a}" V] by auto
+
+lemma valid_countings_a_0: "valid_countings a 0 = 1"
+ by (simp add: valid_countings_set card_V_eq_a cong: conj_cong)
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
+ "a \<le> b \<Longrightarrow> 0 < b \<Longrightarrow> valid_countings a b = 0"
+ by (auto simp add: valid_countings_set Int_absorb1 intro!: bexI[of _ "a + b"])
-subsubsection {* Recursive Cases *}
+lemma Ico_subset_finite: "i \<subseteq> {a ..< b::nat} \<Longrightarrow> finite i"
+ by (auto dest: finite_subset)
-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 Icc_Suc2: "a \<le> b \<Longrightarrow> {a..Suc b} = insert (Suc b) {a..b}"
+ by auto
+
+lemma Ico_Suc2: "a \<le> b \<Longrightarrow> {a..<Suc b} = insert b {a..<b}"
+ by auto
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 *}
+ assumes "b < a"
+ shows "valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b"
+proof -
+ let ?l = "Suc (a + b)"
+ let ?Q = "\<lambda>V c. \<forall>m\<in>{1..c}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V)"
+ let ?V = "\<lambda>P. {V. (V \<in> Pow {0..<Suc ?l} \<and> P V) \<and> card V = Suc a \<and> ?Q V (Suc ?l)}"
+ have "valid_countings (Suc a) (Suc b) = card (?V (\<lambda>V. ?l \<notin> V)) + card (?V (\<lambda>V. ?l \<in> V))"
+ unfolding valid_countings_set
+ by (subst card_Un_disjoint[symmetric]) (auto simp add: set_eq_iff intro!: arg_cong[where f=card])
+ also have "card (?V (\<lambda>V. ?l \<in> V)) = valid_countings a (Suc b)"
+ unfolding valid_countings_set
+ proof (rule card_bij'[where f="\<lambda>V. V - {?l}" and g="insert ?l"])
+ have *: "\<And>m V. m \<in> {1..a + Suc b} \<Longrightarrow> {0..<m} \<inter> (V - {?l}) = {0..<m} \<inter> V"
+ by auto
+ show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}"
+ by (auto simp: Ico_subset_finite *)
+ { fix V assume "V \<subseteq> {0..<?l}"
+ moreover then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
+ by (auto dest: finite_subset)
+ ultimately have "card (insert ?l V) = Suc (card V)"
+ "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))"
+ if "m \<le> Suc ?l" for m
+ using that by auto }
+ then show "insert ?l \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)} \<rightarrow> ?V (\<lambda>V. ?l \<in> V)"
+ using `b < a` by auto
+ qed auto
+ also have "card (?V (\<lambda>V. ?l \<notin> V)) = valid_countings (Suc a) b"
+ unfolding valid_countings_set
+ proof (intro arg_cong[where f="\<lambda>P. card {x. P x}"] ext conj_cong)
+ fix V assume "V \<in> Pow {0..<Suc a + b}" and [simp]: "card V = Suc a"
+ then have [simp]: "V \<subseteq> {0..<Suc ?l}"
+ by auto
+ show "?Q V (Suc ?l) = ?Q V (Suc a + b)"
+ using `b<a` by (simp add: Int_absorb1 Icc_Suc2)
+ qed (auto simp: subset_eq less_Suc_eq)
+ finally show ?thesis
+ by simp
+qed
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)
+proof (induct a arbitrary: b)
+ case 0 show ?case
+ by (cases b) (simp_all add: valid_countings_eq_zero)
next
- case (2 a)
- note a_hyp = "2.hyps"
+ case (Suc a) note Suc_a = this
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"
+ proof (induct b)
+ case (Suc b) note Suc_b = this
show ?case
- proof(cases "a <= b")
- case True
- from this show ?thesis
- unfolding valid_countings_Suc_Suc if_True by (simp add: algebra_simps)
+ proof cases
+ assume "a \<le> b" then show ?thesis
+ by (simp add: valid_countings_eq_zero)
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)
+ assume "\<not> a \<le> b"
+ then have "b < a" by simp
+
+ have "Suc a * (a - Suc b) + (Suc a - b) * Suc b =
+ (Suc a * a - Suc a * Suc b) + (Suc a * Suc b - Suc b * b)"
+ by (simp add: sign_simps)
+ also have "\<dots> = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b"
+ using `b<a` by (intro add_diff_assoc2 mult_mono) auto
+ also have "\<dots> = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b"
+ using `b<a` by (intro arg_cong2[where f="op -"] add_diff_assoc mult_mono) auto
+ also have "\<dots> = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))"
+ by (simp add: sign_simps)
+ finally have rearrange: "Suc a * (a - Suc b) + (Suc a - b) * Suc b = (Suc a - Suc b) * Suc (a + b)"
+ unfolding diff_mult_distrib by simp
+
+ have "(Suc a * Suc (a + b)) * ((Suc a + Suc b) * valid_countings (Suc a) (Suc b)) =
+ (Suc a + Suc b) * Suc a * ((a + Suc b) * valid_countings a (Suc b) + (Suc a + b) * valid_countings (Suc a) b)"
+ unfolding valid_countings_Suc_Suc[OF `b < a`] by (simp add: field_simps)
+ also have "... = (Suc a + Suc b) * ((a - Suc b) * (Suc a * (Suc (a + b) choose a)) +
+ (Suc a - b) * (Suc a * (Suc (a + b) choose Suc a)))"
+ unfolding Suc_a Suc_b by (simp add: field_simps)
+ also have "... = (Suc a * (a - Suc b) + (Suc a - b) * Suc b) * (Suc (Suc a + b) * (Suc a + b choose a))"
+ unfolding Suc_times_binomial_add by (simp add: field_simps)
+ also have "... = Suc a * (Suc a * (a - Suc b) + (Suc a - b) * Suc b) * (Suc a + Suc b choose Suc a)"
+ unfolding Suc_times_binomial_eq by (simp add: field_simps)
+ also have "... = (Suc a * Suc (a + b)) * ((Suc a - Suc b) * (Suc a + Suc b choose Suc a))"
+ unfolding rearrange by (simp only: mult_ac)
+ finally show ?thesis
+ unfolding mult_cancel1 by simp
qed
- qed
+ qed (simp add: valid_countings_a_0)
qed
+lemma valid_countings_eq[code]:
+ "valid_countings a b = (if a + b = 0 then 1 else ((a - b) * ((a + b) choose a)) div (a + b))"
+ by (simp add: valid_countings[symmetric] valid_countings_a_0)
+
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"
@@ -587,7 +279,32 @@
next
case True
from this show ?thesis
- by (auto simp add: valid_countings_a_0 all_countings_a_0 valid_countings_eq_zero)
+ by (auto simp add: valid_countings_a_0 all_countings valid_countings_eq_zero)
qed
+subsubsection {* Executable Definition *}
+
+declare all_countings_def [code del]
+declare all_countings[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 {* Executable Definition *}
+
+declare valid_countings_def [code del]
+
+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"
+
end