Thys/Sparse_Binary_Numbers.thy
 author nipkow Mon, 31 Jul 2017 14:30:33 +0200 changeset 69882 f6d14918f41b parent 69813 d7b714476f3f permissions -rw-r--r--
.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 69813 d7b714476f3f Revived exercises lammich parents: diff changeset ` 1` ```section \Sparse Binary Numbers\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 2` ```theory Sparse_Binary_Numbers ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 3` ```imports Heap_Prelim ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 4` ```begin ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 5` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 6` ```(* ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 7` ``` Material for exercise: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 8` ``` Provide the definitions, let students prove the lemmas. ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 9` ``` Give a hint that they are analogous to binomial heap! ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 10` d7b714476f3f Revived exercises lammich parents: diff changeset ` 11` ```*) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 12` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 13` ```text \ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 14` ``` We implement sparse binary numbers over ranks, ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 15` ``` converting from the weight-based presentation of Okasaki. ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 16` ```\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 17` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 18` ```(* TODO: borrow, decrement, sub *) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 19` ```subsection \Datatype Definition\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 20` ```type_synonym rank = nat ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 21` ```type_synonym snat = "rank list" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 22` d7b714476f3f Revived exercises lammich parents: diff changeset ` 23` ```subsubsection \Invariants\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 24` ```abbreviation invar :: "snat \ bool" where "invar s \ strictly_ascending s" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 25` ```definition \ :: "snat \ nat" where "\ s = (\i\s. 2^i)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 26` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 27` ```lemma \_Nil[simp]: "\ [] = 0" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 28` ``` unfolding \_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 29` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 30` ```lemma \_Cons[simp]: "\ (r#rs) = 2^r + \ rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 31` ``` unfolding \_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 32` d7b714476f3f Revived exercises lammich parents: diff changeset ` 33` ```lemma \_append[simp]: "\ (rs\<^sub>1@rs\<^sub>2) = \ rs\<^sub>1 + \ rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 34` ``` unfolding \_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 35` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 36` ```subsection \Operations\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 37` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 38` ```fun carry :: "rank \ snat \ snat" where ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 39` ``` "carry r [] = [r]" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 40` ```| "carry r (r'#rest) = (if r parents: diff changeset ` 41` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 42` ```lemma carry_invar[simp]: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 43` ``` assumes "invar rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 44` ``` shows "invar (carry r rs)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 45` ``` using assms by (induction r rs rule: carry.induct) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 46` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 47` ```lemma carry_\: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 48` ``` assumes "invar rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 49` ``` assumes "\r'\set rs. r\r'" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 50` ``` shows "\ (carry r rs) = 2^r + \ rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 51` ``` using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 52` ``` by (induction r rs rule: carry.induct) force+ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 53` d7b714476f3f Revived exercises lammich parents: diff changeset ` 54` ```lemma carry_rank_bound: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 55` ``` assumes "r' \ set (carry r rs)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 56` ``` assumes "\r'\set rs. r\<^sub>0 < r'" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 57` ``` assumes "r\<^sub>0 < r" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 58` ``` shows "r\<^sub>0 < r'" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 59` ``` using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 60` ``` by (induction r rs rule: carry.induct) (auto split: if_splits) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 61` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 62` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 63` ```definition "inc rs = carry 0 rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 64` ```lemma inc_invar[simp]: "invar rs \ invar (inc rs)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 65` ``` unfolding inc_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 66` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 67` ```lemma inc_\[simp]: "invar rs \ \ (inc rs) = Suc (\ rs)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 68` ``` unfolding inc_def by (auto simp: carry_\) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 69` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 70` ```fun add :: "snat \ snat \ snat" where ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 71` ``` "add rs [] = rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 72` ```| "add [] rs = rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 73` ```| "add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = ( ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 74` ``` if r\<^sub>1 < r\<^sub>2 then r\<^sub>1#add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 75` ``` else if r\<^sub>21 then r\<^sub>2#add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2 ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 76` ``` else carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 77` ``` )" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 78` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 79` ```lemma add_rank_bound: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 80` ``` assumes "r' \ set (add rs\<^sub>1 rs\<^sub>2)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 81` ``` assumes "\r'\set rs\<^sub>1. r < r'" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 82` ``` assumes "\r'\set rs\<^sub>2. r < r'" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 83` ``` shows "r < r'" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 84` ``` using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 85` ``` apply (induction rs\<^sub>1 rs\<^sub>2 arbitrary: r' rule: add.induct) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 86` ``` apply (auto split: if_splits simp: carry_rank_bound) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 87` ``` done ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 88` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 89` ```lemma add_invar[simp]: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 90` ``` assumes "invar rs\<^sub>1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 91` ``` assumes "invar rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 92` ``` shows "invar (add rs\<^sub>1 rs\<^sub>2)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 93` ``` using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 94` ```proof (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 95` ``` case (3 r\<^sub>1 rs\<^sub>1 r\<^sub>2 rs\<^sub>2) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 96` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 97` ``` consider (LT) "r\<^sub>1 < r\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 98` ``` | (GT) "r\<^sub>1 > r\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 99` ``` | (EQ) "r\<^sub>1 = r\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 100` ``` using antisym_conv3 by blast ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 101` ``` then show ?case proof cases ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 102` ``` case LT ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 103` ``` then show ?thesis using 3 ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 104` ``` by (force elim!: add_rank_bound) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 105` ``` next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 106` ``` case GT ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 107` ``` then show ?thesis using 3 ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 108` ``` by (force elim!: add_rank_bound) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 109` ``` next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 110` ``` case [simp]: EQ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 111` d7b714476f3f Revived exercises lammich parents: diff changeset ` 112` ``` from "3.IH"(3) "3.prems" have [simp]: "invar (add rs\<^sub>1 rs\<^sub>2)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 113` ``` by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 114` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 115` ``` have "r\<^sub>2 < r'" if "r' \ set (add rs\<^sub>1 rs\<^sub>2)" for r' ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 116` ``` using that ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 117` ``` apply (rule add_rank_bound) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 118` ``` using "3.prems" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 119` ``` with EQ show ?thesis by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 120` ``` qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 121` ```qed simp_all ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 122` d7b714476f3f Revived exercises lammich parents: diff changeset ` 123` ```lemma add_\[simp]: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 124` ``` assumes "invar rs\<^sub>1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 125` ``` assumes "invar rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 126` ``` shows "\ (add rs\<^sub>1 rs\<^sub>2) = \ rs\<^sub>1 + \ rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 127` ``` using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 128` ``` apply (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 129` ``` apply (auto simp: carry_\ Suc_leI add_rank_bound) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 130` ``` done ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 131` d7b714476f3f Revived exercises lammich parents: diff changeset ` 132` ```subsection \Complexity\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 133` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 134` ```lemma size_snat: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 135` ``` assumes "invar rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 136` ``` shows "2^length rs \ \ rs + 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 137` ```proof - ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 138` ``` have "(2::nat)^length rs = (\i\{0.. parents: diff changeset ` 139` ``` by (simp add: power2sum) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 140` ``` also note strictly_ascending_sum_mono_lowerbound[OF \invar rs\, of "op ^ (2::nat)"] ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 141` ``` finally show "2 ^ length rs \ \ rs + 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 142` ``` unfolding \_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 143` ```qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 144` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 145` ```subsubsection \Timing Functions\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 146` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 147` ```fun t_carry :: "rank \ snat \ nat" where ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 148` ``` "t_carry r [] = 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 149` ```| "t_carry r (r'#rest) = (if r parents: diff changeset ` 150` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 151` ```definition "t_inc rs = t_carry 0 rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 152` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 153` ```lemma t_inc_bound: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 154` ``` assumes "invar rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 155` ``` shows "t_inc rs \ log 2 (\ rs + 1) + 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 156` ```proof - ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 157` ``` have "t_carry r rs \ length rs + 1" for r ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 158` ``` by (induction r rs rule: t_carry.induct) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 159` ``` hence "t_inc rs \ length rs + 1" unfolding t_inc_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 160` ``` hence "(2::nat)^t_inc rs \ 2^(length rs + 1)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 161` ``` by (rule power_increasing) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 162` ``` also have "\ \ 2*(\ rs + 1)" using size_snat[OF \invar rs\] by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 163` ``` finally have "2 ^ t_inc rs \ 2 * (\ rs + 1)" . ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 164` ``` from le_log2_of_power[OF this] show ?thesis ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 165` ``` by (simp only: log_mult of_nat_mult) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 166` ```qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 167` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 168` ```fun t_add :: "snat \ snat \ nat" where ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 169` ``` "t_add rs [] = 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 170` ```| "t_add [] rs = 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 171` ```| "t_add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = 1 + ( ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 172` ``` if r\<^sub>1 < r\<^sub>2 then t_add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 173` ``` else if r\<^sub>21 then t_add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2 ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 174` ``` else t_carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2 ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 175` ``` )" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 176` d7b714476f3f Revived exercises lammich parents: diff changeset ` 177` ```lemma l_carry_estimate: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 178` ``` "t_carry r rs + length (carry r rs) = 2 + length rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 179` ``` by (induction r rs rule: carry.induct) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 180` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 181` ```lemma l_add_estimate: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 182` ``` "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" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 183` ``` apply (induction rs\<^sub>1 rs\<^sub>2 rule: t_add.induct) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 184` ``` apply (auto simp: l_carry_estimate algebra_simps) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 185` ``` done ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 186` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 187` ```lemma t_add_bound: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 188` ``` fixes rs\<^sub>1 rs\<^sub>2 ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 189` ``` defines "n\<^sub>1 \ \ rs\<^sub>1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 190` ``` defines "n\<^sub>2 \ \ rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 191` ``` assumes INVARS: "invar rs\<^sub>1" "invar rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 192` ``` shows "t_add rs\<^sub>1 rs\<^sub>2 \ 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 193` ```proof - ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 194` ``` define n where "n = n\<^sub>1 + n\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 195` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 196` ``` from l_add_estimate[of rs\<^sub>1 rs\<^sub>2] ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 197` ``` have "t_add rs\<^sub>1 rs\<^sub>2 \ 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 198` ``` hence "(2::nat)^t_add rs\<^sub>1 rs\<^sub>2 \ 2^(2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 199` ``` by (rule power_increasing) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 200` ``` also have "\ = 2*(2^length rs\<^sub>1)\<^sup>2*(2^length rs\<^sub>2)\<^sup>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 201` ``` by (auto simp: algebra_simps power_add power_mult) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 202` ``` also note INVARS(1)[THEN size_snat] ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 203` ``` also note INVARS(2)[THEN size_snat] ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 204` ``` finally have "2 ^ t_add rs\<^sub>1 rs\<^sub>2 \ 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 205` ``` by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 206` ``` from le_log2_of_power[OF this] have "t_add rs\<^sub>1 rs\<^sub>2 \ log 2 \" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 207` ``` by simp ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 208` ``` also have "\ = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 209` ``` by (simp add: log_mult log_nat_power) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 210` ``` also have "n\<^sub>2 \ n" by (auto simp: n_def) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 211` ``` 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)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 212` ``` by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 213` ``` also have "n\<^sub>1 \ n" by (auto simp: n_def) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 214` ``` finally have "t_add rs\<^sub>1 rs\<^sub>2 \ log 2 2 + 4*log 2 (n + 1)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 215` ``` by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 216` ``` also have "log 2 2 \ 2" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 217` ``` finally have "t_add rs\<^sub>1 rs\<^sub>2 \ 4*log 2 (n + 1) + 2" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 218` ``` thus ?thesis unfolding n_def by (auto simp: algebra_simps) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 219` ```qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 220` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 221` ```subsection \Representable Number\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 222` ```text \ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 223` ``` Estimating the largest representable number if indices are bounded by \K\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 224` ```\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 225` ```(* Exercise! *) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 226` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 227` ```definition "max_snat K = [0.. parents: diff changeset ` 228` ```lemma "invar (max_snat K)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 229` ``` unfolding max_snat_def by (induction K) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 230` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 231` ```lemma \_max_snat: "\ (max_snat K) = 2^K - 1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 232` ``` unfolding \_def max_snat_def ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 233` ``` by (simp add: interv_sum_list_conv_sum_set_nat power2sum) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 234` d7b714476f3f Revived exercises lammich parents: diff changeset ` 235` ```text \Indices in @{term \max_snat K\} are actually bounded by @{term \K\}\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 236` ```lemma max_snat_bounded: "\r\set (max_snat K). r parents: diff changeset ` 237` ``` unfolding max_snat_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 238` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 239` ```text \@{term \max_snat K\} is maximal\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 240` ```lemma max_snat_max: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 241` ``` assumes "invar rs" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 242` ``` assumes "\r\set rs. r parents: diff changeset ` 243` ``` shows "\ rs \ \ (max_snat K)" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 244` ``` unfolding \_max_snat ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 245` ``` using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 246` ```proof (induction rs arbitrary: K rule: rev_induct) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 247` ``` case Nil ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 248` ``` then show ?case by simp ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 249` ```next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 250` ``` case (snoc r rs) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 251` ``` from snoc.prems have "invar rs" "\r'\set rs. r' parents: diff changeset ` 252` ``` from snoc.IH[OF this] have IH: "\ rs \ 2 ^ r - 1" . ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 253` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 254` ``` from snoc.prems have "r parents: diff changeset ` 255` ``` hence "r+1 \ K" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 256` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 257` ``` have "\ (rs @ [r]) = \ rs + 2^r" unfolding \_def by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 258` ``` also have "\ \ 2^r - 1 + 2^r" using IH by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 259` ``` also have "\ = 2^(r+1) - 1" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 260` ``` also note \r+1 \ K\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 261` ``` finally show ?case by (auto simp: diff_le_mono) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 262` ```qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 263` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 264` ```subsubsection \Injectivity\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 265` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 266` ```(* Bonus Exercise! *) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 267` ```lemma \_inj: ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 268` ``` assumes "invar rs\<^sub>1" "invar rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 269` ``` shows "\ rs\<^sub>1 = \ rs\<^sub>2 \ rs\<^sub>1 = rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 270` ```proof safe ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 271` ``` assume "\ rs\<^sub>1 = \ rs\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 272` ``` thus "rs\<^sub>1 = rs\<^sub>2" using assms ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 273` ``` proof (induction rs\<^sub>1 arbitrary: rs\<^sub>2 rule: rev_induct) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 274` ``` case Nil ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 275` ``` then show ?case by (cases rs\<^sub>2) auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 276` ``` next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 277` ``` case (snoc r\<^sub>1 rs\<^sub>1 xrs\<^sub>2) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 278` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 279` ``` show ?case proof (cases xrs\<^sub>2 rule: rev_cases) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 280` ``` case Nil ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 281` ``` then show ?thesis using snoc.prems by simp ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 282` ``` next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 283` ``` case snoc2[simp]: (snoc rs\<^sub>2 r\<^sub>2) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 284` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 285` ``` from snoc.prems have "invar rs\<^sub>1" "invar rs\<^sub>2" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 286` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 287` ``` consider (EQ) "r\<^sub>1 = r\<^sub>2" | (LT) "r\<^sub>1 < r\<^sub>2" | (GT) "r\<^sub>1 > r\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 288` ``` using less_linear by blast ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 289` ``` thus ?thesis proof (cases) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 290` ``` case EQ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 291` ``` then show ?thesis using snoc by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 292` ``` next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 293` ``` case LT ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 294` ``` from snoc.prems have "\r\set rs\<^sub>1. r1" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 295` ``` from max_snat_max[unfolded \_max_snat, OF \invar rs\<^sub>1\ this] ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 296` ``` have "\ rs\<^sub>1 < 2 ^ r\<^sub>1" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 297` ``` by auto (metis Suc_pred le_imp_less_Suc pos2 zero_less_power) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 298` ``` hence "\ (rs\<^sub>1@[r\<^sub>1]) < 2 ^ (r\<^sub>1 + 1)" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 299` ``` also have \r\<^sub>1 + 1 \ r\<^sub>2\ using LT by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 300` ``` finally have "\ (rs\<^sub>1 @ [r\<^sub>1]) < 2 ^ r\<^sub>2" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 301` ``` also have "\ xrs\<^sub>2 \ 2 ^ r\<^sub>2" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 302` ``` finally have False using \\ (rs\<^sub>1 @ [r\<^sub>1]) = \ xrs\<^sub>2\ by simp ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 303` ``` then show ?thesis .. ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 304` ``` next ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 305` ``` case GT ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 306` ``` text \Analogously\ ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 307` ``` from snoc.prems have "\r\set rs\<^sub>2. r2" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 308` ``` from max_snat_max[unfolded \_max_snat, OF \invar rs\<^sub>2\ this] ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 309` ``` have "\ rs\<^sub>2 < 2 ^ r\<^sub>2" ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 310` ``` by auto (metis Suc_pred le_imp_less_Suc pos2 zero_less_power) ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 311` ``` hence "\ xrs\<^sub>2 < 2 ^ (r\<^sub>2 + 1)" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 312` ``` also have \r\<^sub>2 + 1 \ r\<^sub>1\ using GT by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 313` ``` finally have "\ (rs\<^sub>2 @ [r\<^sub>2]) < 2 ^ r\<^sub>1" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 314` ``` also have "\ (rs\<^sub>1@[r\<^sub>1]) \ 2 ^ r\<^sub>1" by auto ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 315` ``` finally have False using \\ (rs\<^sub>1 @ [r\<^sub>1]) = \ xrs\<^sub>2\ by simp ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 316` ``` then show ?thesis .. ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 317` ``` qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 318` ``` qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 319` ``` qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 320` ```qed ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 321` d7b714476f3f Revived exercises lammich parents: diff changeset ` 322` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 323` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 324` ``` ``` d7b714476f3f Revived exercises lammich parents: diff changeset ` 325` ```end ```