# HG changeset patch # User nipkow # Date 1540555919 -7200 # Node ID 2c4bf4d84de52e12aab64b9fb3077b2827e908a9 # Parent 278b09a92ed6f05a559beb1493bd76284c49f83f more combinatorics lemmas diff -r 278b09a92ed6 -r 2c4bf4d84de5 src/HOL/Data_Structures/Braun_Tree.thy --- a/src/HOL/Data_Structures/Braun_Tree.thy Thu Oct 25 23:44:07 2018 +0200 +++ b/src/HOL/Data_Structures/Braun_Tree.thy Fri Oct 26 14:11:59 2018 +0200 @@ -7,7 +7,7 @@ begin text \Braun Trees were studied by Braun and Rem~\cite{BraunRem} -and later Hoogerwoord~\cite{Hoogerwoord} who gave them their name.\ +and later Hoogerwoord~\cite{Hoogerwoord}.\ fun braun :: "'a tree \ bool" where "braun Leaf = True" | @@ -51,4 +51,199 @@ qed qed +subsection \Numbering Nodes\ + +text \We show that a tree is a Braun tree iff a parity-based +numbering (\braun_indices\) of nodes yields an interval of numbers.\ + +abbreviation double :: "nat \ nat" where +"double \ (*) 2" + +abbreviation double1 :: "nat \ nat" where +"double1 \ \n. Suc(2*n)" + +fun braun_indices :: "'a tree \ nat set" where +"braun_indices Leaf = {}" | +"braun_indices (Node l _ r) = {1} \ double ` braun_indices l \ double1 ` braun_indices r" + +lemma braun_indices_if_braun: "braun t \ braun_indices t = {1..size t}" +proof(induction t) + case Leaf thus ?case by simp +next + have *: "double ` {a..b} \ double1 ` {a..b} = {2*a..2*b+1}" (is "?l = ?r") for a b + proof + show "?l \ ?r" by auto + next + have "\x2\{a..b}. x \ {Suc (2*x2), 2*x2}" if *: "x \ {2*a .. 2*b+1}" for x + proof - + have "x div 2 \ {a..b}" using * by auto + moreover have "x \ {2 * (x div 2), Suc(2 * (x div 2))}" by auto + ultimately show ?thesis by blast + qed + thus "?r \ ?l" by fastforce + qed + case (Node l x r) + hence "size l = size r \ size l = size r + 1" (is "?A \ ?B") by auto + thus ?case + proof + assume ?A + with Node show ?thesis by (auto simp: *) + next + assume ?B + with Node show ?thesis by (auto simp: * atLeastAtMostSuc_conv) + qed +qed + +text \How many even/odd natural numbers are there between m and n?\ + +lemma card_atLeastAtMost_even: + "card {i \ {m..n::nat}. even i} = (n+1-m + (m+1) mod 2) div 2" (is "?l m n = ?r m n") +proof(induction "n+1 - m" arbitrary: n m) + case 0 thus ?case by simp +next + case Suc + have "m \ n" using Suc(2) by arith + hence "{m..n} = insert m {m+1..n}" by auto + hence "?l m n = card {i \ insert m {m+1..n}. even i}" by simp + also have "\ = ?r m n" (is "?l = ?r") + proof (cases) + assume "even m" + hence "{i \ insert m {m+1..n}. even i} = insert m {i \ {m+1..n}. even i}" by auto + hence "?l = card {i \ {m+1..n}. even i} + 1" by simp + also have "\ = (n-m + (m+2) mod 2) div 2 + 1" using Suc(1)[of n "m+1"] Suc(2) by simp + also have "\ = ?r" using \even m\ \m \ n\ by auto + finally show ?thesis . + next + assume "odd m" + hence "{i \ insert m {m+1..n}. even i} = {i \ {m+1..n}. even i}" by auto + hence "?l = card ..." by simp + also have "\ = (n-m + (m+2) mod 2) div 2" using Suc(1)[of n "m+1"] Suc(2) by simp + also have "\ = ?r" using \odd m\ \m \ n\ even_iff_mod_2_eq_zero[of m] by simp + finally show ?thesis . + qed + finally show ?case . +qed + +lemma card_atLeastAtMost_odd: "card {i \ {m..n::nat}. odd i} = (n+1-m + m mod 2) div 2" +proof - + let ?A = "{i \ {m..n}. odd i}" + let ?B = "{i \ {m+1..n+1}. even i}" + have "card ?A = card (Suc ` ?A)" by (simp add: card_image) + also have "Suc ` ?A = ?B" using Suc_le_D by(force simp: image_iff) + also have "card ?B = (n+1-m + (m) mod 2) div 2" + using card_atLeastAtMost_even[of "m+1" "n+1"] by simp + finally show ?thesis . +qed + +lemma mod2_iff: "x mod 2 = (if even x then 0 else 1)" +by (simp add: odd_iff_mod_2_eq_one) + +lemma compact_ivl_even: assumes "A = {i \ {m..n}. even i}" +shows "A = (\j. 2*(j-1) + m + m mod 2) ` {1..card A}" (is "_ = ?A") +proof + let ?a = "(n+1-m + (m+1) mod 2) div 2" + have "\j \ {1..?a}. i = 2*(j-1) + m + m mod 2" if *: "i \ {m..n}" "even i" for i + proof - + let ?j = "(i - (m + m mod 2)) div 2 + 1" + have "?j \ {1..?a} \ i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_iff) presburger+ + thus ?thesis by blast + qed + thus "A \ ?A" using assms + by(auto simp: image_iff card_atLeastAtMost_even simp del: atLeastAtMost_iff) +next + let ?a = "(n+1-m + (m+1) mod 2) div 2" + have 1: "2 * (j - 1) + m + m mod 2 \ {m..n}" if *: "j \ {1..?a}" for j + using * by(auto simp: mod2_iff) + have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger + show "?A \ A" + apply(simp add: assms card_atLeastAtMost_even del: atLeastAtMost_iff One_nat_def) + using 1 2 by blast +qed + +lemma compact_ivl_odd: + assumes "B = {i \ {m..n}. odd i}" shows "B = (\i. 2*(i-1) + m + (m+1) mod 2) ` {1..card B}" +proof - + define A :: " nat set" where "A = Suc ` B" + have "A = {i \ {m+1..n+1}. even i}" + using Suc_le_D by(force simp add: A_def assms image_iff) + from compact_ivl_even[OF this] + have "A = Suc ` (\i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}" + by (simp add: image_comp o_def) + hence B: "B = (\i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}" + using A_def by (simp add: inj_image_eq_iff) + have "card A = card B" by (metis A_def bij_betw_Suc bij_betw_same_card) + with B show ?thesis by simp +qed + +lemma even_odd_decomp: assumes "\x \ A. even x" "\x \ B. odd x" "A \ B = {m..n}" +shows "(let a = card A; b = card B in + a + b = n+1-m \ + A = (\i. 2*(i-1) + m + m mod 2) ` {1..a} \ + B = (\i. 2*(i-1) + m + (m+1) mod 2) ` {1..b} \ + (a = b \ a = b+1 \ even m \ a+1 = b \ odd m))" +proof - + let ?a = "card A" let ?b = "card B" + have "finite A \ finite B" + by (metis \A \ B = {m..n}\ finite_Un finite_atLeastAtMost) + hence ab: "?a + ?b = Suc n - m" + by (metis Int_emptyI assms card_Un_disjoint card_atLeastAtMost) + have A: "A = {i \ {m..n}. even i}" using assms by auto + hence A': "A = (\i. 2*(i-1) + m + m mod 2) ` {1..?a}" by(rule compact_ivl_even) + have B: "B = {i \ {m..n}. odd i}" using assms by auto + hence B': "B = (\i. 2*(i-1) + m + (m+1) mod 2) ` {1..?b}" by(rule compact_ivl_odd) + have "?a = ?b \ ?a = ?b+1 \ even m \ ?a+1 = ?b \ odd m" + apply(simp add: Let_def mod2_iff + card_atLeastAtMost_even[of m n, simplified A[symmetric]] + card_atLeastAtMost_odd[of m n, simplified B[symmetric]] split!: if_splits) + by linarith + with ab A' B' show ?thesis by simp +qed + +lemma braun_indices1: "i \ braun_indices t \ i \ 1" +by (induction t arbitrary: i) auto + +lemma finite_braun_indices: "finite(braun_indices t)" +by (induction t) auto + +lemma evens_odds_disj: "double ` braun_indices A \ double1 ` B = {}" +using double_not_eq_Suc_double by auto + +lemma card_braun_indices: "card (braun_indices t) = size t" +proof (induction t) + case Leaf thus ?case by simp +next + case Node + thus ?case + by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint + card_insert_if evens_odds_disj card_image inj_on_def dest: braun_indices1) +qed + +lemma eq: "insert (Suc 0) M = {Suc 0..n} \ Suc 0 \ M \ M = {2..n}" +by (metis Suc_n_not_le_n atLeastAtMost_iff atLeastAtMost_insertL insertI1 insert_ident numeral_2_eq_2) + +lemma inj_on_Suc: "inj_on f N \ inj_on (\n. Suc(f n)) N" +by (simp add: inj_on_def) + +lemma braun_if_braun_indices: "braun_indices t = {1..size t} \ braun t" +proof(induction t) +case Leaf + then show ?case by simp +next + case (Node t1 x2 t2) + have 1: "i > 0 \ Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps) + have 2: "i > 0 \ 2 * (i - Suc 0) + 3 = 2*i + 1" for i::nat by(simp add: algebra_simps) + have 3: "double ` braun_indices t1 \ double1 ` braun_indices t2 = + {2..size t1 + size t2 + 1}" using Node.prems braun_indices1[of 0 t2] + apply simp + apply(drule eq) + apply auto + done + thus ?case using Node.IH even_odd_decomp[OF _ _ 3] + by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff + cong: image_cong_strong) +qed + +lemma braun_iff_braun_indices: "braun t \ braun_indices t = {1..size t}" +using braun_if_braun_indices braun_indices_if_braun by blast + end \ No newline at end of file