70190
|
1 |
(* Title: HOL/Word/Misc_Auxiliary.thy
|
|
2 |
Author: Jeremy Dawson, NICTA
|
|
3 |
*)
|
|
4 |
|
|
5 |
section \<open>Generic auxiliary\<close>
|
|
6 |
|
|
7 |
theory Misc_Auxiliary
|
|
8 |
imports Main
|
|
9 |
begin
|
|
10 |
|
|
11 |
subsection \<open>Arithmetic lemmas\<close>
|
|
12 |
|
|
13 |
lemma 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 |
|
|
21 |
lemma 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 |
|
|
25 |
lemma 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 |
|
|
29 |
lemma 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 |
|
|
33 |
lemma 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 |
|
|
37 |
lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
|
|
38 |
by (rule zmod_minus1) simp
|
|
39 |
|
|
40 |
lemma 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 |
|
|
43 |
lemma inc_BitM: "Num.inc (Num.BitM n) = num.Bit0 n"
|
|
44 |
by (simp add: BitM_plus_one[symmetric] add_One)
|
|
45 |
|
|
46 |
|
|
47 |
subsection \<open>Lemmas on list operations\<close>
|
|
48 |
|
|
49 |
lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
|
|
50 |
by (induct n) (auto simp: butlast_take)
|
|
51 |
|
|
52 |
lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
|
|
53 |
using rev_nth by simp
|
|
54 |
|
|
55 |
lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
|
|
56 |
by (simp add: nth_rev)
|
|
57 |
|
|
58 |
lemma hd_butlast: "length xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
|
|
59 |
by (cases xs) auto
|
|
60 |
|
|
61 |
|
|
62 |
subsection \<open>Implicit augmentation of list prefixes\<close>
|
|
63 |
|
|
64 |
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
|
65 |
where
|
|
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 |
|
|
72 |
lemma 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 |
|
|
81 |
lemma 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 |
|
|
84 |
lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
|
|
85 |
by (simp add: takefill_alt replicate_add [symmetric])
|
|
86 |
|
|
87 |
lemma 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 |
|
|
90 |
lemma length_takefill [simp]: "length (takefill fill n l) = n"
|
|
91 |
by (simp add: takefill_alt)
|
|
92 |
|
|
93 |
lemma 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 |
|
|
96 |
lemma 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 |
|
|
99 |
lemma 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 |
|
|
102 |
lemma 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 |
|
|
105 |
lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
|
|
106 |
by (induct xs) auto
|
|
107 |
|
|
108 |
lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
|
|
109 |
by (induct xs arbitrary: l) auto
|
|
110 |
|
|
111 |
lemmas takefill_same [simp] = takefill_same' [OF refl]
|
|
112 |
|
|
113 |
lemma 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 |
|
|
122 |
lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
|
|
123 |
by auto
|
|
124 |
|
|
125 |
lemmas takefill_Suc_cases =
|
|
126 |
list.cases [THEN takefill.Suc [THEN trans]]
|
|
127 |
|
|
128 |
lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
|
|
129 |
lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
|
|
130 |
|
|
131 |
lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
|
|
132 |
takefill_minus [symmetric, THEN trans]]
|
|
133 |
|
|
134 |
lemma takefill_numeral_Nil [simp]:
|
|
135 |
"takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
|
|
136 |
by (simp add: numeral_eq_Suc)
|
|
137 |
|
|
138 |
lemma 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 |
|
|
143 |
subsection \<open>Auxiliary: Range projection\<close>
|
|
144 |
|
|
145 |
definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
|
|
146 |
where "bl_of_nth n f = map f (rev [0..<n])"
|
|
147 |
|
|
148 |
lemma 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 |
|
|
153 |
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
|
|
154 |
by (simp add: bl_of_nth_def)
|
|
155 |
|
|
156 |
lemma 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 |
|
|
159 |
lemma 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 |
|
|
162 |
lemma 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 |
|
|
176 |
lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
|
|
177 |
by (simp add: bl_of_nth_nth_le)
|
|
178 |
|
|
179 |
end
|