1 (* |
|
2 Author: Jeremy Dawson and Gerwin Klein, NICTA |
|
3 |
|
4 Consequences of type definition theorems, and of extended type definition. |
|
5 *) |
|
6 |
|
7 section \<open>Type Definition Theorems\<close> |
|
8 |
|
9 theory Misc_Typedef |
|
10 imports Main Word Bit_Comprehension Bits_Int |
|
11 begin |
|
12 |
|
13 subsection "More lemmas about normal type definitions" |
|
14 |
|
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" |
|
18 by (auto simp: type_definition_def) |
|
19 |
|
20 lemma td_nat_int: "type_definition int nat (Collect ((\<le>) 0))" |
|
21 unfolding type_definition_def by auto |
|
22 |
|
23 context type_definition |
|
24 begin |
|
25 |
|
26 declare Rep [iff] Rep_inverse [simp] Rep_inject [simp] |
|
27 |
|
28 lemma Abs_eqD: "Abs x = Abs y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y" |
|
29 by (simp add: Abs_inject) |
|
30 |
|
31 lemma Abs_inverse': "r \<in> A \<Longrightarrow> Abs r = a \<Longrightarrow> Rep a = r" |
|
32 by (safe elim!: Abs_inverse) |
|
33 |
|
34 lemma Rep_comp_inverse: "Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f" |
|
35 using Rep_inverse by auto |
|
36 |
|
37 lemma Rep_eqD [elim!]: "Rep x = Rep y \<Longrightarrow> x = y" |
|
38 by simp |
|
39 |
|
40 lemma Rep_inverse': "Rep a = r \<Longrightarrow> Abs r = a" |
|
41 by (safe intro!: Rep_inverse) |
|
42 |
|
43 lemma comp_Abs_inverse: "f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f" |
|
44 using Rep_inverse by auto |
|
45 |
|
46 lemma set_Rep: "A = range Rep" |
|
47 proof (rule set_eqI) |
|
48 show "x \<in> A \<longleftrightarrow> x \<in> range Rep" for x |
|
49 by (auto dest: Abs_inverse [of x, symmetric]) |
|
50 qed |
|
51 |
|
52 lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)" |
|
53 proof (rule set_eqI) |
|
54 show "x \<in> A \<longleftrightarrow> x \<in> range (Rep \<circ> Abs)" for x |
|
55 by (auto dest: Abs_inverse [of x, symmetric]) |
|
56 qed |
|
57 |
|
58 lemma Abs_inj_on: "inj_on Abs A" |
|
59 unfolding inj_on_def |
|
60 by (auto dest: Abs_inject [THEN iffD1]) |
|
61 |
|
62 lemma image: "Abs ` A = UNIV" |
|
63 by (fact Abs_image) |
|
64 |
|
65 lemmas td_thm = type_definition_axioms |
|
66 |
|
67 lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" |
|
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 |
|
73 lemma fns4: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr" |
|
74 by auto |
|
75 |
|
76 end |
|
77 |
|
78 interpretation nat_int: type_definition int nat "Collect ((\<le>) 0)" |
|
79 by (rule td_nat_int) |
|
80 |
|
81 declare |
|
82 nat_int.Rep_cases [cases del] |
|
83 nat_int.Abs_cases [cases del] |
|
84 nat_int.Rep_induct [induct del] |
|
85 nat_int.Abs_induct [induct del] |
|
86 |
|
87 |
|
88 subsection "Extended form of type definition predicate" |
|
89 |
|
90 lemma td_conds: |
|
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" |
|
93 apply safe |
|
94 apply (simp_all add: comp_assoc) |
|
95 apply (simp_all add: o_assoc) |
|
96 done |
|
97 |
|
98 lemma fn_comm_power: "fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n" |
|
99 apply (rule ext) |
|
100 apply (induct n) |
|
101 apply (auto dest: fun_cong) |
|
102 done |
|
103 |
|
104 lemmas fn_comm_power' = |
|
105 ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def] |
|
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 |
|
113 lemma Abs_norm [simp]: "Abs (norm x) = Abs x" |
|
114 using eq_norm [of x] by (auto elim: Rep_inverse') |
|
115 |
|
116 lemma td_th: "g \<circ> Abs = f \<Longrightarrow> f (Rep x) = g x" |
|
117 by (drule comp_Abs_inverse [symmetric]) simp |
|
118 |
|
119 lemma eq_norm': "Rep \<circ> Abs = norm" |
|
120 by (auto simp: eq_norm) |
|
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 |
|
127 lemma set_iff_norm: "w \<in> A \<longleftrightarrow> w = norm w" |
|
128 by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
|
129 |
|
130 lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" |
|
131 apply (rule iffI) |
|
132 apply (clarsimp simp add: eq_norm) |
|
133 apply (simp add: eq_norm' [symmetric]) |
|
134 done |
|
135 |
|
136 lemma norm_eq_iff: "norm x = norm y \<longleftrightarrow> Abs x = Abs y" |
|
137 by (simp add: eq_norm' [symmetric]) |
|
138 |
|
139 lemma norm_comps: |
|
140 "Abs \<circ> norm = Abs" |
|
141 "norm \<circ> Rep = Rep" |
|
142 "norm \<circ> norm = norm" |
|
143 by (auto simp: eq_norm' [symmetric] o_def) |
|
144 |
|
145 lemmas norm_norm [simp] = norm_comps |
|
146 |
|
147 lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr" |
|
148 by (fold eq_norm') auto |
|
149 |
|
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> |
|
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" |
|
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 |
|
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" |
|
171 apply (fold eq_norm') |
|
172 apply safe |
|
173 prefer 2 |
|
174 apply (simp add: comp_assoc) |
|
175 apply (rule ext) |
|
176 apply (drule_tac f="a \<circ> b" for a b in fun_cong) |
|
177 apply simp |
|
178 done |
|
179 |
|
180 lemma fns: "fr \<circ> norm = norm \<circ> fr \<Longrightarrow> fa \<circ> Abs = Abs \<circ> fr \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
|
181 apply safe |
|
182 apply (frule fns1b) |
|
183 prefer 2 |
|
184 apply (frule fns1a) |
|
185 apply (rule fns3 [THEN iffD1]) |
|
186 prefer 3 |
|
187 apply (rule fns2 [THEN iffD1]) |
|
188 apply (simp_all add: comp_assoc) |
|
189 apply (simp_all add: o_assoc) |
|
190 done |
|
191 |
|
192 lemma range_norm: "range (Rep \<circ> Abs) = A" |
|
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 |
|
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 (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq) |
|
353 |
|
354 lemmas td_nth = test_bit.td_thm |
|
355 |
|
356 end |
|