13 mapped to target-language builtin integers. |
11 mapped to target-language builtin integers. |
14 *} |
12 *} |
15 |
13 |
16 subsection {* Datatype of indices *} |
14 subsection {* Datatype of indices *} |
17 |
15 |
18 typedef index = "UNIV \<Colon> nat set" |
16 typedef (open) index = "UNIV \<Colon> nat set" |
19 morphisms nat_of_index index_of_nat by rule |
17 morphisms nat_of of_nat by rule |
20 |
18 |
21 lemma index_of_nat_nat_of_index [simp]: |
19 lemma of_nat_nat_of [simp]: |
22 "index_of_nat (nat_of_index k) = k" |
20 "of_nat (nat_of k) = k" |
23 by (rule nat_of_index_inverse) |
21 by (rule nat_of_inverse) |
24 |
22 |
25 lemma nat_of_index_index_of_nat [simp]: |
23 lemma nat_of_of_nat [simp]: |
26 "nat_of_index (index_of_nat n) = n" |
24 "nat_of (of_nat n) = n" |
27 by (rule index_of_nat_inverse) |
25 by (rule of_nat_inverse) (rule UNIV_I) |
28 (unfold index_def, rule UNIV_I) |
|
29 |
26 |
30 lemma [measure_function]: |
27 lemma [measure_function]: |
31 "is_measure nat_of_index" by (rule is_measure_trivial) |
28 "is_measure nat_of" by (rule is_measure_trivial) |
32 |
29 |
33 lemma index: |
30 lemma index: |
34 "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))" |
31 "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))" |
35 proof |
32 proof |
36 fix n :: nat |
33 fix n :: nat |
37 assume "\<And>n\<Colon>index. PROP P n" |
34 assume "\<And>n\<Colon>index. PROP P n" |
38 then show "PROP P (index_of_nat n)" . |
35 then show "PROP P (of_nat n)" . |
39 next |
36 next |
40 fix n :: index |
37 fix n :: index |
41 assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)" |
38 assume "\<And>n\<Colon>nat. PROP P (of_nat n)" |
42 then have "PROP P (index_of_nat (nat_of_index n))" . |
39 then have "PROP P (of_nat (nat_of n))" . |
43 then show "PROP P n" by simp |
40 then show "PROP P n" by simp |
44 qed |
41 qed |
45 |
42 |
46 lemma index_case: |
43 lemma index_case: |
47 assumes "\<And>n. k = index_of_nat n \<Longrightarrow> P" |
44 assumes "\<And>n. k = of_nat n \<Longrightarrow> P" |
48 shows P |
45 shows P |
49 by (rule assms [of "nat_of_index k"]) simp |
46 by (rule assms [of "nat_of k"]) simp |
50 |
47 |
51 lemma index_induct_raw: |
48 lemma index_induct_raw: |
52 assumes "\<And>n. P (index_of_nat n)" |
49 assumes "\<And>n. P (of_nat n)" |
53 shows "P k" |
50 shows "P k" |
54 proof - |
51 proof - |
55 from assms have "P (index_of_nat (nat_of_index k))" . |
52 from assms have "P (of_nat (nat_of k))" . |
56 then show ?thesis by simp |
53 then show ?thesis by simp |
57 qed |
54 qed |
58 |
55 |
59 lemma nat_of_index_inject [simp]: |
56 lemma nat_of_inject [simp]: |
60 "nat_of_index k = nat_of_index l \<longleftrightarrow> k = l" |
57 "nat_of k = nat_of l \<longleftrightarrow> k = l" |
61 by (rule nat_of_index_inject) |
58 by (rule nat_of_inject) |
62 |
59 |
63 lemma index_of_nat_inject [simp]: |
60 lemma of_nat_inject [simp]: |
64 "index_of_nat n = index_of_nat m \<longleftrightarrow> n = m" |
61 "of_nat n = of_nat m \<longleftrightarrow> n = m" |
65 by (auto intro!: index_of_nat_inject simp add: index_def) |
62 by (rule of_nat_inject) (rule UNIV_I)+ |
66 |
63 |
67 instantiation index :: zero |
64 instantiation index :: zero |
68 begin |
65 begin |
69 |
66 |
70 definition [simp, code del]: |
67 definition [simp, code del]: |
71 "0 = index_of_nat 0" |
68 "0 = of_nat 0" |
72 |
69 |
73 instance .. |
70 instance .. |
74 |
71 |
75 end |
72 end |
76 |
73 |
77 definition [simp]: |
74 definition [simp]: |
78 "Suc_index k = index_of_nat (Suc (nat_of_index k))" |
75 "Suc_index k = of_nat (Suc (nat_of k))" |
79 |
76 |
80 rep_datatype "0 \<Colon> index" Suc_index |
77 rep_datatype "0 \<Colon> index" Suc_index |
81 proof - |
78 proof - |
82 fix P :: "index \<Rightarrow> bool" |
79 fix P :: "index \<Rightarrow> bool" |
83 fix k :: index |
80 fix k :: index |
84 assume "P 0" then have init: "P (index_of_nat 0)" by simp |
81 assume "P 0" then have init: "P (of_nat 0)" by simp |
85 assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)" |
82 assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)" |
86 then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" . |
83 then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" . |
87 then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp |
84 then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp |
88 from init step have "P (index_of_nat (nat_of_index k))" |
85 from init step have "P (of_nat (nat_of k))" |
89 by (induct "nat_of_index k") simp_all |
86 by (induct "nat_of k") simp_all |
90 then show "P k" by simp |
87 then show "P k" by simp |
91 qed simp_all |
88 qed simp_all |
92 |
89 |
93 lemmas [code del] = index.recs index.cases |
90 lemmas [code del] = index.recs index.cases |
94 |
91 |
95 declare index_case [case_names nat, cases type: index] |
92 declare index_case [case_names nat, cases type: index] |
96 declare index.induct [case_names nat, induct type: index] |
93 declare index.induct [case_names nat, induct type: index] |
97 |
94 |
98 lemma [code]: |
95 lemma [code]: |
99 "index_size = nat_of_index" |
96 "index_size = nat_of" |
100 proof (rule ext) |
97 proof (rule ext) |
101 fix k |
98 fix k |
102 have "index_size k = nat_size (nat_of_index k)" |
99 have "index_size k = nat_size (nat_of k)" |
103 by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) |
100 by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) |
104 also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all |
101 also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all |
105 finally show "index_size k = nat_of_index k" . |
102 finally show "index_size k = nat_of k" . |
106 qed |
103 qed |
107 |
104 |
108 lemma [code]: |
105 lemma [code]: |
109 "size = nat_of_index" |
106 "size = nat_of" |
110 proof (rule ext) |
107 proof (rule ext) |
111 fix k |
108 fix k |
112 show "size k = nat_of_index k" |
109 show "size k = nat_of k" |
113 by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) |
110 by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) |
114 qed |
111 qed |
115 |
112 |
116 lemma [code]: |
113 lemma [code]: |
117 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)" |
114 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)" |
118 by (cases k, cases l) (simp add: eq) |
115 by (cases k, cases l) (simp add: eq) |
119 |
116 |
120 lemma [code nbe]: |
117 lemma [code nbe]: |
121 "eq_class.eq (k::index) k \<longleftrightarrow> True" |
118 "eq_class.eq (k::index) k \<longleftrightarrow> True" |
122 by (rule HOL.eq_refl) |
119 by (rule HOL.eq_refl) |
145 |
142 |
146 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" |
143 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" |
147 begin |
144 begin |
148 |
145 |
149 definition [simp, code del]: |
146 definition [simp, code del]: |
150 "(1\<Colon>index) = index_of_nat 1" |
147 "(1\<Colon>index) = of_nat 1" |
151 |
148 |
152 definition [simp, code del]: |
149 definition [simp, code del]: |
153 "n + m = index_of_nat (nat_of_index n + nat_of_index m)" |
150 "n + m = of_nat (nat_of n + nat_of m)" |
154 |
151 |
155 definition [simp, code del]: |
152 definition [simp, code del]: |
156 "n - m = index_of_nat (nat_of_index n - nat_of_index m)" |
153 "n - m = of_nat (nat_of n - nat_of m)" |
157 |
154 |
158 definition [simp, code del]: |
155 definition [simp, code del]: |
159 "n * m = index_of_nat (nat_of_index n * nat_of_index m)" |
156 "n * m = of_nat (nat_of n * nat_of m)" |
160 |
157 |
161 definition [simp, code del]: |
158 definition [simp, code del]: |
162 "n div m = index_of_nat (nat_of_index n div nat_of_index m)" |
159 "n div m = of_nat (nat_of n div nat_of m)" |
163 |
160 |
164 definition [simp, code del]: |
161 definition [simp, code del]: |
165 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)" |
162 "n mod m = of_nat (nat_of n mod nat_of m)" |
166 |
163 |
167 definition [simp, code del]: |
164 definition [simp, code del]: |
168 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m" |
165 "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m" |
169 |
166 |
170 definition [simp, code del]: |
167 definition [simp, code del]: |
171 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m" |
168 "n < m \<longleftrightarrow> nat_of n < nat_of m" |
172 |
169 |
173 instance by default (auto simp add: left_distrib index) |
170 instance proof |
|
171 qed (auto simp add: left_distrib) |
174 |
172 |
175 end |
173 end |
176 |
174 |
177 lemma zero_index_code [code inline, code]: |
175 lemma zero_index_code [code inline, code]: |
178 "(0\<Colon>index) = Numeral0" |
176 "(0\<Colon>index) = Numeral0" |
185 by (simp add: number_of_index_def Pls_def Bit1_def) |
183 by (simp add: number_of_index_def Pls_def Bit1_def) |
186 lemma [code post]: "Numeral1 = (1\<Colon>index)" |
184 lemma [code post]: "Numeral1 = (1\<Colon>index)" |
187 using one_index_code .. |
185 using one_index_code .. |
188 |
186 |
189 lemma plus_index_code [code nbe]: |
187 lemma plus_index_code [code nbe]: |
190 "index_of_nat n + index_of_nat m = index_of_nat (n + m)" |
188 "of_nat n + of_nat m = of_nat (n + m)" |
191 by simp |
189 by simp |
192 |
190 |
193 definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where |
191 definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where |
194 [simp, code del]: "subtract_index = op -" |
192 [simp, code del]: "subtract_index = op -" |
195 |
193 |
196 lemma subtract_index_code [code nbe]: |
194 lemma subtract_index_code [code nbe]: |
197 "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)" |
195 "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)" |
198 by simp |
196 by simp |
199 |
197 |
200 lemma minus_index_code [code]: |
198 lemma minus_index_code [code]: |
201 "n - m = subtract_index n m" |
199 "n - m = subtract_index n m" |
202 by simp |
200 by simp |
203 |
201 |
204 lemma times_index_code [code nbe]: |
202 lemma times_index_code [code nbe]: |
205 "index_of_nat n * index_of_nat m = index_of_nat (n * m)" |
203 "of_nat n * of_nat m = of_nat (n * m)" |
206 by simp |
204 by simp |
207 |
205 |
208 lemma less_eq_index_code [code nbe]: |
206 lemma less_eq_index_code [code nbe]: |
209 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m" |
207 "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m" |
210 by simp |
208 by simp |
211 |
209 |
212 lemma less_index_code [code nbe]: |
210 lemma less_index_code [code nbe]: |
213 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m" |
211 "of_nat n < of_nat m \<longleftrightarrow> n < m" |
214 by simp |
212 by simp |
215 |
213 |
216 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp |
214 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp |
217 |
215 |
218 lemma index_of_nat_code [code]: |
216 lemma of_nat_code [code]: |
219 "index_of_nat = of_nat" |
217 "of_nat = Nat.of_nat" |
220 proof |
218 proof |
221 fix n :: nat |
219 fix n :: nat |
222 have "of_nat n = index_of_nat n" |
220 have "Nat.of_nat n = of_nat n" |
223 by (induct n) simp_all |
221 by (induct n) simp_all |
224 then show "index_of_nat n = of_nat n" |
222 then show "of_nat n = Nat.of_nat n" |
225 by (rule sym) |
223 by (rule sym) |
226 qed |
224 qed |
227 |
225 |
228 lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1" |
226 lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1" |
229 by (cases i) auto |
227 by (cases i) auto |
230 |
228 |
231 definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where |
229 definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where |
232 "nat_of_index_aux i n = nat_of_index i + n" |
230 "nat_of_aux i n = nat_of i + n" |
233 |
231 |
234 lemma nat_of_index_aux_code [code]: |
232 lemma nat_of_aux_code [code]: |
235 "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))" |
233 "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))" |
236 by (auto simp add: nat_of_index_aux_def index_not_eq_zero) |
234 by (auto simp add: nat_of_aux_def index_not_eq_zero) |
237 |
235 |
238 lemma nat_of_index_code [code]: |
236 lemma nat_of_code [code]: |
239 "nat_of_index i = nat_of_index_aux i 0" |
237 "nat_of i = nat_of_aux i 0" |
240 by (simp add: nat_of_index_aux_def) |
238 by (simp add: nat_of_aux_def) |
241 |
239 |
242 definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where |
240 definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where |
243 [code del]: "div_mod_index n m = (n div m, n mod m)" |
241 [code del]: "div_mod_index n m = (n div m, n mod m)" |
244 |
242 |
245 lemma [code]: |
243 lemma [code]: |