author | krauss |
Tue, 28 Sep 2010 09:54:07 +0200 | |
changeset 39754 | 150f831ce4a3 |
parent 39272 | 0b61951d2682 |
child 41228 | e1fce873b814 |
permissions | -rw-r--r-- |
28021 | 1 |
(* Title: HOL/ex/Numeral.thy |
2 |
Author: Florian Haftmann |
|
29947 | 3 |
*) |
28021 | 4 |
|
29947 | 5 |
header {* An experimental alternative numeral representation. *} |
28021 | 6 |
|
7 |
theory Numeral |
|
33346 | 8 |
imports Main |
28021 | 9 |
begin |
10 |
||
11 |
subsection {* The @{text num} type *} |
|
12 |
||
29943 | 13 |
datatype num = One | Dig0 num | Dig1 num |
14 |
||
15 |
text {* Increment function for type @{typ num} *} |
|
16 |
||
31021 | 17 |
primrec inc :: "num \<Rightarrow> num" where |
29943 | 18 |
"inc One = Dig0 One" |
19 |
| "inc (Dig0 x) = Dig1 x" |
|
20 |
| "inc (Dig1 x) = Dig0 (inc x)" |
|
21 |
||
22 |
text {* Converting between type @{typ num} and type @{typ nat} *} |
|
23 |
||
31021 | 24 |
primrec nat_of_num :: "num \<Rightarrow> nat" where |
29943 | 25 |
"nat_of_num One = Suc 0" |
26 |
| "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x" |
|
27 |
| "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)" |
|
28 |
||
31021 | 29 |
primrec num_of_nat :: "nat \<Rightarrow> num" where |
29943 | 30 |
"num_of_nat 0 = One" |
31 |
| "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" |
|
32 |
||
29945 | 33 |
lemma nat_of_num_pos: "0 < nat_of_num x" |
29943 | 34 |
by (induct x) simp_all |
35 |
||
31028 | 36 |
lemma nat_of_num_neq_0: "nat_of_num x \<noteq> 0" |
29943 | 37 |
by (induct x) simp_all |
38 |
||
39 |
lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)" |
|
40 |
by (induct x) simp_all |
|
41 |
||
42 |
lemma num_of_nat_double: |
|
43 |
"0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)" |
|
44 |
by (induct n) simp_all |
|
45 |
||
28021 | 46 |
text {* |
29943 | 47 |
Type @{typ num} is isomorphic to the strictly positive |
28021 | 48 |
natural numbers. |
49 |
*} |
|
50 |
||
29943 | 51 |
lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" |
29945 | 52 |
by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) |
28021 | 53 |
|
29943 | 54 |
lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
55 |
by (induct n) (simp_all add: nat_of_num_inc) |
|
28021 | 56 |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
57 |
lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
58 |
proof |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
59 |
assume "nat_of_num x = nat_of_num y" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
60 |
then have "num_of_nat (nat_of_num x) = num_of_nat (nat_of_num y)" by simp |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
61 |
then show "x = y" by (simp add: nat_of_num_inverse) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
62 |
qed simp |
28021 | 63 |
|
29943 | 64 |
lemma num_induct [case_names One inc]: |
65 |
fixes P :: "num \<Rightarrow> bool" |
|
66 |
assumes One: "P One" |
|
67 |
and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
|
68 |
shows "P x" |
|
69 |
proof - |
|
70 |
obtain n where n: "Suc n = nat_of_num x" |
|
71 |
by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0) |
|
72 |
have "P (num_of_nat (Suc n))" |
|
73 |
proof (induct n) |
|
74 |
case 0 show ?case using One by simp |
|
28021 | 75 |
next |
29943 | 76 |
case (Suc n) |
77 |
then have "P (inc (num_of_nat (Suc n)))" by (rule inc) |
|
78 |
then show "P (num_of_nat (Suc (Suc n)))" by simp |
|
28021 | 79 |
qed |
29943 | 80 |
with n show "P x" |
81 |
by (simp add: nat_of_num_inverse) |
|
28021 | 82 |
qed |
83 |
||
84 |
text {* |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
85 |
From now on, there are two possible models for @{typ num}: as |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
86 |
positive naturals (rule @{text "num_induct"}) and as digit |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
87 |
representation (rules @{text "num.induct"}, @{text "num.cases"}). |
28021 | 88 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
89 |
It is not entirely clear in which context it is better to use the |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
90 |
one or the other, or whether the construction should be reversed. |
28021 | 91 |
*} |
92 |
||
93 |
||
29945 | 94 |
subsection {* Numeral operations *} |
28021 | 95 |
|
96 |
ML {* |
|
31902 | 97 |
structure Dig_Simps = Named_Thms |
98 |
( |
|
99 |
val name = "numeral" |
|
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38054
diff
changeset
|
100 |
val description = "simplification rules for numerals" |
31902 | 101 |
) |
28021 | 102 |
*} |
103 |
||
31902 | 104 |
setup Dig_Simps.setup |
28021 | 105 |
|
29945 | 106 |
instantiation num :: "{plus,times,ord}" |
107 |
begin |
|
28021 | 108 |
|
109 |
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
|
37765 | 110 |
"m + n = num_of_nat (nat_of_num m + nat_of_num n)" |
28021 | 111 |
|
112 |
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
|
37765 | 113 |
"m * n = num_of_nat (nat_of_num m * nat_of_num n)" |
28021 | 114 |
|
29945 | 115 |
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where |
37765 | 116 |
"m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" |
28021 | 117 |
|
29945 | 118 |
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where |
37765 | 119 |
"m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" |
28021 | 120 |
|
29945 | 121 |
instance .. |
28021 | 122 |
|
123 |
end |
|
124 |
||
29945 | 125 |
lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" |
126 |
unfolding plus_num_def |
|
127 |
by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos) |
|
128 |
||
129 |
lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y" |
|
130 |
unfolding times_num_def |
|
131 |
by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos) |
|
28021 | 132 |
|
29945 | 133 |
lemma Dig_plus [numeral, simp, code]: |
134 |
"One + One = Dig0 One" |
|
135 |
"One + Dig0 m = Dig1 m" |
|
136 |
"One + Dig1 m = Dig0 (m + One)" |
|
137 |
"Dig0 n + One = Dig1 n" |
|
138 |
"Dig0 n + Dig0 m = Dig0 (n + m)" |
|
139 |
"Dig0 n + Dig1 m = Dig1 (n + m)" |
|
140 |
"Dig1 n + One = Dig0 (n + One)" |
|
141 |
"Dig1 n + Dig0 m = Dig1 (n + m)" |
|
142 |
"Dig1 n + Dig1 m = Dig0 (n + m + One)" |
|
143 |
by (simp_all add: num_eq_iff nat_of_num_add) |
|
28021 | 144 |
|
29945 | 145 |
lemma Dig_times [numeral, simp, code]: |
146 |
"One * One = One" |
|
147 |
"One * Dig0 n = Dig0 n" |
|
148 |
"One * Dig1 n = Dig1 n" |
|
149 |
"Dig0 n * One = Dig0 n" |
|
150 |
"Dig0 n * Dig0 m = Dig0 (n * Dig0 m)" |
|
151 |
"Dig0 n * Dig1 m = Dig0 (n * Dig1 m)" |
|
152 |
"Dig1 n * One = Dig1 n" |
|
153 |
"Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)" |
|
154 |
"Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)" |
|
155 |
by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult |
|
156 |
left_distrib right_distrib) |
|
28021 | 157 |
|
29945 | 158 |
lemma less_eq_num_code [numeral, simp, code]: |
159 |
"One \<le> n \<longleftrightarrow> True" |
|
160 |
"Dig0 m \<le> One \<longleftrightarrow> False" |
|
161 |
"Dig1 m \<le> One \<longleftrightarrow> False" |
|
162 |
"Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n" |
|
163 |
"Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" |
|
164 |
"Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n" |
|
165 |
"Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n" |
|
166 |
using nat_of_num_pos [of n] nat_of_num_pos [of m] |
|
167 |
by (auto simp add: less_eq_num_def less_num_def) |
|
168 |
||
169 |
lemma less_num_code [numeral, simp, code]: |
|
170 |
"m < One \<longleftrightarrow> False" |
|
171 |
"One < One \<longleftrightarrow> False" |
|
172 |
"One < Dig0 n \<longleftrightarrow> True" |
|
173 |
"One < Dig1 n \<longleftrightarrow> True" |
|
174 |
"Dig0 m < Dig0 n \<longleftrightarrow> m < n" |
|
175 |
"Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n" |
|
176 |
"Dig1 m < Dig1 n \<longleftrightarrow> m < n" |
|
177 |
"Dig1 m < Dig0 n \<longleftrightarrow> m < n" |
|
178 |
using nat_of_num_pos [of n] nat_of_num_pos [of m] |
|
179 |
by (auto simp add: less_eq_num_def less_num_def) |
|
180 |
||
181 |
text {* Rules using @{text One} and @{text inc} as constructors *} |
|
28021 | 182 |
|
29945 | 183 |
lemma add_One: "x + One = inc x" |
184 |
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
|
185 |
||
186 |
lemma add_inc: "x + inc y = inc (x + y)" |
|
187 |
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
|
188 |
||
189 |
lemma mult_One: "x * One = x" |
|
190 |
by (simp add: num_eq_iff nat_of_num_mult) |
|
191 |
||
192 |
lemma mult_inc: "x * inc y = x * y + x" |
|
193 |
by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) |
|
194 |
||
195 |
text {* A double-and-decrement function *} |
|
28021 | 196 |
|
29945 | 197 |
primrec DigM :: "num \<Rightarrow> num" where |
198 |
"DigM One = One" |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
199 |
| "DigM (Dig0 n) = Dig1 (DigM n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
200 |
| "DigM (Dig1 n) = Dig1 (Dig0 n)" |
28021 | 201 |
|
29945 | 202 |
lemma DigM_plus_one: "DigM n + One = Dig0 n" |
203 |
by (induct n) simp_all |
|
204 |
||
205 |
lemma add_One_commute: "One + n = n + One" |
|
206 |
by (induct n) simp_all |
|
207 |
||
208 |
lemma one_plus_DigM: "One + DigM n = Dig0 n" |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
209 |
by (simp add: add_One_commute DigM_plus_one) |
28021 | 210 |
|
29954 | 211 |
text {* Squaring and exponentiation *} |
29947 | 212 |
|
213 |
primrec square :: "num \<Rightarrow> num" where |
|
214 |
"square One = One" |
|
215 |
| "square (Dig0 n) = Dig0 (Dig0 (square n))" |
|
216 |
| "square (Dig1 n) = Dig1 (Dig0 (square n + n))" |
|
217 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
218 |
primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where |
29954 | 219 |
"pow x One = x" |
220 |
| "pow x (Dig0 y) = square (pow x y)" |
|
221 |
| "pow x (Dig1 y) = x * square (pow x y)" |
|
29947 | 222 |
|
28021 | 223 |
|
224 |
subsection {* Binary numerals *} |
|
225 |
||
226 |
text {* |
|
227 |
We embed binary representations into a generic algebraic |
|
29934 | 228 |
structure using @{text of_num}. |
28021 | 229 |
*} |
230 |
||
231 |
class semiring_numeral = semiring + monoid_mult |
|
232 |
begin |
|
233 |
||
234 |
primrec of_num :: "num \<Rightarrow> 'a" where |
|
31028 | 235 |
of_num_One [numeral]: "of_num One = 1" |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
236 |
| "of_num (Dig0 n) = of_num n + of_num n" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
237 |
| "of_num (Dig1 n) = of_num n + of_num n + 1" |
28021 | 238 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
239 |
lemma of_num_inc: "of_num (inc n) = of_num n + 1" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
240 |
by (induct n) (simp_all add: add_ac) |
29943 | 241 |
|
31028 | 242 |
lemma of_num_add: "of_num (m + n) = of_num m + of_num n" |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
243 |
by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac) |
31028 | 244 |
|
245 |
lemma of_num_mult: "of_num (m * n) = of_num m * of_num n" |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
246 |
by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib) |
31028 | 247 |
|
28021 | 248 |
declare of_num.simps [simp del] |
249 |
||
250 |
end |
|
251 |
||
252 |
ML {* |
|
31027 | 253 |
fun mk_num k = |
254 |
if k > 1 then |
|
255 |
let |
|
256 |
val (l, b) = Integer.div_mod k 2; |
|
257 |
val bit = (if b = 0 then @{term Dig0} else @{term Dig1}); |
|
258 |
in bit $ (mk_num l) end |
|
259 |
else if k = 1 then @{term One} |
|
260 |
else error ("mk_num " ^ string_of_int k); |
|
28021 | 261 |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
262 |
fun dest_num @{term One} = 1 |
28021 | 263 |
| dest_num (@{term Dig0} $ n) = 2 * dest_num n |
31027 | 264 |
| dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1 |
265 |
| dest_num t = raise TERM ("dest_num", [t]); |
|
28021 | 266 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
267 |
fun mk_numeral phi T k = Morphism.term phi (Const (@{const_name of_num}, @{typ num} --> T)) |
28021 | 268 |
$ mk_num k |
269 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
270 |
fun dest_numeral phi (u $ t) = |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
271 |
if Term.aconv_untyped (u, Morphism.term phi (Const (@{const_name of_num}, dummyT))) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
272 |
then (range_type (fastype_of u), dest_num t) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
273 |
else raise TERM ("dest_numeral", [u, t]); |
28021 | 274 |
*} |
275 |
||
276 |
syntax |
|
277 |
"_Numerals" :: "xnum \<Rightarrow> 'a" ("_") |
|
278 |
||
279 |
parse_translation {* |
|
280 |
let |
|
281 |
fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2) |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
282 |
of (0, 1) => Const (@{const_name One}, dummyT) |
28021 | 283 |
| (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n |
284 |
| (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n |
|
285 |
else raise Match; |
|
286 |
fun numeral_tr [Free (num, _)] = |
|
287 |
let |
|
288 |
val {leading_zeros, value, ...} = Syntax.read_xnum num; |
|
289 |
val _ = leading_zeros = 0 andalso value > 0 |
|
290 |
orelse error ("Bad numeral: " ^ num); |
|
291 |
in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end |
|
292 |
| numeral_tr ts = raise TERM ("numeral_tr", ts); |
|
35113 | 293 |
in [(@{syntax_const "_Numerals"}, numeral_tr)] end |
28021 | 294 |
*} |
295 |
||
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
296 |
typed_print_translation (advanced) {* |
28021 | 297 |
let |
298 |
fun dig b n = b + 2 * n; |
|
299 |
fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) = |
|
300 |
dig 0 (int_of_num' n) |
|
301 |
| int_of_num' (Const (@{const_syntax Dig1}, _) $ n) = |
|
302 |
dig 1 (int_of_num' n) |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
303 |
| int_of_num' (Const (@{const_syntax One}, _)) = 1; |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
304 |
fun num_tr' ctxt show_sorts T [n] = |
28021 | 305 |
let |
306 |
val k = int_of_num' n; |
|
35113 | 307 |
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k); |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
308 |
in |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
309 |
case T of |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
310 |
Type (@{type_name fun}, [_, T']) => |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
311 |
if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t' |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38923
diff
changeset
|
312 |
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T' |
28021 | 313 |
| T' => if T' = dummyT then t' else raise Match |
314 |
end; |
|
315 |
in [(@{const_syntax of_num}, num_tr')] end |
|
316 |
*} |
|
317 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
318 |
|
29945 | 319 |
subsection {* Class-specific numeral rules *} |
28021 | 320 |
|
29945 | 321 |
subsubsection {* Class @{text semiring_numeral} *} |
322 |
||
28021 | 323 |
context semiring_numeral |
324 |
begin |
|
325 |
||
29943 | 326 |
abbreviation "Num1 \<equiv> of_num One" |
28021 | 327 |
|
328 |
text {* |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
329 |
Alas, there is still the duplication of @{term 1}, although the |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
330 |
duplicated @{term 0} has disappeared. We could get rid of it by |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
331 |
replacing the constructor @{term 1} in @{typ num} by two |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
332 |
constructors @{text two} and @{text three}, resulting in a further |
28021 | 333 |
blow-up. But it could be worth the effort. |
334 |
*} |
|
335 |
||
336 |
lemma of_num_plus_one [numeral]: |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
337 |
"of_num n + 1 = of_num (n + One)" |
31028 | 338 |
by (simp only: of_num_add of_num_One) |
28021 | 339 |
|
340 |
lemma of_num_one_plus [numeral]: |
|
31028 | 341 |
"1 + of_num n = of_num (One + n)" |
342 |
by (simp only: of_num_add of_num_One) |
|
28021 | 343 |
|
344 |
lemma of_num_plus [numeral]: |
|
345 |
"of_num m + of_num n = of_num (m + n)" |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
346 |
by (simp only: of_num_add) |
28021 | 347 |
|
348 |
lemma of_num_times_one [numeral]: |
|
349 |
"of_num n * 1 = of_num n" |
|
350 |
by simp |
|
351 |
||
352 |
lemma of_num_one_times [numeral]: |
|
353 |
"1 * of_num n = of_num n" |
|
354 |
by simp |
|
355 |
||
356 |
lemma of_num_times [numeral]: |
|
357 |
"of_num m * of_num n = of_num (m * n)" |
|
31028 | 358 |
unfolding of_num_mult .. |
28021 | 359 |
|
360 |
end |
|
361 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
362 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
363 |
subsubsection {* Structures with a zero: class @{text semiring_1} *} |
28021 | 364 |
|
365 |
context semiring_1 |
|
366 |
begin |
|
367 |
||
368 |
subclass semiring_numeral .. |
|
369 |
||
370 |
lemma of_nat_of_num [numeral]: "of_nat (of_num n) = of_num n" |
|
371 |
by (induct n) |
|
372 |
(simp_all add: semiring_numeral_class.of_num.simps of_num.simps add_ac) |
|
373 |
||
374 |
declare of_nat_1 [numeral] |
|
375 |
||
376 |
lemma Dig_plus_zero [numeral]: |
|
377 |
"0 + 1 = 1" |
|
378 |
"0 + of_num n = of_num n" |
|
379 |
"1 + 0 = 1" |
|
380 |
"of_num n + 0 = of_num n" |
|
381 |
by simp_all |
|
382 |
||
383 |
lemma Dig_times_zero [numeral]: |
|
384 |
"0 * 1 = 0" |
|
385 |
"0 * of_num n = 0" |
|
386 |
"1 * 0 = 0" |
|
387 |
"of_num n * 0 = 0" |
|
388 |
by simp_all |
|
389 |
||
390 |
end |
|
391 |
||
392 |
lemma nat_of_num_of_num: "nat_of_num = of_num" |
|
393 |
proof |
|
394 |
fix n |
|
29943 | 395 |
have "of_num n = nat_of_num n" |
396 |
by (induct n) (simp_all add: of_num.simps) |
|
28021 | 397 |
then show "nat_of_num n = of_num n" by simp |
398 |
qed |
|
399 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
400 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
401 |
subsubsection {* Equality: class @{text semiring_char_0} *} |
28021 | 402 |
|
403 |
context semiring_char_0 |
|
404 |
begin |
|
405 |
||
31028 | 406 |
lemma of_num_eq_iff [numeral]: "of_num m = of_num n \<longleftrightarrow> m = n" |
28021 | 407 |
unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric] |
29943 | 408 |
of_nat_eq_iff num_eq_iff .. |
28021 | 409 |
|
31028 | 410 |
lemma of_num_eq_one_iff [numeral]: "of_num n = 1 \<longleftrightarrow> n = One" |
411 |
using of_num_eq_iff [of n One] by (simp add: of_num_One) |
|
28021 | 412 |
|
31028 | 413 |
lemma one_eq_of_num_iff [numeral]: "1 = of_num n \<longleftrightarrow> One = n" |
414 |
using of_num_eq_iff [of One n] by (simp add: of_num_One) |
|
28021 | 415 |
|
416 |
end |
|
417 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
418 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
419 |
subsubsection {* Comparisons: class @{text linordered_semidom} *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
420 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
421 |
text {* |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
422 |
Perhaps the underlying structure could even |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
423 |
be more general than @{text linordered_semidom}. |
28021 | 424 |
*} |
425 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
426 |
context linordered_semidom |
28021 | 427 |
begin |
428 |
||
29991 | 429 |
lemma of_num_pos [numeral]: "0 < of_num n" |
430 |
by (induct n) (simp_all add: of_num.simps add_pos_pos) |
|
431 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
432 |
lemma of_num_not_zero [numeral]: "of_num n \<noteq> 0" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
433 |
using of_num_pos [of n] by simp |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
434 |
|
28021 | 435 |
lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n" |
436 |
proof - |
|
437 |
have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n" |
|
438 |
unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff .. |
|
439 |
then show ?thesis by (simp add: of_nat_of_num) |
|
440 |
qed |
|
441 |
||
31028 | 442 |
lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n \<le> One" |
443 |
using of_num_less_eq_iff [of n One] by (simp add: of_num_One) |
|
28021 | 444 |
|
445 |
lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n" |
|
31028 | 446 |
using of_num_less_eq_iff [of One n] by (simp add: of_num_One) |
28021 | 447 |
|
448 |
lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n" |
|
449 |
proof - |
|
450 |
have "of_nat (of_num m) < of_nat (of_num n) \<longleftrightarrow> m < n" |
|
451 |
unfolding less_num_def nat_of_num_of_num of_nat_less_iff .. |
|
452 |
then show ?thesis by (simp add: of_nat_of_num) |
|
453 |
qed |
|
454 |
||
455 |
lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1" |
|
31028 | 456 |
using of_num_less_iff [of n One] by (simp add: of_num_One) |
28021 | 457 |
|
31028 | 458 |
lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> One < n" |
459 |
using of_num_less_iff [of One n] by (simp add: of_num_One) |
|
28021 | 460 |
|
29991 | 461 |
lemma of_num_nonneg [numeral]: "0 \<le> of_num n" |
462 |
by (induct n) (simp_all add: of_num.simps add_nonneg_nonneg) |
|
463 |
||
464 |
lemma of_num_less_zero_iff [numeral]: "\<not> of_num n < 0" |
|
465 |
by (simp add: not_less of_num_nonneg) |
|
466 |
||
467 |
lemma of_num_le_zero_iff [numeral]: "\<not> of_num n \<le> 0" |
|
468 |
by (simp add: not_le of_num_pos) |
|
469 |
||
470 |
end |
|
471 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
472 |
context linordered_idom |
29991 | 473 |
begin |
474 |
||
30792 | 475 |
lemma minus_of_num_less_of_num_iff: "- of_num m < of_num n" |
29991 | 476 |
proof - |
477 |
have "- of_num m < 0" by (simp add: of_num_pos) |
|
478 |
also have "0 < of_num n" by (simp add: of_num_pos) |
|
479 |
finally show ?thesis . |
|
480 |
qed |
|
481 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
482 |
lemma minus_of_num_not_equal_of_num: "- of_num m \<noteq> of_num n" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
483 |
using minus_of_num_less_of_num_iff [of m n] by simp |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
484 |
|
30792 | 485 |
lemma minus_of_num_less_one_iff: "- of_num n < 1" |
31028 | 486 |
using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One) |
29991 | 487 |
|
30792 | 488 |
lemma minus_one_less_of_num_iff: "- 1 < of_num n" |
31028 | 489 |
using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_One) |
29991 | 490 |
|
30792 | 491 |
lemma minus_one_less_one_iff: "- 1 < 1" |
31028 | 492 |
using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_One) |
30792 | 493 |
|
494 |
lemma minus_of_num_le_of_num_iff: "- of_num m \<le> of_num n" |
|
29991 | 495 |
by (simp add: less_imp_le minus_of_num_less_of_num_iff) |
496 |
||
30792 | 497 |
lemma minus_of_num_le_one_iff: "- of_num n \<le> 1" |
29991 | 498 |
by (simp add: less_imp_le minus_of_num_less_one_iff) |
499 |
||
30792 | 500 |
lemma minus_one_le_of_num_iff: "- 1 \<le> of_num n" |
29991 | 501 |
by (simp add: less_imp_le minus_one_less_of_num_iff) |
502 |
||
30792 | 503 |
lemma minus_one_le_one_iff: "- 1 \<le> 1" |
504 |
by (simp add: less_imp_le minus_one_less_one_iff) |
|
505 |
||
506 |
lemma of_num_le_minus_of_num_iff: "\<not> of_num m \<le> - of_num n" |
|
29991 | 507 |
by (simp add: not_le minus_of_num_less_of_num_iff) |
508 |
||
30792 | 509 |
lemma one_le_minus_of_num_iff: "\<not> 1 \<le> - of_num n" |
29991 | 510 |
by (simp add: not_le minus_of_num_less_one_iff) |
511 |
||
30792 | 512 |
lemma of_num_le_minus_one_iff: "\<not> of_num n \<le> - 1" |
29991 | 513 |
by (simp add: not_le minus_one_less_of_num_iff) |
514 |
||
30792 | 515 |
lemma one_le_minus_one_iff: "\<not> 1 \<le> - 1" |
516 |
by (simp add: not_le minus_one_less_one_iff) |
|
517 |
||
518 |
lemma of_num_less_minus_of_num_iff: "\<not> of_num m < - of_num n" |
|
29991 | 519 |
by (simp add: not_less minus_of_num_le_of_num_iff) |
520 |
||
30792 | 521 |
lemma one_less_minus_of_num_iff: "\<not> 1 < - of_num n" |
29991 | 522 |
by (simp add: not_less minus_of_num_le_one_iff) |
523 |
||
30792 | 524 |
lemma of_num_less_minus_one_iff: "\<not> of_num n < - 1" |
29991 | 525 |
by (simp add: not_less minus_one_le_of_num_iff) |
526 |
||
30792 | 527 |
lemma one_less_minus_one_iff: "\<not> 1 < - 1" |
528 |
by (simp add: not_less minus_one_le_one_iff) |
|
529 |
||
530 |
lemmas le_signed_numeral_special [numeral] = |
|
531 |
minus_of_num_le_of_num_iff |
|
532 |
minus_of_num_le_one_iff |
|
533 |
minus_one_le_of_num_iff |
|
534 |
minus_one_le_one_iff |
|
535 |
of_num_le_minus_of_num_iff |
|
536 |
one_le_minus_of_num_iff |
|
537 |
of_num_le_minus_one_iff |
|
538 |
one_le_minus_one_iff |
|
539 |
||
540 |
lemmas less_signed_numeral_special [numeral] = |
|
541 |
minus_of_num_less_of_num_iff |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
542 |
minus_of_num_not_equal_of_num |
30792 | 543 |
minus_of_num_less_one_iff |
544 |
minus_one_less_of_num_iff |
|
545 |
minus_one_less_one_iff |
|
546 |
of_num_less_minus_of_num_iff |
|
547 |
one_less_minus_of_num_iff |
|
548 |
of_num_less_minus_one_iff |
|
549 |
one_less_minus_one_iff |
|
550 |
||
28021 | 551 |
end |
552 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
553 |
subsubsection {* Structures with subtraction: class @{text semiring_1_minus} *} |
28021 | 554 |
|
555 |
class semiring_minus = semiring + minus + zero + |
|
556 |
assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a" |
|
557 |
assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a" |
|
558 |
begin |
|
559 |
||
560 |
lemma minus_inverts_plus2: "a + b = c \<Longrightarrow> c - a = b" |
|
561 |
by (simp add: add_ac minus_inverts_plus1 [of b a]) |
|
562 |
||
563 |
lemma minus_minus_zero_inverts_plus2: "a + b = c \<Longrightarrow> a - c = 0 - b" |
|
564 |
by (simp add: add_ac minus_minus_zero_inverts_plus1 [of b a]) |
|
565 |
||
566 |
end |
|
567 |
||
568 |
class semiring_1_minus = semiring_1 + semiring_minus |
|
569 |
begin |
|
570 |
||
571 |
lemma Dig_of_num_pos: |
|
572 |
assumes "k + n = m" |
|
573 |
shows "of_num m - of_num n = of_num k" |
|
574 |
using assms by (simp add: of_num_plus minus_inverts_plus1) |
|
575 |
||
576 |
lemma Dig_of_num_zero: |
|
577 |
shows "of_num n - of_num n = 0" |
|
578 |
by (rule minus_inverts_plus1) simp |
|
579 |
||
580 |
lemma Dig_of_num_neg: |
|
581 |
assumes "k + m = n" |
|
582 |
shows "of_num m - of_num n = 0 - of_num k" |
|
583 |
by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms) |
|
584 |
||
585 |
lemmas Dig_plus_eval = |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
586 |
of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject |
28021 | 587 |
|
588 |
simproc_setup numeral_minus ("of_num m - of_num n") = {* |
|
589 |
let |
|
590 |
(*TODO proper implicit use of morphism via pattern antiquotations*) |
|
591 |
fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct; |
|
592 |
fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n); |
|
593 |
fun attach_num ct = (dest_num (Thm.term_of ct), ct); |
|
594 |
fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t; |
|
595 |
val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
596 |
fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
597 |
OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"}, |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
598 |
[Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]]; |
28021 | 599 |
in fn phi => fn _ => fn ct => case try cdifference ct |
600 |
of NONE => (NONE) |
|
601 |
| SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0 |
|
602 |
then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct |
|
603 |
else mk_meta_eq (let |
|
604 |
val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j)); |
|
605 |
in |
|
606 |
(if j > 0 then (Morphism.thm phi @{thm Dig_of_num_pos}) OF [cert cj cl ck] |
|
607 |
else (Morphism.thm phi @{thm Dig_of_num_neg}) OF [cert cj ck cl]) |
|
608 |
end) end) |
|
609 |
end |
|
610 |
*} |
|
611 |
||
612 |
lemma Dig_of_num_minus_zero [numeral]: |
|
613 |
"of_num n - 0 = of_num n" |
|
614 |
by (simp add: minus_inverts_plus1) |
|
615 |
||
616 |
lemma Dig_one_minus_zero [numeral]: |
|
617 |
"1 - 0 = 1" |
|
618 |
by (simp add: minus_inverts_plus1) |
|
619 |
||
620 |
lemma Dig_one_minus_one [numeral]: |
|
621 |
"1 - 1 = 0" |
|
622 |
by (simp add: minus_inverts_plus1) |
|
623 |
||
624 |
lemma Dig_of_num_minus_one [numeral]: |
|
29941 | 625 |
"of_num (Dig0 n) - 1 = of_num (DigM n)" |
28021 | 626 |
"of_num (Dig1 n) - 1 = of_num (Dig0 n)" |
29941 | 627 |
by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) |
28021 | 628 |
|
629 |
lemma Dig_one_minus_of_num [numeral]: |
|
29941 | 630 |
"1 - of_num (Dig0 n) = 0 - of_num (DigM n)" |
28021 | 631 |
"1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)" |
29941 | 632 |
by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) |
28021 | 633 |
|
634 |
end |
|
635 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
636 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
637 |
subsubsection {* Structures with negation: class @{text ring_1} *} |
29945 | 638 |
|
28021 | 639 |
context ring_1 |
640 |
begin |
|
641 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
642 |
subclass semiring_1_minus proof |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
643 |
qed (simp_all add: algebra_simps) |
28021 | 644 |
|
645 |
lemma Dig_zero_minus_of_num [numeral]: |
|
646 |
"0 - of_num n = - of_num n" |
|
647 |
by simp |
|
648 |
||
649 |
lemma Dig_zero_minus_one [numeral]: |
|
650 |
"0 - 1 = - 1" |
|
651 |
by simp |
|
652 |
||
653 |
lemma Dig_uminus_uminus [numeral]: |
|
654 |
"- (- of_num n) = of_num n" |
|
655 |
by simp |
|
656 |
||
657 |
lemma Dig_plus_uminus [numeral]: |
|
658 |
"of_num m + - of_num n = of_num m - of_num n" |
|
659 |
"- of_num m + of_num n = of_num n - of_num m" |
|
660 |
"- of_num m + - of_num n = - (of_num m + of_num n)" |
|
661 |
"of_num m - - of_num n = of_num m + of_num n" |
|
662 |
"- of_num m - of_num n = - (of_num m + of_num n)" |
|
663 |
"- of_num m - - of_num n = of_num n - of_num m" |
|
664 |
by (simp_all add: diff_minus add_commute) |
|
665 |
||
666 |
lemma Dig_times_uminus [numeral]: |
|
667 |
"- of_num n * of_num m = - (of_num n * of_num m)" |
|
668 |
"of_num n * - of_num m = - (of_num n * of_num m)" |
|
669 |
"- of_num n * - of_num m = of_num n * of_num m" |
|
31028 | 670 |
by simp_all |
28021 | 671 |
|
672 |
lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n" |
|
673 |
by (induct n) |
|
674 |
(simp_all only: of_num.simps semiring_numeral_class.of_num.simps of_int_add, simp_all) |
|
675 |
||
676 |
declare of_int_1 [numeral] |
|
677 |
||
678 |
end |
|
679 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
680 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
681 |
subsubsection {* Structures with exponentiation *} |
29954 | 682 |
|
683 |
lemma of_num_square: "of_num (square x) = of_num x * of_num x" |
|
684 |
by (induct x) |
|
31028 | 685 |
(simp_all add: of_num.simps of_num_add algebra_simps) |
29954 | 686 |
|
31028 | 687 |
lemma of_num_pow: "of_num (pow x y) = of_num x ^ of_num y" |
29954 | 688 |
by (induct y) |
31028 | 689 |
(simp_all add: of_num.simps of_num_square of_num_mult power_add) |
29954 | 690 |
|
31028 | 691 |
lemma power_of_num [numeral]: "of_num x ^ of_num y = of_num (pow x y)" |
692 |
unfolding of_num_pow .. |
|
29954 | 693 |
|
694 |
lemma power_zero_of_num [numeral]: |
|
31029 | 695 |
"0 ^ of_num n = (0::'a::semiring_1)" |
29954 | 696 |
using of_num_pos [where n=n and ?'a=nat] |
697 |
by (simp add: power_0_left) |
|
698 |
||
699 |
lemma power_minus_Dig0 [numeral]: |
|
31029 | 700 |
fixes x :: "'a::ring_1" |
29954 | 701 |
shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)" |
31028 | 702 |
by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) |
29954 | 703 |
|
704 |
lemma power_minus_Dig1 [numeral]: |
|
31029 | 705 |
fixes x :: "'a::ring_1" |
29954 | 706 |
shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))" |
31028 | 707 |
by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) |
29954 | 708 |
|
709 |
declare power_one [numeral] |
|
710 |
||
711 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
712 |
subsubsection {* Greetings to @{typ nat}. *} |
28021 | 713 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
714 |
instance nat :: semiring_1_minus proof |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
715 |
qed simp_all |
28021 | 716 |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
717 |
lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)" |
28021 | 718 |
unfolding of_num_plus_one [symmetric] by simp |
719 |
||
720 |
lemma nat_number: |
|
721 |
"1 = Suc 0" |
|
29942
31069b8d39df
replace 1::num with One; remove monoid_mult instance
huffman
parents:
29941
diff
changeset
|
722 |
"of_num One = Suc 0" |
29941 | 723 |
"of_num (Dig0 n) = Suc (of_num (DigM n))" |
28021 | 724 |
"of_num (Dig1 n) = Suc (of_num (Dig0 n))" |
29941 | 725 |
by (simp_all add: of_num.simps DigM_plus_one Suc_of_num) |
28021 | 726 |
|
727 |
declare diff_0_eq_0 [numeral] |
|
728 |
||
729 |
||
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
730 |
subsection {* Proof tools setup *} |
28021 | 731 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
732 |
subsubsection {* Numeral equations as default simplification rules *} |
28021 | 733 |
|
31029 | 734 |
declare (in semiring_numeral) of_num_One [simp] |
735 |
declare (in semiring_numeral) of_num_plus_one [simp] |
|
736 |
declare (in semiring_numeral) of_num_one_plus [simp] |
|
737 |
declare (in semiring_numeral) of_num_plus [simp] |
|
738 |
declare (in semiring_numeral) of_num_times [simp] |
|
739 |
||
740 |
declare (in semiring_1) of_nat_of_num [simp] |
|
741 |
||
742 |
declare (in semiring_char_0) of_num_eq_iff [simp] |
|
743 |
declare (in semiring_char_0) of_num_eq_one_iff [simp] |
|
744 |
declare (in semiring_char_0) one_eq_of_num_iff [simp] |
|
745 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
746 |
declare (in linordered_semidom) of_num_pos [simp] |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
747 |
declare (in linordered_semidom) of_num_not_zero [simp] |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
748 |
declare (in linordered_semidom) of_num_less_eq_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
749 |
declare (in linordered_semidom) of_num_less_eq_one_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
750 |
declare (in linordered_semidom) one_less_eq_of_num_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
751 |
declare (in linordered_semidom) of_num_less_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
752 |
declare (in linordered_semidom) of_num_less_one_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
753 |
declare (in linordered_semidom) one_less_of_num_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
754 |
declare (in linordered_semidom) of_num_nonneg [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
755 |
declare (in linordered_semidom) of_num_less_zero_iff [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
756 |
declare (in linordered_semidom) of_num_le_zero_iff [simp] |
31029 | 757 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
758 |
declare (in linordered_idom) le_signed_numeral_special [simp] |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33523
diff
changeset
|
759 |
declare (in linordered_idom) less_signed_numeral_special [simp] |
31029 | 760 |
|
761 |
declare (in semiring_1_minus) Dig_of_num_minus_one [simp] |
|
762 |
declare (in semiring_1_minus) Dig_one_minus_of_num [simp] |
|
763 |
||
764 |
declare (in ring_1) Dig_plus_uminus [simp] |
|
765 |
declare (in ring_1) of_int_of_num [simp] |
|
766 |
||
767 |
declare power_of_num [simp] |
|
768 |
declare power_zero_of_num [simp] |
|
769 |
declare power_minus_Dig0 [simp] |
|
770 |
declare power_minus_Dig1 [simp] |
|
771 |
||
772 |
declare Suc_of_num [simp] |
|
773 |
||
28021 | 774 |
|
31026
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
775 |
subsubsection {* Reorientation of equalities *} |
31025 | 776 |
|
777 |
setup {* |
|
33523 | 778 |
Reorient_Proc.add |
31025 | 779 |
(fn Const(@{const_name of_num}, _) $ _ => true |
780 |
| Const(@{const_name uminus}, _) $ |
|
781 |
(Const(@{const_name of_num}, _) $ _) => true |
|
782 |
| _ => false) |
|
783 |
*} |
|
784 |
||
33523 | 785 |
simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = Reorient_Proc.proc |
786 |
||
31025 | 787 |
|
31026
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
788 |
subsubsection {* Constant folding for multiplication in semirings *} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
789 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
790 |
context semiring_numeral |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
791 |
begin |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
792 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
793 |
lemma mult_of_num_commute: "x * of_num n = of_num n * x" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
794 |
by (induct n) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
795 |
(simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
796 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
797 |
definition |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
798 |
"commutes_with a b \<longleftrightarrow> a * b = b * a" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
799 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
800 |
lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
801 |
unfolding commutes_with_def . |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
802 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
803 |
lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
804 |
unfolding commutes_with_def by (simp only: mult_assoc [symmetric]) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
805 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
806 |
lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x" |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
807 |
unfolding commutes_with_def by (simp_all add: mult_of_num_commute) |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
808 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
809 |
lemmas mult_ac_numeral = |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
810 |
mult_assoc |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
811 |
commutes_with_commute |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
812 |
commutes_with_left_commute |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
813 |
commutes_with_numeral |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
814 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
815 |
end |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
816 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
817 |
ML {* |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
818 |
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
819 |
struct |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
820 |
val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
821 |
val eq_reflection = eq_reflection |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
822 |
fun is_numeral (Const(@{const_name of_num}, _) $ _) = true |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
823 |
| is_numeral _ = false; |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
824 |
end; |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
825 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
826 |
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
827 |
*} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
828 |
|
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
829 |
simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") = |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
830 |
{* fn phi => fn ss => fn ct => |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
831 |
Semiring_Times_Assoc.proc ss (Thm.term_of ct) *} |
020efcbfe2d8
add semiring_assoc_fold simproc for unsigned numerals
huffman
parents:
31025
diff
changeset
|
832 |
|
31025 | 833 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
834 |
subsection {* Code generator setup for @{typ int} *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
835 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
836 |
text {* Reversing standard setup *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
837 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
838 |
lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
839 |
lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
840 |
declare zero_is_num_zero [code_unfold del] |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
841 |
declare one_is_num_one [code_unfold del] |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
842 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
843 |
lemma [code, code del]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
844 |
"(1 :: int) = 1" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
845 |
"(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
846 |
"(uminus :: int \<Rightarrow> int) = uminus" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
847 |
"(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
848 |
"(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *" |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
849 |
"(HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool) = HOL.equal" |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
850 |
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
851 |
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
852 |
by rule+ |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
853 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
854 |
text {* Constructors *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
855 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
856 |
definition Pls :: "num \<Rightarrow> int" where |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
857 |
[simp, code_post]: "Pls n = of_num n" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
858 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
859 |
definition Mns :: "num \<Rightarrow> int" where |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
860 |
[simp, code_post]: "Mns n = - of_num n" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
861 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
862 |
code_datatype "0::int" Pls Mns |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
863 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
864 |
lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric] |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
865 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
866 |
text {* Auxiliary operations *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
867 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
868 |
definition dup :: "int \<Rightarrow> int" where |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
869 |
[simp]: "dup k = k + k" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
870 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
871 |
lemma Dig_dup [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
872 |
"dup 0 = 0" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
873 |
"dup (Pls n) = Pls (Dig0 n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
874 |
"dup (Mns n) = Mns (Dig0 n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
875 |
by (simp_all add: of_num.simps) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
876 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
877 |
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
878 |
[simp]: "sub m n = (of_num m - of_num n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
879 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
880 |
lemma Dig_sub [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
881 |
"sub One One = 0" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
882 |
"sub (Dig0 m) One = of_num (DigM m)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
883 |
"sub (Dig1 m) One = of_num (Dig0 m)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
884 |
"sub One (Dig0 n) = - of_num (DigM n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
885 |
"sub One (Dig1 n) = - of_num (Dig0 n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
886 |
"sub (Dig0 m) (Dig0 n) = dup (sub m n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
887 |
"sub (Dig1 m) (Dig1 n) = dup (sub m n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
888 |
"sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
889 |
"sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
890 |
by (simp_all add: algebra_simps num_eq_iff nat_of_num_add) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
891 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
892 |
text {* Implementations *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
893 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
894 |
lemma one_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
895 |
"1 = Pls One" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
896 |
by (simp add: of_num_One) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
897 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
898 |
lemma plus_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
899 |
"k + 0 = (k::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
900 |
"0 + l = (l::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
901 |
"Pls m + Pls n = Pls (m + n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
902 |
"Pls m + Mns n = sub m n" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
903 |
"Mns m + Pls n = sub n m" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
904 |
"Mns m + Mns n = Mns (m + n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
905 |
by simp_all |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
906 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
907 |
lemma uminus_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
908 |
"uminus 0 = (0::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
909 |
"uminus (Pls m) = Mns m" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
910 |
"uminus (Mns m) = Pls m" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
911 |
by simp_all |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
912 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
913 |
lemma minus_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
914 |
"k - 0 = (k::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
915 |
"0 - l = uminus (l::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
916 |
"Pls m - Pls n = sub m n" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
917 |
"Pls m - Mns n = Pls (m + n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
918 |
"Mns m - Pls n = Mns (m + n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
919 |
"Mns m - Mns n = sub n m" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
920 |
by simp_all |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
921 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
922 |
lemma times_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
923 |
"k * 0 = (0::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
924 |
"0 * l = (0::int)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
925 |
"Pls m * Pls n = Pls (m * n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
926 |
"Pls m * Mns n = Mns (m * n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
927 |
"Mns m * Pls n = Mns (m * n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
928 |
"Mns m * Mns n = Pls (m * n)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
929 |
by simp_all |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
930 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
931 |
lemma eq_int_code [code]: |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
932 |
"HOL.equal 0 (0::int) \<longleftrightarrow> True" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
933 |
"HOL.equal 0 (Pls l) \<longleftrightarrow> False" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
934 |
"HOL.equal 0 (Mns l) \<longleftrightarrow> False" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
935 |
"HOL.equal (Pls k) 0 \<longleftrightarrow> False" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
936 |
"HOL.equal (Pls k) (Pls l) \<longleftrightarrow> HOL.equal k l" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
937 |
"HOL.equal (Pls k) (Mns l) \<longleftrightarrow> False" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
938 |
"HOL.equal (Mns k) 0 \<longleftrightarrow> False" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
939 |
"HOL.equal (Mns k) (Pls l) \<longleftrightarrow> False" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
940 |
"HOL.equal (Mns k) (Mns l) \<longleftrightarrow> HOL.equal k l" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
941 |
by (auto simp add: equal dest: sym) |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
942 |
|
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
943 |
lemma [code nbe]: |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
944 |
"HOL.equal (k::int) k \<longleftrightarrow> True" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
945 |
by (fact equal_refl) |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
946 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
947 |
lemma less_eq_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
948 |
"0 \<le> (0::int) \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
949 |
"0 \<le> Pls l \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
950 |
"0 \<le> Mns l \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
951 |
"Pls k \<le> 0 \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
952 |
"Pls k \<le> Pls l \<longleftrightarrow> k \<le> l" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
953 |
"Pls k \<le> Mns l \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
954 |
"Mns k \<le> 0 \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
955 |
"Mns k \<le> Pls l \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
956 |
"Mns k \<le> Mns l \<longleftrightarrow> l \<le> k" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
957 |
by simp_all |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
958 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
959 |
lemma less_int_code [code]: |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
960 |
"0 < (0::int) \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
961 |
"0 < Pls l \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
962 |
"0 < Mns l \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
963 |
"Pls k < 0 \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
964 |
"Pls k < Pls l \<longleftrightarrow> k < l" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
965 |
"Pls k < Mns l \<longleftrightarrow> False" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
966 |
"Mns k < 0 \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
967 |
"Mns k < Pls l \<longleftrightarrow> True" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
968 |
"Mns k < Mns l \<longleftrightarrow> l < k" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
969 |
by simp_all |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
970 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
971 |
hide_const (open) sub dup |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
972 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
973 |
text {* Pretty literals *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
974 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
975 |
ML {* |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
976 |
local open Code_Thingol in |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
977 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
978 |
fun add_code print target = |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
979 |
let |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
980 |
fun dest_num one' dig0' dig1' thm = |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
981 |
let |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
982 |
fun dest_dig (IConst (c, _)) = if c = dig0' then 0 |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
983 |
else if c = dig1' then 1 |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
984 |
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal dig" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
985 |
| dest_dig _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal digit"; |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
986 |
fun dest_num (IConst (c, _)) = if c = one' then 1 |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
987 |
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
988 |
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_dig t1 |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
989 |
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
990 |
in dest_num end; |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
991 |
fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] = |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
992 |
(Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t |
38923 | 993 |
fun add_syntax (c, sgn) = Code_Target.add_const_syntax target c |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
994 |
(SOME (Code_Printer.complex_const_syntax |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
995 |
(1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}], |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
996 |
pretty sgn)))); |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
997 |
in |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
998 |
add_syntax (@{const_name Pls}, I) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
999 |
#> add_syntax (@{const_name Mns}, (fn k => ~ k)) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1000 |
end; |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1001 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1002 |
end |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1003 |
*} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1004 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1005 |
hide_const (open) One Dig0 Dig1 |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1006 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1007 |
|
31025 | 1008 |
subsection {* Toy examples *} |
28021 | 1009 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1010 |
definition "foo \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat)" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1011 |
definition "bar \<longleftrightarrow> #4 * #2 + #7 \<ge> (#8 :: int) - #3" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1012 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1013 |
code_thms foo bar |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1014 |
export_code foo bar checking SML OCaml? Haskell? Scala? |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1015 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1016 |
text {* This is an ad-hoc @{text Code_Integer} setup. *} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1017 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1018 |
setup {* |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1019 |
fold (add_code Code_Printer.literal_numeral) |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1020 |
[Code_ML.target_SML, Code_ML.target_OCaml, Code_Haskell.target, Code_Scala.target] |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1021 |
*} |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1022 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1023 |
code_type int |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1024 |
(SML "IntInf.int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1025 |
(OCaml "Big'_int.big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1026 |
(Haskell "Integer") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1027 |
(Scala "BigInt") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1028 |
(Eval "int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1029 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1030 |
code_const "0::int" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1031 |
(SML "0/ :/ IntInf.int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1032 |
(OCaml "Big'_int.zero") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1033 |
(Haskell "0") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1034 |
(Scala "BigInt(0)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1035 |
(Eval "0/ :/ int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1036 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1037 |
code_const Int.pred |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1038 |
(SML "IntInf.- ((_), 1)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1039 |
(OCaml "Big'_int.pred'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1040 |
(Haskell "!(_/ -/ 1)") |
38773
f9837065b5e8
prevent line breaks after Scala symbolic operators
haftmann
parents:
38054
diff
changeset
|
1041 |
(Scala "!(_ -/ 1)") |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1042 |
(Eval "!(_/ -/ 1)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1043 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1044 |
code_const Int.succ |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1045 |
(SML "IntInf.+ ((_), 1)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1046 |
(OCaml "Big'_int.succ'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1047 |
(Haskell "!(_/ +/ 1)") |
38773
f9837065b5e8
prevent line breaks after Scala symbolic operators
haftmann
parents:
38054
diff
changeset
|
1048 |
(Scala "!(_ +/ 1)") |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1049 |
(Eval "!(_/ +/ 1)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1050 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1051 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1052 |
(SML "IntInf.+ ((_), (_))") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1053 |
(OCaml "Big'_int.add'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1054 |
(Haskell infixl 6 "+") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1055 |
(Scala infixl 7 "+") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1056 |
(Eval infixl 8 "+") |
37826 | 1057 |
|
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1058 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1059 |
(SML "IntInf.~") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1060 |
(OCaml "Big'_int.minus'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1061 |
(Haskell "negate") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1062 |
(Scala "!(- _)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1063 |
(Eval "~/ _") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1064 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1065 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1066 |
(SML "IntInf.- ((_), (_))") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1067 |
(OCaml "Big'_int.sub'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1068 |
(Haskell infixl 6 "-") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1069 |
(Scala infixl 7 "-") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1070 |
(Eval infixl 8 "-") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1071 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1072 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1073 |
(SML "IntInf.* ((_), (_))") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1074 |
(OCaml "Big'_int.mult'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1075 |
(Haskell infixl 7 "*") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1076 |
(Scala infixl 8 "*") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1077 |
(Eval infixl 9 "*") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1078 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1079 |
code_const pdivmod |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1080 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1081 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1082 |
(Haskell "divMod/ (abs _)/ (abs _)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1083 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1084 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
37826 | 1085 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38797
diff
changeset
|
1086 |
code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1087 |
(SML "!((_ : IntInf.int) = _)") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1088 |
(OCaml "Big'_int.eq'_big'_int") |
39272 | 1089 |
(Haskell infix 4 "==") |
38054
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1090 |
(Scala infixl 5 "==") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1091 |
(Eval infixl 6 "=") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1092 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1093 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1094 |
(SML "IntInf.<= ((_), (_))") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1095 |
(OCaml "Big'_int.le'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1096 |
(Haskell infix 4 "<=") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1097 |
(Scala infixl 4 "<=") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1098 |
(Eval infixl 6 "<=") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1099 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1100 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1101 |
(SML "IntInf.< ((_), (_))") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1102 |
(OCaml "Big'_int.lt'_big'_int") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1103 |
(Haskell infix 4 "<") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1104 |
(Scala infixl 4 "<") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1105 |
(Eval infixl 6 "<") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1106 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1107 |
code_const Code_Numeral.int_of |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1108 |
(SML "IntInf.fromInt") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1109 |
(OCaml "_") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1110 |
(Haskell "toInteger") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1111 |
(Scala "!_.as'_BigInt") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1112 |
(Eval "_") |
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1113 |
|
acd48ef85bfc
tuned; added pretty numerals for code generation
haftmann
parents:
37826
diff
changeset
|
1114 |
export_code foo bar checking SML OCaml? Haskell? Scala? |
28021 | 1115 |
|
1116 |
end |