diff -r f6360c0c531b -r 3529946fca19 src/HOL/Data_Structures/Braun_Tree.thy --- a/src/HOL/Data_Structures/Braun_Tree.thy Tue Mar 18 21:39:42 2025 +0000 +++ b/src/HOL/Data_Structures/Braun_Tree.thy Wed Mar 19 22:18:52 2025 +0000 @@ -3,19 +3,19 @@ section \Braun Trees\ theory Braun_Tree -imports "HOL-Library.Tree_Real" + imports "HOL-Library.Tree_Real" begin text \Braun Trees were studied by Braun and Rem~\<^cite>\"BraunRem"\ and later Hoogerwoord~\<^cite>\"Hoogerwoord"\.\ fun braun :: "'a tree \ bool" where -"braun Leaf = True" | -"braun (Node l x r) = ((size l = size r \ size l = size r + 1) \ braun l \ braun r)" + "braun Leaf = True" | + "braun (Node l x r) = ((size l = size r \ size l = size r + 1) \ braun l \ braun r)" lemma braun_Node': "braun (Node l x r) = (size r \ size l \ size l \ size r + 1 \ braun l \ braun r)" -by auto + by auto text \The shape of a Braun-tree is uniquely determined by its size:\ @@ -45,14 +45,14 @@ numbering (\braun_indices\) of nodes yields an interval of numbers.\ fun braun_indices :: "'a tree \ nat set" where -"braun_indices Leaf = {}" | -"braun_indices (Node l _ r) = {1} \ (*) 2 ` braun_indices l \ Suc ` (*) 2 ` braun_indices r" + "braun_indices Leaf = {}" | + "braun_indices (Node l _ r) = {1} \ (*) 2 ` braun_indices l \ Suc ` (*) 2 ` braun_indices r" lemma braun_indices1: "0 \ braun_indices t" -by (induction t) auto + by (induction t) auto lemma finite_braun_indices: "finite(braun_indices t)" -by (induction t) auto + by (induction t) auto text "One direction:" @@ -87,7 +87,7 @@ text "The other direction is more complicated. The following proof is due to Thomas Sewell." lemma disj_evens_odds: "(*) 2 ` A \ Suc ` (*) 2 ` B = {}" -using double_not_eq_Suc_double by auto + using double_not_eq_Suc_double by auto lemma card_braun_indices: "card (braun_indices t) = size t" proof (induction t) @@ -96,7 +96,7 @@ case Node thus ?case by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint - card_insert_if disj_evens_odds card_image inj_on_def braun_indices1) + card_insert_if disj_evens_odds card_image inj_on_def braun_indices1) qed lemma braun_indices_intvl_base_1: @@ -120,19 +120,20 @@ fixes S :: "nat set" assumes "S = {m..n} \ {i. even i}" shows "\m' n'. S = (\i. i * 2) ` {m'..n'}" - apply (rule exI[where x="Suc m div 2"], rule exI[where x="n div 2"]) - apply (fastforce simp add: assms mult.commute) - done +proof - + have "S = (\i. i * 2) ` {Suc m div 2..n div 2}" + by (fastforce simp add: assms mult.commute) + then show ?thesis + by blast +qed lemma odd_of_intvl_intvl: fixes S :: "nat set" assumes "S = {m..n} \ {i. odd i}" shows "\m' n'. S = Suc ` (\i. i * 2) ` {m'..n'}" proof - - have step1: "\m'. S = Suc ` ({m'..n - 1} \ {i. even i})" - apply (rule_tac x="if n = 0 then 1 else m - 1" in exI) - apply (auto simp: assms image_def elim!: oddE) - done + have "S = Suc ` ({if n = 0 then 1 else m - 1..n - 1} \ Collect even)" + by (auto simp: assms image_def elim!: oddE) thus ?thesis by (metis even_of_intvl_intvl) qed @@ -148,186 +149,35 @@ lemma braun_if_braun_indices: "braun_indices t = {1..size t} \ braun t" proof(induction t) -case Leaf + case Leaf then show ?case by simp next case (Node l x r) obtain t where t: "t = Node l x r" by simp - from Node.prems have eq: "{2 .. size t} = (\i. i * 2) ` braun_indices l \ Suc ` (\i. i * 2) ` braun_indices r" + then have "insert (Suc 0) ((*) 2 ` braun_indices l \ Suc ` (*) 2 ` braun_indices r) \ {2..} + = {Suc 0..Suc (size l + size r)} \ {2..}" + by (metis Node.prems One_nat_def Suc_eq_plus1 Un_insert_left braun_indices.simps(2) + sup_bot_left tree.size(4)) + then have eq: "{2 .. size t} = (\i. i * 2) ` braun_indices l \ Suc ` (\i. i * 2) ` braun_indices r" (is "?R = ?S \ ?T") - apply clarsimp - apply (drule_tac f="\S. S \ {2..}" in arg_cong) - apply (simp add: t mult.commute Int_Un_distrib2 image_int_eq_image braun_indices1_le) - done + by (simp add: t mult.commute Int_Un_distrib2 image_int_eq_image braun_indices1_le) then have ST: "?S = ?R \ {i. even i}" "?T = ?R \ {i. odd i}" by (simp_all add: Int_Un_distrib2 image_int_eq_image) from ST have l: "braun_indices l = {1 .. size l}" by (fastforce dest: braun_indices_intvl_base_1 dest!: even_of_intvl_intvl - simp: mult.commute inj_image_eq_iff[OF inj_onI]) + simp: mult.commute inj_image_eq_iff[OF inj_onI]) from ST have r: "braun_indices r = {1 .. size r}" by (fastforce dest: braun_indices_intvl_base_1 dest!: odd_of_intvl_intvl - simp: mult.commute inj_image_eq_iff[OF inj_onI]) + simp: mult.commute inj_image_eq_iff[OF inj_onI]) note STa = ST[THEN eqset_imp_iff, THEN iffD2] note STb = STa[of "size t"] STa[of "size t - 1"] - then have sizes: "size l = size r \ size l = size r + 1" - apply (clarsimp simp: t l r inj_image_mem_iff[OF inj_onI]) - apply (cases "even (size l)"; cases "even (size r)"; clarsimp elim!: oddE; fastforce) - done - from l r sizes show ?case + then have "size l = size r \ size l = size r + 1" + using t l r by atomize auto + with l r show ?case by (clarsimp simp: Node.IH) 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 - -(* An older less appealing proof: -lemma Suc0_notin_double: "Suc 0 \ ( * ) 2 ` A" -by(auto) - -lemma zero_in_double_iff: "(0::nat) \ ( * ) 2 ` A \ 0 \ A" -by(auto) - -lemma Suc_in_Suc_image_iff: "Suc n \ Suc ` A \ n \ A" -by(auto) - -lemmas nat_in_image = Suc0_notin_double zero_in_double_iff Suc_in_Suc_image_iff - -lemma disj_union_eq_iff: - "\ L1 \ R2 = {}; L2 \ R1 = {} \ \ L1 \ R1 = L2 \ R2 \ L1 = L2 \ R1 = R2" -by blast - -lemma inj_braun_indices: "braun_indices t1 = braun_indices t2 \ t1 = (t2::unit tree)" -proof(induction t1 arbitrary: t2) - case Leaf thus ?case using braun_indices.elims by blast -next - case (Node l1 x1 r1) - have "t2 \ Leaf" - proof - assume "t2 = Leaf" - with Node.prems show False by simp - qed - thus ?case using Node - by (auto simp: neq_Leaf_iff insert_ident nat_in_image braun_indices1 - disj_union_eq_iff disj_evens_odds inj_image_eq_iff inj_def) -qed - -text \How many even/odd natural numbers are there between m and n?\ - -lemma card_Icc_even_nat: - "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_Icc_odd_nat: "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_Icc_even_nat[of "m+1" "n+1"] by simp - finally show ?thesis . -qed - -lemma compact_Icc_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_eq_if) presburger+ - thus ?thesis by blast - qed - thus "A \ ?A" using assms - by(auto simp: image_iff card_Icc_even_nat 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_eq_if) - have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger - show "?A \ A" - apply(simp add: assms card_Icc_even_nat del: atLeastAtMost_iff One_nat_def) - using 1 2 by blast -qed - -lemma compact_Icc_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_Icc_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_Icc_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_Icc_odd) - have "?a = ?b \ ?a = ?b+1 \ even m \ ?a+1 = ?b \ odd m" - apply(simp add: Let_def mod2_eq_if - card_Icc_even_nat[of m n, simplified A[symmetric]] - card_Icc_odd_nat[of m n, simplified B[symmetric]] split!: if_splits) - by linarith - with ab A' B' show ?thesis by simp -qed - -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: "( * ) 2 ` braun_indices t1 \ Suc ` ( * ) 2 ` braun_indices t2 = - {2..size t1 + size t2 + 1}" using Node.prems - by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1) - 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 image_comp - cong: image_cong_simp) -qed -*) + using braun_if_braun_indices braun_indices_if_braun by blast end \ No newline at end of file