1(*  Title:      HOL/Word/Misc_Auxiliary.thy
2    Author:     Jeremy Dawson, NICTA
3*)
4
5section \<open>Generic auxiliary\<close>
6
7theory Misc_Auxiliary
8  imports Main
9begin
10
11subsection \<open>Arithmetic lemmas\<close>
12
13lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
14  for b n :: int
15  apply safe
16    apply (erule (1) mod_pos_pos_trivial)
17   apply (erule_tac [!] subst)
18   apply auto
19  done
20
21lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
22  for a n :: int
23  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
24
25lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
26  for b n :: int
27  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
28
29lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
30  for b n :: int
31  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
32
33lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
34  for n d :: int
35  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
36
37lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
38  by (rule zmod_minus1) simp
39
40lemma sub_inc_One: "Num.sub (Num.inc n) num.One = numeral n"
41  by (metis add_diff_cancel add_neg_numeral_special(3) add_uminus_conv_diff numeral_inc)
42  
43lemma inc_BitM: "Num.inc (Num.BitM n) = num.Bit0 n"
44  by (simp add: BitM_plus_one[symmetric] add_One)
45
46
47subsection \<open>Lemmas on list operations\<close>
48
49lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
50  by (induct n) (auto simp: butlast_take)
51
52lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
53  using rev_nth by simp
54
55lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
56  by (simp add: nth_rev)
57
58lemma hd_butlast: "length xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
59  by (cases xs) auto
60
61
62subsection \<open>Implicit augmentation of list prefixes\<close>
63
64primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
65where
66    Z: "takefill fill 0 xs = []"
67  | Suc: "takefill fill (Suc n) xs =
68      (case xs of
69        [] \<Rightarrow> fill # takefill fill n xs
70      | y # ys \<Rightarrow> y # takefill fill n ys)"
71
72lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
73  apply (induct n arbitrary: m l)
74   apply clarsimp
75  apply clarsimp
76  apply (case_tac m)
77   apply (simp split: list.split)
78  apply (simp split: list.split)
79  done
80
81lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
82  by (induct n arbitrary: l) (auto split: list.split)
83
84lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
85  by (simp add: takefill_alt replicate_add [symmetric])
86
87lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
88  by (induct m arbitrary: l n) (auto split: list.split)
89
90lemma length_takefill [simp]: "length (takefill fill n l) = n"
91  by (simp add: takefill_alt)
92
93lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
94  by (induct k arbitrary: w n) (auto split: list.split)
95
96lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
97  by (induct k arbitrary: w) (auto split: list.split)
98
99lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
100  by (auto simp: le_iff_add takefill_le')
101
102lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
103  by (auto simp: le_iff_add take_takefill')
104
105lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
106  by (induct xs) auto
107
108lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
109  by (induct xs arbitrary: l) auto
110
111lemmas takefill_same [simp] = takefill_same' [OF refl]
112
113lemma tf_rev:
114  "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
115    rev (takefill y m (rev (takefill x k (rev bl))))"
116  apply (rule nth_equalityI)
117   apply (auto simp add: nth_takefill nth_rev)
118  apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
119  apply arith
120  done
121
122lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
123  by auto
124
125lemmas takefill_Suc_cases =
126  list.cases [THEN takefill.Suc [THEN trans]]
127
128lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
129lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
130
131lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
132  takefill_minus [symmetric, THEN trans]]
133
134lemma takefill_numeral_Nil [simp]:
135  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
136  by (simp add: numeral_eq_Suc)
137
138lemma takefill_numeral_Cons [simp]:
139  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
140  by (simp add: numeral_eq_Suc)
141
142
143subsection \<open>Auxiliary: Range projection\<close>
144
145definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
146  where "bl_of_nth n f = map f (rev [0..<n])"
147
148lemma bl_of_nth_simps [simp, code]:
149  "bl_of_nth 0 f = []"
150  "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
151  by (simp_all add: bl_of_nth_def)
152
153lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
154  by (simp add: bl_of_nth_def)
155
156lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
157  by (simp add: bl_of_nth_def rev_map)
158
159lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
160  by (simp add: bl_of_nth_def)
161
162lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
163  apply (induct n arbitrary: xs)
164   apply clarsimp
165  apply clarsimp
166  apply (rule trans [OF _ hd_Cons_tl])
167   apply (frule Suc_le_lessD)
168   apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
169   apply (subst hd_drop_conv_nth)
170    apply force
171   apply simp_all
172  apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
173  apply simp
174  done
175
176lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
177  by (simp add: bl_of_nth_nth_le)
178
179end
180