(*<*) theory sol11 imports "../../../Public/Thys/Heap_Prelim" begin (*>*) text {* \ExerciseSheet{11}{7.~7.~2017} *} (****** Note: This lists the solution of the original exercise question, which I modified on the fly during the tutorial. The solutions that were elaborated during the tutorial are available as tut11.thy. *) text \ \Exercise{Sparse Binary Numbers} Implement operations carry, inc, and add on sparse binary numbers, analogously to the operations link, ins, and meld on binomial heaps. Show that the operations have logarithmic worst-case complexity. \ type_synonym rank = nat type_synonym snat = "rank list" abbreviation invar :: "snat \ bool" where "invar s \ strictly_ascending s" definition \ :: "snat \ nat" where "\ s = (\i\s. 2^i)" (*<*) lemma \_Nil[simp]: "\ [] = 0" unfolding \_def by auto lemma \_Cons[simp]: "\ (r#rs) = 2^r + \ rs" unfolding \_def by auto lemma \_append[simp]: "\ (rs\<^sub>1@rs\<^sub>2) = \ rs\<^sub>1 + \ rs\<^sub>2" unfolding \_def by auto (*>*) fun carry :: "rank \ snat \ snat" (*<*) where "carry r [] = [r]" | "carry r (r'#rest) = (if r*) lemma carry_invar[simp]: (*<*) assumes "invar rs" shows "invar (carry r rs)" using assms by (induction r rs rule: carry.induct) auto (*>*) lemma carry_\: (*<*) assumes "invar rs" assumes "\r'\set rs. r\r'" shows "\ (carry r rs) = 2^r + \ rs" using assms by (induction r rs rule: carry.induct) force+ (*>*) (*<*) lemma carry_rank_bound: assumes "r' \ set (carry r rs)" assumes "\r'\set rs. r\<^sub>0 < r'" assumes "r\<^sub>0 < r" shows "r\<^sub>0 < r'" using assms by (induction r rs rule: carry.induct) (auto split: if_splits) (*>*) definition inc :: "snat \ snat" (*<*) where "inc rs = carry 0 rs" (*>*) lemma inc_invar[simp]: "invar rs \ invar (inc rs)" (*<*) unfolding inc_def by auto (*>*) lemma inc_\[simp]: "invar rs \ \ (inc rs) = Suc (\ rs)" (*<*) unfolding inc_def by (auto simp: carry_\) (*>*) fun add :: "snat \ snat \ snat" (*<*) where "add rs [] = rs" | "add [] rs = rs" | "add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = ( if r\<^sub>1 < r\<^sub>2 then r\<^sub>1#add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2) else if r\<^sub>21 then r\<^sub>2#add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2 else carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) )" (*>*) (*<*) lemma add_rank_bound: assumes "r' \ set (add rs\<^sub>1 rs\<^sub>2)" assumes "\r'\set rs\<^sub>1. r < r'" assumes "\r'\set rs\<^sub>2. r < r'" shows "r < r'" using assms apply (induction rs\<^sub>1 rs\<^sub>2 arbitrary: r' rule: add.induct) apply (auto split: if_splits simp: carry_rank_bound) done (*>*) lemma add_invar[simp]: assumes "invar rs\<^sub>1" assumes "invar rs\<^sub>2" shows "invar (add rs\<^sub>1 rs\<^sub>2)" (*<*) using assms proof (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct) case (3 r\<^sub>1 rs\<^sub>1 r\<^sub>2 rs\<^sub>2) consider (LT) "r\<^sub>1 < r\<^sub>2" | (GT) "r\<^sub>1 > r\<^sub>2" | (EQ) "r\<^sub>1 = r\<^sub>2" using antisym_conv3 by blast then show ?case proof cases case LT then show ?thesis using 3 by (force elim!: add_rank_bound) next case GT then show ?thesis using 3 by (force elim!: add_rank_bound) next case [simp]: EQ from "3.IH"(3) "3.prems" have [simp]: "invar (add rs\<^sub>1 rs\<^sub>2)" by auto have "r\<^sub>2 < r'" if "r' \ set (add rs\<^sub>1 rs\<^sub>2)" for r' using that apply (rule add_rank_bound) using "3.prems" by auto with EQ show ?thesis by auto qed qed simp_all (*>*) lemma add_\[simp]: assumes "invar rs\<^sub>1" assumes "invar rs\<^sub>2" shows "\ (add rs\<^sub>1 rs\<^sub>2) = \ rs\<^sub>1 + \ rs\<^sub>2" (*<*) using assms apply (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct) apply (auto simp: carry_\ Suc_leI add_rank_bound) done (*>*) lemma size_snat: assumes "invar rs" shows "2^length rs \ \ rs + 1" (*<*) proof - have "(2::nat)^length rs = (\i\{0..invar rs\, of "op ^ (2::nat)"] finally show "2 ^ length rs \ \ rs + 1" unfolding \_def by auto qed (*>*) fun t_carry :: "rank \ snat \ nat" (*<*) where "t_carry r [] = 1" | "t_carry r (r'#rest) = (if r*) definition t_inc :: "snat \ nat" (*<*) where "t_inc rs = t_carry 0 rs" (*>*) lemma t_inc_bound: assumes "invar rs" shows "t_inc rs \ log 2 (\ rs + 1) + 1" (*<*) proof - have "t_carry r rs \ length rs + 1" for r by (induction r rs rule: t_carry.induct) auto hence "t_inc rs \ length rs + 1" unfolding t_inc_def by auto hence "(2::nat)^t_inc rs \ 2^(length rs + 1)" by (rule power_increasing) auto also have "\ \ 2*(\ rs + 1)" using size_snat[OF \invar rs\] by auto finally have "2 ^ t_inc rs \ 2 * (\ rs + 1)" . from le_log2_of_power[OF this] show ?thesis by (simp only: log_mult of_nat_mult) auto qed (*>*) fun t_add :: "snat \ snat \ nat" (*<*) where "t_add rs [] = 1" | "t_add [] rs = 1" | "t_add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = 1 + ( if r\<^sub>1 < r\<^sub>2 then t_add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2) else if r\<^sub>21 then t_add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2 else t_carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2 )" (*>*) (*<*) lemma l_carry_estimate: "t_carry r rs + length (carry r rs) = 2 + length rs" by (induction r rs rule: carry.induct) auto lemma l_add_estimate: "length (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2 \ 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1" apply (induction rs\<^sub>1 rs\<^sub>2 rule: t_add.induct) apply (auto simp: l_carry_estimate algebra_simps) done (*>*) lemma t_add_bound: fixes rs\<^sub>1 rs\<^sub>2 defines "n\<^sub>1 \ \ rs\<^sub>1" defines "n\<^sub>2 \ \ rs\<^sub>2" assumes INVARS: "invar rs\<^sub>1" "invar rs\<^sub>2" shows "t_add rs\<^sub>1 rs\<^sub>2 \ 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2" (*<*) proof - define n where "n = n\<^sub>1 + n\<^sub>2" from l_add_estimate[of rs\<^sub>1 rs\<^sub>2] have "t_add rs\<^sub>1 rs\<^sub>2 \ 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1" by auto hence "(2::nat)^t_add rs\<^sub>1 rs\<^sub>2 \ 2^(2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1)" by (rule power_increasing) auto also have "\ = 2*(2^length rs\<^sub>1)\<^sup>2*(2^length rs\<^sub>2)\<^sup>2" by (auto simp: algebra_simps power_add power_mult) also note INVARS(1)[THEN size_snat] also note INVARS(2)[THEN size_snat] finally have "2 ^ t_add rs\<^sub>1 rs\<^sub>2 \ 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2" by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def) from le_log2_of_power[OF this] have "t_add rs\<^sub>1 rs\<^sub>2 \ log 2 \" by simp also have "\ = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)" by (simp add: log_mult log_nat_power) also have "n\<^sub>2 \ n" by (auto simp: n_def) finally have "t_add rs\<^sub>1 rs\<^sub>2 \ log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)" by auto also have "n\<^sub>1 \ n" by (auto simp: n_def) finally have "t_add rs\<^sub>1 rs\<^sub>2 \ log 2 2 + 4*log 2 (n + 1)" by auto also have "log 2 2 \ 2" by auto finally have "t_add rs\<^sub>1 rs\<^sub>2 \ 4*log 2 (n + 1) + 2" by auto thus ?thesis unfolding n_def by (auto simp: algebra_simps) qed (*>*) (*<*) end (*>*)