author | haftmann |
Fri, 25 Sep 2020 05:26:09 +0000 | |
changeset 72292 | 4a58c38b85ff |
parent 71942 | d2654b30f7bd |
child 72397 | 48013583e8e6 |
permissions | -rw-r--r-- |
65363 | 1 |
(* |
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
39302
diff
changeset
|
2 |
Author: Jeremy Dawson and Gerwin Klein, NICTA |
24333 | 3 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
49739
diff
changeset
|
4 |
Consequences of type definition theorems, and of extended type definition. |
24333 | 5 |
*) |
24350 | 6 |
|
61799 | 7 |
section \<open>Type Definition Theorems\<close> |
24350 | 8 |
|
37655 | 9 |
theory Misc_Typedef |
72292 | 10 |
imports Main Word |
26560 | 11 |
begin |
24333 | 12 |
|
72292 | 13 |
subsection "More lemmas about normal type definitions" |
25262
d0928156e326
Added reference to Jeremy Dawson's paper on the word library.
kleing
parents:
24350
diff
changeset
|
14 |
|
67120 | 15 |
lemma tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" |
16 |
and tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" |
|
17 |
and tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y" |
|
24333 | 18 |
by (auto simp: type_definition_def) |
19 |
||
67399 | 20 |
lemma td_nat_int: "type_definition int nat (Collect ((\<le>) 0))" |
24333 | 21 |
unfolding type_definition_def by auto |
22 |
||
23 |
context type_definition |
|
24 |
begin |
|
25 |
||
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
26 |
declare Rep [iff] Rep_inverse [simp] Rep_inject [simp] |
24333 | 27 |
|
67120 | 28 |
lemma Abs_eqD: "Abs x = Abs y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y" |
24333 | 29 |
by (simp add: Abs_inject) |
65363 | 30 |
|
67120 | 31 |
lemma Abs_inverse': "r \<in> A \<Longrightarrow> Abs r = a \<Longrightarrow> Rep a = r" |
24333 | 32 |
by (safe elim!: Abs_inverse) |
33 |
||
67120 | 34 |
lemma Rep_comp_inverse: "Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
35 |
using Rep_inverse by auto |
24333 | 36 |
|
67120 | 37 |
lemma Rep_eqD [elim!]: "Rep x = Rep y \<Longrightarrow> x = y" |
24333 | 38 |
by simp |
39 |
||
67120 | 40 |
lemma Rep_inverse': "Rep a = r \<Longrightarrow> Abs r = a" |
24333 | 41 |
by (safe intro!: Rep_inverse) |
42 |
||
67120 | 43 |
lemma comp_Abs_inverse: "f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
44 |
using Rep_inverse by auto |
24333 | 45 |
|
67120 | 46 |
lemma set_Rep: "A = range Rep" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
37655
diff
changeset
|
47 |
proof (rule set_eqI) |
67120 | 48 |
show "x \<in> A \<longleftrightarrow> x \<in> range Rep" for x |
24333 | 49 |
by (auto dest: Abs_inverse [of x, symmetric]) |
65363 | 50 |
qed |
24333 | 51 |
|
65363 | 52 |
lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
37655
diff
changeset
|
53 |
proof (rule set_eqI) |
67120 | 54 |
show "x \<in> A \<longleftrightarrow> x \<in> range (Rep \<circ> Abs)" for x |
24333 | 55 |
by (auto dest: Abs_inverse [of x, symmetric]) |
65363 | 56 |
qed |
24333 | 57 |
|
58 |
lemma Abs_inj_on: "inj_on Abs A" |
|
65363 | 59 |
unfolding inj_on_def |
24333 | 60 |
by (auto dest: Abs_inject [THEN iffD1]) |
61 |
||
62 |
lemma image: "Abs ` A = UNIV" |
|
71942 | 63 |
by (fact Abs_image) |
24333 | 64 |
|
65 |
lemmas td_thm = type_definition_axioms |
|
66 |
||
67120 | 67 |
lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" |
24333 | 68 |
by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) |
69 |
||
70 |
lemmas fns1a = disjI1 [THEN fns1] |
|
71 |
lemmas fns1b = disjI2 [THEN fns1] |
|
72 |
||
67120 | 73 |
lemma fns4: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
74 |
by auto |
24333 | 75 |
|
76 |
end |
|
77 |
||
67399 | 78 |
interpretation nat_int: type_definition int nat "Collect ((\<le>) 0)" |
24333 | 79 |
by (rule td_nat_int) |
80 |
||
27138
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
81 |
declare |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
82 |
nat_int.Rep_cases [cases del] |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
83 |
nat_int.Abs_cases [cases del] |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
84 |
nat_int.Rep_induct [induct del] |
63fdfcf6c7a3
proper deletion of nat cases/induct rules from type_definition;
wenzelm
parents:
27135
diff
changeset
|
85 |
nat_int.Abs_induct [induct del] |
24333 | 86 |
|
87 |
||
24350 | 88 |
subsection "Extended form of type definition predicate" |
24333 | 89 |
|
90 |
lemma td_conds: |
|
67120 | 91 |
"norm \<circ> norm = norm \<Longrightarrow> |
92 |
fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<and> norm \<circ> fr \<circ> norm = norm \<circ> fr" |
|
24333 | 93 |
apply safe |
49739 | 94 |
apply (simp_all add: comp_assoc) |
24333 | 95 |
apply (simp_all add: o_assoc) |
96 |
done |
|
97 |
||
67120 | 98 |
lemma fn_comm_power: "fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n" |
65363 | 99 |
apply (rule ext) |
24333 | 100 |
apply (induct n) |
101 |
apply (auto dest: fun_cong) |
|
102 |
done |
|
103 |
||
104 |
lemmas fn_comm_power' = |
|
45604 | 105 |
ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def] |
24333 | 106 |
|
107 |
||
108 |
locale td_ext = type_definition + |
|
109 |
fixes norm |
|
110 |
assumes eq_norm: "\<And>x. Rep (Abs x) = norm x" |
|
111 |
begin |
|
112 |
||
67120 | 113 |
lemma Abs_norm [simp]: "Abs (norm x) = Abs x" |
24333 | 114 |
using eq_norm [of x] by (auto elim: Rep_inverse') |
115 |
||
67120 | 116 |
lemma td_th: "g \<circ> Abs = f \<Longrightarrow> f (Rep x) = g x" |
24333 | 117 |
by (drule comp_Abs_inverse [symmetric]) simp |
118 |
||
65363 | 119 |
lemma eq_norm': "Rep \<circ> Abs = norm" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
120 |
by (auto simp: eq_norm) |
24333 | 121 |
|
122 |
lemma norm_Rep [simp]: "norm (Rep x) = Rep x" |
|
123 |
by (auto simp: eq_norm' intro: td_th) |
|
124 |
||
125 |
lemmas td = td_thm |
|
126 |
||
67613 | 127 |
lemma set_iff_norm: "w \<in> A \<longleftrightarrow> w = norm w" |
24333 | 128 |
by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
129 |
||
67120 | 130 |
lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" |
24333 | 131 |
apply (rule iffI) |
132 |
apply (clarsimp simp add: eq_norm) |
|
133 |
apply (simp add: eq_norm' [symmetric]) |
|
134 |
done |
|
135 |
||
67120 | 136 |
lemma norm_eq_iff: "norm x = norm y \<longleftrightarrow> Abs x = Abs y" |
24333 | 137 |
by (simp add: eq_norm' [symmetric]) |
138 |
||
65363 | 139 |
lemma norm_comps: |
140 |
"Abs \<circ> norm = Abs" |
|
141 |
"norm \<circ> Rep = Rep" |
|
142 |
"norm \<circ> norm = norm" |
|
24333 | 143 |
by (auto simp: eq_norm' [symmetric] o_def) |
144 |
||
145 |
lemmas norm_norm [simp] = norm_comps |
|
146 |
||
67120 | 147 |
lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr" |
45538
1fffa81b9b83
eliminated slightly odd Rep' with dynamically-scoped [simplified];
wenzelm
parents:
44939
diff
changeset
|
148 |
by (fold eq_norm') auto |
24333 | 149 |
|
67408 | 150 |
text \<open> |
151 |
following give conditions for converses to \<open>td_fns1\<close> |
|
152 |
\<^item> the condition \<open>norm \<circ> fr \<circ> norm = fr \<circ> norm\<close> says that |
|
153 |
\<open>fr\<close> takes normalised arguments to normalised results |
|
154 |
\<^item> \<open>norm \<circ> fr \<circ> norm = norm \<circ> fr\<close> says that \<open>fr\<close> |
|
155 |
takes norm-equivalent arguments to norm-equivalent results |
|
156 |
\<^item> \<open>fr \<circ> norm = fr\<close> says that \<open>fr\<close> |
|
157 |
takes norm-equivalent arguments to the same result |
|
158 |
\<^item> \<open>norm \<circ> fr = fr\<close> says that \<open>fr\<close> takes any argument to a normalised result |
|
159 |
\<close> |
|
67120 | 160 |
lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
24333 | 161 |
apply (fold eq_norm') |
162 |
apply safe |
|
163 |
prefer 2 |
|
164 |
apply (simp add: o_assoc) |
|
165 |
apply (rule ext) |
|
166 |
apply (drule_tac x="Rep x" in fun_cong) |
|
167 |
apply auto |
|
168 |
done |
|
169 |
||
67120 | 170 |
lemma fns3: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> fa \<circ> Abs = Abs \<circ> fr" |
24333 | 171 |
apply (fold eq_norm') |
172 |
apply safe |
|
173 |
prefer 2 |
|
49739 | 174 |
apply (simp add: comp_assoc) |
24333 | 175 |
apply (rule ext) |
65363 | 176 |
apply (drule_tac f="a \<circ> b" for a b in fun_cong) |
24333 | 177 |
apply simp |
178 |
done |
|
179 |
||
67120 | 180 |
lemma fns: "fr \<circ> norm = norm \<circ> fr \<Longrightarrow> fa \<circ> Abs = Abs \<circ> fr \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
24333 | 181 |
apply safe |
182 |
apply (frule fns1b) |
|
65363 | 183 |
prefer 2 |
184 |
apply (frule fns1a) |
|
24333 | 185 |
apply (rule fns3 [THEN iffD1]) |
186 |
prefer 3 |
|
187 |
apply (rule fns2 [THEN iffD1]) |
|
49739 | 188 |
apply (simp_all add: comp_assoc) |
24333 | 189 |
apply (simp_all add: o_assoc) |
190 |
done |
|
191 |
||
67120 | 192 |
lemma range_norm: "range (Rep \<circ> Abs) = A" |
24333 | 193 |
by (simp add: set_Rep_Abs) |
194 |
||
195 |
end |
|
196 |
||
197 |
lemmas td_ext_def' = |
|
198 |
td_ext_def [unfolded type_definition_def td_ext_axioms_def] |
|
199 |
||
72292 | 200 |
|
201 |
subsection \<open>Type-definition locale instantiations\<close> |
|
202 |
||
203 |
definition uints :: "nat \<Rightarrow> int set" |
|
204 |
\<comment> \<open>the sets of integers representing the words\<close> |
|
205 |
where "uints n = range (take_bit n)" |
|
206 |
||
207 |
definition sints :: "nat \<Rightarrow> int set" |
|
208 |
where "sints n = range (signed_take_bit (n - 1))" |
|
209 |
||
210 |
lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" |
|
211 |
by (simp add: uints_def range_bintrunc) |
|
212 |
||
213 |
lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}" |
|
214 |
by (simp add: sints_def range_sbintrunc) |
|
215 |
||
216 |
definition unats :: "nat \<Rightarrow> nat set" |
|
217 |
where "unats n = {i. i < 2 ^ n}" |
|
218 |
||
219 |
\<comment> \<open>naturals\<close> |
|
220 |
lemma uints_unats: "uints n = int ` unats n" |
|
221 |
apply (unfold unats_def uints_num) |
|
222 |
apply safe |
|
223 |
apply (rule_tac image_eqI) |
|
224 |
apply (erule_tac nat_0_le [symmetric]) |
|
225 |
by auto |
|
226 |
||
227 |
lemma unats_uints: "unats n = nat ` uints n" |
|
228 |
by (auto simp: uints_unats image_iff) |
|
229 |
||
230 |
lemma td_ext_uint: |
|
231 |
"td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) |
|
232 |
(\<lambda>w::int. w mod 2 ^ LENGTH('a))" |
|
233 |
apply (unfold td_ext_def') |
|
234 |
apply transfer |
|
235 |
apply (simp add: uints_num take_bit_eq_mod) |
|
236 |
done |
|
237 |
||
238 |
interpretation word_uint: |
|
239 |
td_ext |
|
240 |
"uint::'a::len word \<Rightarrow> int" |
|
241 |
word_of_int |
|
242 |
"uints (LENGTH('a::len))" |
|
243 |
"\<lambda>w. w mod 2 ^ LENGTH('a::len)" |
|
244 |
by (fact td_ext_uint) |
|
245 |
||
246 |
lemmas td_uint = word_uint.td_thm |
|
247 |
lemmas int_word_uint = word_uint.eq_norm |
|
248 |
||
249 |
lemma td_ext_ubin: |
|
250 |
"td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) |
|
251 |
(take_bit (LENGTH('a)))" |
|
252 |
apply standard |
|
253 |
apply transfer |
|
254 |
apply simp |
|
255 |
done |
|
256 |
||
257 |
interpretation word_ubin: |
|
258 |
td_ext |
|
259 |
"uint::'a::len word \<Rightarrow> int" |
|
260 |
word_of_int |
|
261 |
"uints (LENGTH('a::len))" |
|
262 |
"take_bit (LENGTH('a::len))" |
|
263 |
by (fact td_ext_ubin) |
|
264 |
||
265 |
lemma td_ext_unat [OF refl]: |
|
266 |
"n = LENGTH('a::len) \<Longrightarrow> |
|
267 |
td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" |
|
268 |
apply (standard; transfer) |
|
269 |
apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff |
|
270 |
flip: take_bit_eq_mod) |
|
271 |
done |
|
272 |
||
273 |
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] |
|
274 |
||
275 |
interpretation word_unat: |
|
276 |
td_ext |
|
277 |
"unat::'a::len word \<Rightarrow> nat" |
|
278 |
of_nat |
|
279 |
"unats (LENGTH('a::len))" |
|
280 |
"\<lambda>i. i mod 2 ^ LENGTH('a::len)" |
|
281 |
by (rule td_ext_unat) |
|
282 |
||
283 |
lemmas td_unat = word_unat.td_thm |
|
284 |
||
285 |
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] |
|
286 |
||
287 |
lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))" |
|
288 |
for z :: "'a::len word" |
|
289 |
apply (unfold unats_def) |
|
290 |
apply clarsimp |
|
291 |
apply (rule xtrans, rule unat_lt2p, assumption) |
|
292 |
done |
|
293 |
||
294 |
lemma td_ext_sbin: |
|
295 |
"td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) |
|
296 |
(signed_take_bit (LENGTH('a) - 1))" |
|
297 |
by (standard; transfer) (auto simp add: sints_def) |
|
298 |
||
299 |
lemma td_ext_sint: |
|
300 |
"td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) |
|
301 |
(\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - |
|
302 |
2 ^ (LENGTH('a) - 1))" |
|
303 |
using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2) |
|
304 |
||
305 |
text \<open> |
|
306 |
We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version |
|
307 |
and interpretations do not produce thm duplicates. I.e. |
|
308 |
we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>, |
|
309 |
because the latter is the same thm as the former. |
|
310 |
\<close> |
|
311 |
interpretation word_sint: |
|
312 |
td_ext |
|
313 |
"sint ::'a::len word \<Rightarrow> int" |
|
314 |
word_of_int |
|
315 |
"sints (LENGTH('a::len))" |
|
316 |
"\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) - |
|
317 |
2 ^ (LENGTH('a::len) - 1)" |
|
318 |
by (rule td_ext_sint) |
|
319 |
||
320 |
interpretation word_sbin: |
|
321 |
td_ext |
|
322 |
"sint ::'a::len word \<Rightarrow> int" |
|
323 |
word_of_int |
|
324 |
"sints (LENGTH('a::len))" |
|
325 |
"signed_take_bit (LENGTH('a::len) - 1)" |
|
326 |
by (rule td_ext_sbin) |
|
327 |
||
328 |
lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm] |
|
329 |
||
330 |
lemmas td_sint = word_sint.td |
|
331 |
||
332 |
lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)" |
|
333 |
by (fact uints_def [unfolded no_bintr_alt1]) |
|
334 |
||
335 |
lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq] |
|
336 |
lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq] |
|
337 |
||
338 |
lemmas bintr_num = |
|
339 |
word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b |
|
340 |
lemmas sbintr_num = |
|
341 |
word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b |
|
342 |
||
343 |
lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]] |
|
344 |
lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]] |
|
345 |
||
346 |
interpretation test_bit: |
|
347 |
td_ext |
|
348 |
"(!!) :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool" |
|
349 |
set_bits |
|
350 |
"{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len)}" |
|
351 |
"(\<lambda>h i. h i \<and> i < LENGTH('a::len))" |
|
352 |
by standard |
|
353 |
(auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq) |
|
354 |
||
355 |
lemmas td_nth = test_bit.td_thm |
|
356 |
||
24333 | 357 |
end |