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