7 theory Code_Index |
7 theory Code_Index |
8 imports ATP_Linkup |
8 imports ATP_Linkup |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 Indices are isomorphic to HOL @{typ int} but |
12 Indices are isomorphic to HOL @{typ nat} but |
13 mapped to target-language builtin integers |
13 mapped to target-language builtin integers |
14 *} |
14 *} |
15 |
15 |
16 subsection {* Datatype of indices *} |
16 subsection {* Datatype of indices *} |
17 |
17 |
18 datatype index = index_of_int int |
18 datatype index = index_of_nat nat |
19 |
19 |
20 lemmas [code func del] = index.recs index.cases |
20 lemmas [code func del] = index.recs index.cases |
21 |
21 |
22 fun |
22 primrec |
23 int_of_index :: "index \<Rightarrow> int" |
23 nat_of_index :: "index \<Rightarrow> nat" |
24 where |
24 where |
25 "int_of_index (index_of_int k) = k" |
25 "nat_of_index (index_of_nat k) = k" |
26 lemmas [code func del] = int_of_index.simps |
26 lemmas [code func del] = nat_of_index.simps |
27 |
27 |
28 lemma index_id [simp]: |
28 lemma index_id [simp]: |
29 "index_of_int (int_of_index k) = k" |
29 "index_of_nat (nat_of_index n) = n" |
30 by (cases k) simp_all |
30 by (cases n) simp_all |
|
31 |
|
32 lemma nat_of_index_inject [simp]: |
|
33 "nat_of_index n = nat_of_index m \<longleftrightarrow> n = m" |
|
34 by (cases n) auto |
31 |
35 |
32 lemma index: |
36 lemma index: |
33 "(\<And>k\<Colon>index. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (index_of_int k))" |
37 "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))" |
34 proof |
38 proof |
35 fix k :: int |
39 fix n :: nat |
36 assume "\<And>k\<Colon>index. PROP P k" |
40 assume "\<And>n\<Colon>index. PROP P n" |
37 then show "PROP P (index_of_int k)" . |
41 then show "PROP P (index_of_nat n)" . |
38 next |
42 next |
39 fix k :: index |
43 fix n :: index |
40 assume "\<And>k\<Colon>int. PROP P (index_of_int k)" |
44 assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)" |
41 then have "PROP P (index_of_int (int_of_index k))" . |
45 then have "PROP P (index_of_nat (nat_of_index n))" . |
42 then show "PROP P k" by simp |
46 then show "PROP P n" by simp |
43 qed |
47 qed |
44 |
48 |
45 lemma [code func]: "size (k\<Colon>index) = 0" |
49 lemma [code func]: "size (n\<Colon>index) = 0" |
46 by (cases k) simp_all |
50 by (cases n) simp_all |
47 |
51 |
48 |
52 |
49 subsection {* Built-in integers as datatype on numerals *} |
53 subsection {* Indices as datatype of ints *} |
50 |
54 |
51 instance index :: number |
55 instantiation index :: number |
52 "number_of \<equiv> index_of_int" .. |
56 begin |
|
57 |
|
58 definition |
|
59 "number_of = index_of_nat o nat" |
|
60 |
|
61 instance .. |
|
62 |
|
63 end |
53 |
64 |
54 code_datatype "number_of \<Colon> int \<Rightarrow> index" |
65 code_datatype "number_of \<Colon> int \<Rightarrow> index" |
55 |
66 |
56 lemma number_of_index_id [simp]: |
|
57 "number_of (int_of_index k) = k" |
|
58 unfolding number_of_index_def by simp |
|
59 |
|
60 lemma number_of_index_shift: |
|
61 "number_of k = index_of_int (number_of k)" |
|
62 by (simp add: number_of_is_id number_of_index_def) |
|
63 |
|
64 lemma int_of_index_number_of [simp]: |
|
65 "int_of_index (number_of k) = number_of k" |
|
66 unfolding number_of_index_def number_of_is_id by simp |
|
67 |
|
68 |
67 |
69 subsection {* Basic arithmetic *} |
68 subsection {* Basic arithmetic *} |
70 |
69 |
71 instance index :: zero |
70 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" |
72 [simp]: "0 \<equiv> index_of_int 0" .. |
71 begin |
73 lemmas [code func del] = zero_index_def |
72 |
74 |
73 definition [simp, code func del]: |
75 instance index :: one |
74 "(0\<Colon>index) = index_of_nat 0" |
76 [simp]: "1 \<equiv> index_of_int 1" .. |
|
77 lemmas [code func del] = one_index_def |
|
78 |
|
79 instance index :: plus |
|
80 [simp]: "k + l \<equiv> index_of_int (int_of_index k + int_of_index l)" .. |
|
81 lemmas [code func del] = plus_index_def |
|
82 lemma plus_index_code [code func]: |
|
83 "index_of_int k + index_of_int l = index_of_int (k + l)" |
|
84 unfolding plus_index_def by simp |
|
85 |
|
86 instance index :: minus |
|
87 [simp]: "- k \<equiv> index_of_int (- int_of_index k)" |
|
88 [simp]: "k - l \<equiv> index_of_int (int_of_index k - int_of_index l)" .. |
|
89 lemmas [code func del] = uminus_index_def minus_index_def |
|
90 lemma uminus_index_code [code func]: |
|
91 "- index_of_int k \<equiv> index_of_int (- k)" |
|
92 unfolding uminus_index_def by simp |
|
93 lemma minus_index_code [code func]: |
|
94 "index_of_int k - index_of_int l = index_of_int (k - l)" |
|
95 unfolding minus_index_def by simp |
|
96 |
|
97 instance index :: times |
|
98 [simp]: "k * l \<equiv> index_of_int (int_of_index k * int_of_index l)" .. |
|
99 lemmas [code func del] = times_index_def |
|
100 lemma times_index_code [code func]: |
|
101 "index_of_int k * index_of_int l = index_of_int (k * l)" |
|
102 unfolding times_index_def by simp |
|
103 |
|
104 instance index :: ord |
|
105 [simp]: "k \<le> l \<equiv> int_of_index k \<le> int_of_index l" |
|
106 [simp]: "k < l \<equiv> int_of_index k < int_of_index l" .. |
|
107 lemmas [code func del] = less_eq_index_def less_index_def |
|
108 lemma less_eq_index_code [code func]: |
|
109 "index_of_int k \<le> index_of_int l \<longleftrightarrow> k \<le> l" |
|
110 unfolding less_eq_index_def by simp |
|
111 lemma less_index_code [code func]: |
|
112 "index_of_int k < index_of_int l \<longleftrightarrow> k < l" |
|
113 unfolding less_index_def by simp |
|
114 |
|
115 instance index :: "Divides.div" |
|
116 [simp]: "k div l \<equiv> index_of_int (int_of_index k div int_of_index l)" |
|
117 [simp]: "k mod l \<equiv> index_of_int (int_of_index k mod int_of_index l)" .. |
|
118 |
|
119 instance index :: ring_1 |
|
120 by default (auto simp add: left_distrib right_distrib) |
|
121 |
|
122 lemma of_nat_index: "of_nat n = index_of_int (of_nat n)" |
|
123 proof (induct n) |
|
124 case 0 show ?case by simp |
|
125 next |
|
126 case (Suc n) |
|
127 then have "int_of_index (index_of_int (int n)) |
|
128 = int_of_index (of_nat n)" by simp |
|
129 then have "int n = int_of_index (of_nat n)" by simp |
|
130 then show ?case by simp |
|
131 qed |
|
132 |
|
133 instance index :: number_ring |
|
134 by default |
|
135 (simp_all add: left_distrib number_of_index_def of_int_of_nat of_nat_index) |
|
136 |
75 |
137 lemma zero_index_code [code inline, code func]: |
76 lemma zero_index_code [code inline, code func]: |
138 "(0\<Colon>index) = Numeral0" |
77 "(0\<Colon>index) = Numeral0" |
139 by simp |
78 by (simp add: number_of_index_def Pls_def) |
|
79 |
|
80 definition [simp, code func del]: |
|
81 "(1\<Colon>index) = index_of_nat 1" |
140 |
82 |
141 lemma one_index_code [code inline, code func]: |
83 lemma one_index_code [code inline, code func]: |
142 "(1\<Colon>index) = Numeral1" |
84 "(1\<Colon>index) = Numeral1" |
143 by simp |
85 by (simp add: number_of_index_def Pls_def Bit_def) |
144 |
86 |
145 instance index :: abs |
87 definition [simp, code func del]: |
146 "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" .. |
88 "n + m = index_of_nat (nat_of_index n + nat_of_index m)" |
147 |
89 |
148 lemma index_of_int [code func]: |
90 lemma plus_index_code [code func]: |
149 "index_of_int k = (if k = 0 then 0 |
91 "index_of_nat n + index_of_nat m = index_of_nat (n + m)" |
150 else if k = -1 then -1 |
92 by simp |
151 else let (l, m) = divAlg (k, 2) in 2 * index_of_int l + |
93 |
152 (if m = 0 then 0 else 1))" |
94 definition [simp, code func del]: |
153 by (simp add: number_of_index_shift Let_def split_def divAlg_mod_div) arith |
95 "n - m = index_of_nat (nat_of_index n - nat_of_index m)" |
154 |
96 |
155 lemma int_of_index [code func]: |
97 definition [simp, code func del]: |
156 "int_of_index k = (if k = 0 then 0 |
98 "n * m = index_of_nat (nat_of_index n * nat_of_index m)" |
157 else if k = -1 then -1 |
99 |
158 else let l = k div 2; m = k mod 2 in 2 * int_of_index l + |
100 lemma times_index_code [code func]: |
159 (if m = 0 then 0 else 1))" |
101 "index_of_nat n * index_of_nat m = index_of_nat (n * m)" |
160 by (auto simp add: number_of_index_shift Let_def split_def) arith |
102 by simp |
161 |
103 |
162 |
104 definition [simp, code func del]: |
163 subsection {* Conversion to and from @{typ nat} *} |
105 "n div m = index_of_nat (nat_of_index n div nat_of_index m)" |
164 |
106 |
165 definition |
107 definition [simp, code func del]: |
166 nat_of_index :: "index \<Rightarrow> nat" |
108 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)" |
167 where |
109 |
168 [code func del]: "nat_of_index = nat o int_of_index" |
110 lemma div_index_code [code func]: |
169 |
111 "index_of_nat n div index_of_nat m = index_of_nat (n div m)" |
170 definition |
112 by simp |
171 nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where |
113 |
172 [code func del]: "nat_of_index_aux i n = nat_of_index i + n" |
114 lemma mod_index_code [code func]: |
173 |
115 "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)" |
174 lemma nat_of_index_aux_code [code]: |
116 by simp |
175 "nat_of_index_aux i n = (if i \<le> 0 then n else nat_of_index_aux (i - 1) (Suc n))" |
117 |
176 by (auto simp add: nat_of_index_aux_def nat_of_index_def) |
118 definition [simp, code func del]: |
177 |
119 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m" |
178 lemma nat_of_index_code [code]: |
120 |
179 "nat_of_index i = nat_of_index_aux i 0" |
121 definition [simp, code func del]: |
180 by (simp add: nat_of_index_aux_def) |
122 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m" |
181 |
123 |
182 definition |
124 lemma less_eq_index_code [code func]: |
183 index_of_nat :: "nat \<Rightarrow> index" |
125 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m" |
184 where |
126 by simp |
185 [code func del]: "index_of_nat = index_of_int o of_nat" |
127 |
186 |
128 lemma less_index_code [code func]: |
187 lemma index_of_nat [code func]: |
129 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m" |
188 "index_of_nat 0 = 0" |
130 by simp |
189 "index_of_nat (Suc n) = index_of_nat n + 1" |
131 |
190 unfolding index_of_nat_def by simp_all |
132 instance by default (auto simp add: left_distrib index) |
191 |
133 |
192 lemma index_nat_id [simp]: |
134 end |
193 "nat_of_index (index_of_nat n) = n" |
|
194 "index_of_nat (nat_of_index i) = (if i \<le> 0 then 0 else i)" |
|
195 unfolding index_of_nat_def nat_of_index_def by simp_all |
|
196 |
135 |
197 |
136 |
198 subsection {* ML interface *} |
137 subsection {* ML interface *} |
199 |
138 |
200 ML {* |
139 ML {* |
201 structure Index = |
140 structure Index = |
202 struct |
141 struct |
203 |
142 |
204 fun mk k = @{term index_of_int} $ HOLogic.mk_number @{typ index} k; |
143 fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k; |
205 |
144 |
206 end; |
145 end; |
207 *} |
146 *} |
208 |
147 |
209 |
148 |
210 subsection {* Code serialization *} |
149 subsection {* Code serialization *} |
|
150 |
|
151 text {* Pecularity for operations with potentially negative result *} |
|
152 |
|
153 definition |
|
154 minus_index' :: "index \<Rightarrow> index \<Rightarrow> index" |
|
155 where |
|
156 [code func del]: "minus_index' = op -" |
|
157 |
|
158 lemma minus_index_code [code func]: |
|
159 "n - m = (let q = minus_index' n m |
|
160 in if q < 0 then 0 else q)" |
|
161 by (simp add: minus_index'_def Let_def) |
|
162 |
|
163 text {* Implementation of indices by bounded integers *} |
211 |
164 |
212 code_type index |
165 code_type index |
213 (SML "int") |
166 (SML "int") |
214 (OCaml "int") |
167 (OCaml "int") |
215 (Haskell "Integer") |
168 (Haskell "Integer") |