1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7section "Generic Lemmas used in the Word Library" 8 9theory HOL_Lemmas 10imports Main 11begin 12 13definition 14 strict_part_mono :: "'a set \<Rightarrow> ('a :: order \<Rightarrow> 'b :: order) \<Rightarrow> bool" where 15 "strict_part_mono S f \<equiv> \<forall>A\<in>S. \<forall>B\<in>S. A < B \<longrightarrow> f A < f B" 16 17lemma strict_part_mono_by_steps: 18 "strict_part_mono {..n :: nat} f = (n \<noteq> 0 \<longrightarrow> f (n - 1) < f n \<and> strict_part_mono {.. n - 1} f)" 19 apply (cases n; simp add: strict_part_mono_def) 20 apply (safe; clarsimp) 21 apply (case_tac "B = Suc nat"; simp) 22 apply (case_tac "A = nat"; clarsimp) 23 apply (erule order_less_trans [rotated]) 24 apply simp 25 done 26 27lemma strict_part_mono_singleton[simp]: 28 "strict_part_mono {x} f" 29 by (simp add: strict_part_mono_def) 30 31lemma strict_part_mono_lt: 32 "\<lbrakk> x < f 0; strict_part_mono {.. n :: nat} f \<rbrakk> \<Longrightarrow> \<forall>m \<le> n. x < f m" 33 by (metis atMost_iff le_0_eq le_cases neq0_conv order.strict_trans strict_part_mono_def) 34 35lemma strict_part_mono_reverseE: 36 "\<lbrakk> f n \<le> f m; strict_part_mono {.. N :: nat} f; n \<le> N \<rbrakk> \<Longrightarrow> n \<le> m" 37 by (rule ccontr) (fastforce simp: linorder_not_le strict_part_mono_def) 38 39lemma takeWhile_take_has_property: 40 "n \<le> length (takeWhile P xs) \<Longrightarrow> \<forall>x \<in> set (take n xs). P x" 41 by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all) 42 43lemma takeWhile_take_has_property_nth: 44 "\<lbrakk> n < length (takeWhile P xs) \<rbrakk> \<Longrightarrow> P (xs ! n)" 45 by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all) 46 47lemma takeWhile_replicate: 48 "takeWhile f (replicate len x) = (if f x then replicate len x else [])" 49 by (induct_tac len) auto 50 51lemma takeWhile_replicate_empty: 52 "\<not> f x \<Longrightarrow> takeWhile f (replicate len x) = []" 53 by (simp add: takeWhile_replicate) 54 55lemma takeWhile_replicate_id: 56 "f x \<Longrightarrow> takeWhile f (replicate len x) = replicate len x" 57 by (simp add: takeWhile_replicate) 58 59lemma power_sub: 60 fixes a :: nat 61 assumes lt: "n \<le> m" 62 and av: "0 < a" 63 shows "a ^ (m - n) = a ^ m div a ^ n" 64proof (subst nat_mult_eq_cancel1 [symmetric]) 65 show "(0::nat) < a ^ n" using av by simp 66next 67 from lt obtain q where mv: "n + q = m" 68 by (auto simp: le_iff_add) 69 70 have "a ^ n * (a ^ m div a ^ n) = a ^ m" 71 proof (subst mult.commute) 72 have "a ^ m = (a ^ m div a ^ n) * a ^ n + a ^ m mod a ^ n" 73 by (rule div_mult_mod_eq [symmetric]) 74 75 moreover have "a ^ m mod a ^ n = 0" 76 by (subst mod_eq_0_iff_dvd, subst dvd_def, rule exI [where x = "a ^ q"], 77 (subst power_add [symmetric] mv)+, rule refl) 78 79 ultimately show "(a ^ m div a ^ n) * a ^ n = a ^ m" by simp 80 qed 81 82 then show "a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n)" using lt 83 by (simp add: power_add [symmetric]) 84qed 85 86 87lemma union_sub: 88 "\<lbrakk>B \<subseteq> A; C \<subseteq> B\<rbrakk> \<Longrightarrow> (A - B) \<union> (B - C) = (A - C)" 89 by fastforce 90 91lemma insert_sub: 92 "x \<in> xs \<Longrightarrow> (insert x (xs - ys)) = (xs - (ys - {x}))" 93 by blast 94 95lemma ran_upd: 96 "\<lbrakk> inj_on f (dom f); f y = Some z \<rbrakk> \<Longrightarrow> ran (\<lambda>x. if x = y then None else f x) = ran f - {z}" 97 unfolding ran_def 98 apply (rule set_eqI) 99 apply simp 100 by (metis domI inj_on_eq_iff option.sel) 101 102lemma nat_less_power_trans: 103 fixes n :: nat 104 assumes nv: "n < 2 ^ (m - k)" 105 and kv: "k \<le> m" 106 shows "2 ^ k * n < 2 ^ m" 107proof (rule order_less_le_trans) 108 show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)" 109 by (rule mult_less_mono2 [OF nv zero_less_power]) simp 110 111 show "(2::nat) ^ k * 2 ^ (m - k) \<le> 2 ^ m" using nv kv 112 by (subst power_add [symmetric]) simp 113qed 114 115lemma nat_le_power_trans: 116 fixes n :: nat 117 shows "\<lbrakk>n \<le> 2 ^ (m - k); k \<le> m\<rbrakk> \<Longrightarrow> 2 ^ k * n \<le> 2 ^ m" 118 by (metis le_add_diff_inverse mult_le_mono2 semiring_normalization_rules(26)) 119 120lemma x_power_minus_1: 121 fixes x :: "'a :: {ab_group_add, power, numeral, one}" 122 shows "x + (2::'a) ^ n - (1::'a) = x + (2 ^ n - 1)" by simp 123 124lemma nat_diff_add: 125 fixes i :: nat 126 shows "\<lbrakk> i + j = k \<rbrakk> \<Longrightarrow> i = k - j" 127 by arith 128 129lemma pow_2_gt: "n \<ge> 2 \<Longrightarrow> (2::int) < 2 ^ n" 130 by (induct n) auto 131 132lemma if_apply_def2: 133 "(if P then F else G) = (\<lambda>x. (P \<longrightarrow> F x) \<and> (\<not> P \<longrightarrow> G x))" 134 by simp 135 136lemma case_bool_If: 137 "case_bool P Q b = (if b then P else Q)" 138 by simp 139 140lemma sum_to_zero: 141 "(a :: 'a :: ring) + b = 0 \<Longrightarrow> a = (- b)" 142 by (drule arg_cong[where f="\<lambda> x. x - a"], simp) 143 144lemma arith_is_1: 145 "\<lbrakk> x \<le> Suc 0; x > 0 \<rbrakk> \<Longrightarrow> x = 1" 146 by arith 147 148lemma if_f: 149 "(if a then f b else f c) = f (if a then b else c)" 150 by simp 151 152lemma upt_add_eq_append': 153 assumes "i \<le> j" and "j \<le> k" 154 shows "[i..<k] = [i..<j] @ [j..<k]" 155 using assms le_Suc_ex upt_add_eq_append by blast 156 157lemma split_upt_on_n: 158 "n < m \<Longrightarrow> [0 ..< m] = [0 ..< n] @ [n] @ [Suc n ..< m]" 159 by (metis append_Cons append_Nil less_Suc_eq_le less_imp_le_nat upt_add_eq_append' 160 upt_rec zero_less_Suc) 161 162lemma drop_Suc_nth: 163 "n < length xs \<Longrightarrow> drop n xs = xs!n # drop (Suc n) xs" 164 by (simp add: Cons_nth_drop_Suc) 165 166lemma n_less_equal_power_2 [simp]: 167 "n < 2 ^ n" 168 by (induct n; simp) 169 170lemma nat_min_simps [simp]: 171 "(a::nat) \<le> b \<Longrightarrow> min b a = a" 172 "a \<le> b \<Longrightarrow> min a b = a" 173 by auto 174 175lemma power_sub_int: 176 "\<lbrakk> m \<le> n; 0 < b \<rbrakk> \<Longrightarrow> b ^ n div b ^ m = (b ^ (n - m) :: int)" 177 apply (subgoal_tac "\<exists>n'. n = m + n'") 178 apply (clarsimp simp: power_add) 179 apply (rule exI[where x="n - m"]) 180 apply simp 181 done 182 183lemma suc_le_pow_2: 184 "1 < (n::nat) \<Longrightarrow> Suc n < 2 ^ n" 185 by (induct n; clarsimp) 186 (case_tac "n = 1"; clarsimp) 187 188lemma nat_le_Suc_less_imp: 189 "x < y \<Longrightarrow> x \<le> y - Suc 0" 190 by arith 191 192lemma length_takeWhile_less: 193 "\<exists>x\<in>set xs. \<not> P x \<Longrightarrow> length (takeWhile P xs) < length xs" 194 by (induct xs) (auto split: if_splits) 195 196lemma drop_eq_mono: 197 assumes le: "m \<le> n" 198 assumes drop: "drop m xs = drop m ys" 199 shows "drop n xs = drop n ys" 200proof - 201 have ex: "\<exists>p. n = p + m" by (rule exI[of _ "n - m"]) (simp add: le) 202 then obtain p where p: "n = p + m" by blast 203 show ?thesis unfolding p drop_drop[symmetric] drop by simp 204qed 205 206lemma nat_Suc_less_le_imp: 207 "(k::nat) < Suc n \<Longrightarrow> k \<le> n" 208 by auto 209 210lemma nat_add_less_by_max: 211 "\<lbrakk> (x::nat) \<le> xmax ; y < k - xmax \<rbrakk> \<Longrightarrow> x + y < k" 212 by simp 213 214lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c" 215 apply (cut_tac m = q and n = c in mod_less_divisor) 216 apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto) 217 apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst) 218 apply (simp add: add_mult_distrib2) 219 done 220 221lemma nat_le_Suc_less: 222 "0 < y \<Longrightarrow> (x \<le> y - Suc 0) = (x < y)" 223 by arith 224 225lemma nat_power_minus_less: 226 "a < 2 ^ (x - n) \<Longrightarrow> (a :: nat) < 2 ^ x" 227 by (erule order_less_le_trans) simp 228 229end 230