1.1 --- a/src/HOL/Library/Code_Integer.thy Wed Jul 28 14:09:56 2010 +0200
1.2 +++ b/src/HOL/Library/Code_Integer.thy Wed Jul 28 14:11:48 2010 +0200
1.3 @@ -19,6 +19,7 @@
1.4 (OCaml "Big'_int.big'_int")
1.5 (Haskell "Integer")
1.6 (Scala "BigInt")
1.7 + (Eval "int")
1.8
1.9 code_instance int :: eq
1.10 (Haskell -)
2.1 --- a/src/HOL/ex/Numeral.thy Wed Jul 28 14:09:56 2010 +0200
2.2 +++ b/src/HOL/ex/Numeral.thy Wed Jul 28 14:11:48 2010 +0200
2.3 @@ -55,10 +55,11 @@
2.4 by (induct n) (simp_all add: nat_of_num_inc)
2.5
2.6 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
2.7 - apply safe
2.8 - apply (drule arg_cong [where f=num_of_nat])
2.9 - apply (simp add: nat_of_num_inverse)
2.10 - done
2.11 +proof
2.12 + assume "nat_of_num x = nat_of_num y"
2.13 + then have "num_of_nat (nat_of_num x) = num_of_nat (nat_of_num y)" by simp
2.14 + then show "x = y" by (simp add: nat_of_num_inverse)
2.15 +qed simp
2.16
2.17 lemma num_induct [case_names One inc]:
2.18 fixes P :: "num \<Rightarrow> bool"
2.19 @@ -81,12 +82,12 @@
2.20 qed
2.21
2.22 text {*
2.23 - From now on, there are two possible models for @{typ num}:
2.24 - as positive naturals (rule @{text "num_induct"})
2.25 - and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
2.26 + From now on, there are two possible models for @{typ num}: as
2.27 + positive naturals (rule @{text "num_induct"}) and as digit
2.28 + representation (rules @{text "num.induct"}, @{text "num.cases"}).
2.29
2.30 - It is not entirely clear in which context it is better to use
2.31 - the one or the other, or whether the construction should be reversed.
2.32 + It is not entirely clear in which context it is better to use the
2.33 + one or the other, or whether the construction should be reversed.
2.34 *}
2.35
2.36
2.37 @@ -154,18 +155,6 @@
2.38 by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
2.39 left_distrib right_distrib)
2.40
2.41 -lemma Dig_eq:
2.42 - "One = One \<longleftrightarrow> True"
2.43 - "One = Dig0 n \<longleftrightarrow> False"
2.44 - "One = Dig1 n \<longleftrightarrow> False"
2.45 - "Dig0 m = One \<longleftrightarrow> False"
2.46 - "Dig1 m = One \<longleftrightarrow> False"
2.47 - "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
2.48 - "Dig0 m = Dig1 n \<longleftrightarrow> False"
2.49 - "Dig1 m = Dig0 n \<longleftrightarrow> False"
2.50 - "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
2.51 - by simp_all
2.52 -
2.53 lemma less_eq_num_code [numeral, simp, code]:
2.54 "One \<le> n \<longleftrightarrow> True"
2.55 "Dig0 m \<le> One \<longleftrightarrow> False"
2.56 @@ -207,8 +196,8 @@
2.57
2.58 primrec DigM :: "num \<Rightarrow> num" where
2.59 "DigM One = One"
2.60 - | "DigM (Dig0 n) = Dig1 (DigM n)"
2.61 - | "DigM (Dig1 n) = Dig1 (Dig0 n)"
2.62 +| "DigM (Dig0 n) = Dig1 (DigM n)"
2.63 +| "DigM (Dig1 n) = Dig1 (Dig0 n)"
2.64
2.65 lemma DigM_plus_one: "DigM n + One = Dig0 n"
2.66 by (induct n) simp_all
2.67 @@ -217,7 +206,7 @@
2.68 by (induct n) simp_all
2.69
2.70 lemma one_plus_DigM: "One + DigM n = Dig0 n"
2.71 - unfolding add_One_commute DigM_plus_one ..
2.72 + by (simp add: add_One_commute DigM_plus_one)
2.73
2.74 text {* Squaring and exponentiation *}
2.75
2.76 @@ -226,8 +215,7 @@
2.77 | "square (Dig0 n) = Dig0 (Dig0 (square n))"
2.78 | "square (Dig1 n) = Dig1 (Dig0 (square n + n))"
2.79
2.80 -primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
2.81 -where
2.82 +primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where
2.83 "pow x One = x"
2.84 | "pow x (Dig0 y) = square (pow x y)"
2.85 | "pow x (Dig1 y) = x * square (pow x y)"
2.86 @@ -245,31 +233,22 @@
2.87
2.88 primrec of_num :: "num \<Rightarrow> 'a" where
2.89 of_num_One [numeral]: "of_num One = 1"
2.90 - | "of_num (Dig0 n) = of_num n + of_num n"
2.91 - | "of_num (Dig1 n) = of_num n + of_num n + 1"
2.92 +| "of_num (Dig0 n) = of_num n + of_num n"
2.93 +| "of_num (Dig1 n) = of_num n + of_num n + 1"
2.94
2.95 -lemma of_num_inc: "of_num (inc x) = of_num x + 1"
2.96 - by (induct x) (simp_all add: add_ac)
2.97 +lemma of_num_inc: "of_num (inc n) = of_num n + 1"
2.98 + by (induct n) (simp_all add: add_ac)
2.99
2.100 lemma of_num_add: "of_num (m + n) = of_num m + of_num n"
2.101 - apply (induct n rule: num_induct)
2.102 - apply (simp_all add: add_One add_inc of_num_inc add_ac)
2.103 - done
2.104 + by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac)
2.105
2.106 lemma of_num_mult: "of_num (m * n) = of_num m * of_num n"
2.107 - apply (induct n rule: num_induct)
2.108 - apply (simp add: mult_One)
2.109 - apply (simp add: mult_inc of_num_add of_num_inc right_distrib)
2.110 - done
2.111 + by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib)
2.112
2.113 declare of_num.simps [simp del]
2.114
2.115 end
2.116
2.117 -text {*
2.118 - ML stuff and syntax.
2.119 -*}
2.120 -
2.121 ML {*
2.122 fun mk_num k =
2.123 if k > 1 then
2.124 @@ -285,13 +264,13 @@
2.125 | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1
2.126 | dest_num t = raise TERM ("dest_num", [t]);
2.127
2.128 -(*FIXME these have to gain proper context via morphisms phi*)
2.129 -
2.130 -fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T)
2.131 +fun mk_numeral phi T k = Morphism.term phi (Const (@{const_name of_num}, @{typ num} --> T))
2.132 $ mk_num k
2.133
2.134 -fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) =
2.135 - (T, dest_num t)
2.136 +fun dest_numeral phi (u $ t) =
2.137 + if Term.aconv_untyped (u, Morphism.term phi (Const (@{const_name of_num}, dummyT)))
2.138 + then (range_type (fastype_of u), dest_num t)
2.139 + else raise TERM ("dest_numeral", [u, t]);
2.140 *}
2.141
2.142 syntax
2.143 @@ -335,12 +314,9 @@
2.144 in [(@{const_syntax of_num}, num_tr')] end
2.145 *}
2.146
2.147 +
2.148 subsection {* Class-specific numeral rules *}
2.149
2.150 -text {*
2.151 - @{const of_num} is a morphism.
2.152 -*}
2.153 -
2.154 subsubsection {* Class @{text semiring_numeral} *}
2.155
2.156 context semiring_numeral
2.157 @@ -349,11 +325,10 @@
2.158 abbreviation "Num1 \<equiv> of_num One"
2.159
2.160 text {*
2.161 - Alas, there is still the duplication of @{term 1},
2.162 - thought the duplicated @{term 0} has disappeared.
2.163 - We could get rid of it by replacing the constructor
2.164 - @{term 1} in @{typ num} by two constructors
2.165 - @{text two} and @{text three}, resulting in a further
2.166 + Alas, there is still the duplication of @{term 1}, although the
2.167 + duplicated @{term 0} has disappeared. We could get rid of it by
2.168 + replacing the constructor @{term 1} in @{typ num} by two
2.169 + constructors @{text two} and @{text three}, resulting in a further
2.170 blow-up. But it could be worth the effort.
2.171 *}
2.172
2.173 @@ -367,7 +342,7 @@
2.174
2.175 lemma of_num_plus [numeral]:
2.176 "of_num m + of_num n = of_num (m + n)"
2.177 - unfolding of_num_add ..
2.178 + by (simp only: of_num_add)
2.179
2.180 lemma of_num_times_one [numeral]:
2.181 "of_num n * 1 = of_num n"
2.182 @@ -383,9 +358,8 @@
2.183
2.184 end
2.185
2.186 -subsubsection {*
2.187 - Structures with a zero: class @{text semiring_1}
2.188 -*}
2.189 +
2.190 +subsubsection {* Structures with a zero: class @{text semiring_1} *}
2.191
2.192 context semiring_1
2.193 begin
2.194 @@ -422,9 +396,8 @@
2.195 then show "nat_of_num n = of_num n" by simp
2.196 qed
2.197
2.198 -subsubsection {*
2.199 - Equality: class @{text semiring_char_0}
2.200 -*}
2.201 +
2.202 +subsubsection {* Equality: class @{text semiring_char_0} *}
2.203
2.204 context semiring_char_0
2.205 begin
2.206 @@ -441,18 +414,23 @@
2.207
2.208 end
2.209
2.210 -subsubsection {*
2.211 - Comparisons: class @{text linordered_semidom}
2.212 +
2.213 +subsubsection {* Comparisons: class @{text linordered_semidom} *}
2.214 +
2.215 +text {*
2.216 + Perhaps the underlying structure could even
2.217 + be more general than @{text linordered_semidom}.
2.218 *}
2.219
2.220 -text {* Could be perhaps more general than here. *}
2.221 -
2.222 context linordered_semidom
2.223 begin
2.224
2.225 lemma of_num_pos [numeral]: "0 < of_num n"
2.226 by (induct n) (simp_all add: of_num.simps add_pos_pos)
2.227
2.228 +lemma of_num_not_zero [numeral]: "of_num n \<noteq> 0"
2.229 + using of_num_pos [of n] by simp
2.230 +
2.231 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"
2.232 proof -
2.233 have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n"
2.234 @@ -500,6 +478,9 @@
2.235 finally show ?thesis .
2.236 qed
2.237
2.238 +lemma minus_of_num_not_equal_of_num: "- of_num m \<noteq> of_num n"
2.239 + using minus_of_num_less_of_num_iff [of m n] by simp
2.240 +
2.241 lemma minus_of_num_less_one_iff: "- of_num n < 1"
2.242 using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One)
2.243
2.244 @@ -557,6 +538,7 @@
2.245
2.246 lemmas less_signed_numeral_special [numeral] =
2.247 minus_of_num_less_of_num_iff
2.248 + minus_of_num_not_equal_of_num
2.249 minus_of_num_less_one_iff
2.250 minus_one_less_of_num_iff
2.251 minus_one_less_one_iff
2.252 @@ -567,9 +549,7 @@
2.253
2.254 end
2.255
2.256 -subsubsection {*
2.257 - Structures with subtraction: class @{text semiring_1_minus}
2.258 -*}
2.259 +subsubsection {* Structures with subtraction: class @{text semiring_1_minus} *}
2.260
2.261 class semiring_minus = semiring + minus + zero +
2.262 assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
2.263 @@ -612,8 +592,9 @@
2.264 fun attach_num ct = (dest_num (Thm.term_of ct), ct);
2.265 fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;
2.266 val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
2.267 - fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
2.268 - [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
2.269 + fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq}
2.270 + OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
2.271 + [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
2.272 in fn phi => fn _ => fn ct => case try cdifference ct
2.273 of NONE => (NONE)
2.274 | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0
2.275 @@ -651,15 +632,14 @@
2.276
2.277 end
2.278
2.279 -subsubsection {*
2.280 - Structures with negation: class @{text ring_1}
2.281 -*}
2.282 +
2.283 +subsubsection {* Structures with negation: class @{text ring_1} *}
2.284
2.285 context ring_1
2.286 begin
2.287
2.288 -subclass semiring_1_minus
2.289 - proof qed (simp_all add: algebra_simps)
2.290 +subclass semiring_1_minus proof
2.291 +qed (simp_all add: algebra_simps)
2.292
2.293 lemma Dig_zero_minus_of_num [numeral]:
2.294 "0 - of_num n = - of_num n"
2.295 @@ -696,9 +676,8 @@
2.296
2.297 end
2.298
2.299 -subsubsection {*
2.300 - Structures with exponentiation
2.301 -*}
2.302 +
2.303 +subsubsection {* Structures with exponentiation *}
2.304
2.305 lemma of_num_square: "of_num (square x) = of_num x * of_num x"
2.306 by (induct x)
2.307 @@ -729,11 +708,10 @@
2.308 declare power_one [numeral]
2.309
2.310
2.311 -subsubsection {*
2.312 - Greetings to @{typ nat}.
2.313 -*}
2.314 +subsubsection {* Greetings to @{typ nat}. *}
2.315
2.316 -instance nat :: semiring_1_minus proof qed simp_all
2.317 +instance nat :: semiring_1_minus proof
2.318 +qed simp_all
2.319
2.320 lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)"
2.321 unfolding of_num_plus_one [symmetric] by simp
2.322 @@ -748,141 +726,9 @@
2.323 declare diff_0_eq_0 [numeral]
2.324
2.325
2.326 -subsection {* Code generator setup for @{typ int} *}
2.327 +subsection {* Proof tools setup *}
2.328
2.329 -definition Pls :: "num \<Rightarrow> int" where
2.330 - [simp, code_post]: "Pls n = of_num n"
2.331 -
2.332 -definition Mns :: "num \<Rightarrow> int" where
2.333 - [simp, code_post]: "Mns n = - of_num n"
2.334 -
2.335 -code_datatype "0::int" Pls Mns
2.336 -
2.337 -lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
2.338 -
2.339 -definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
2.340 - [simp]: "sub m n = (of_num m - of_num n)"
2.341 -
2.342 -definition dup :: "int \<Rightarrow> int" where
2.343 - "dup k = 2 * k"
2.344 -
2.345 -lemma Dig_sub [code]:
2.346 - "sub One One = 0"
2.347 - "sub (Dig0 m) One = of_num (DigM m)"
2.348 - "sub (Dig1 m) One = of_num (Dig0 m)"
2.349 - "sub One (Dig0 n) = - of_num (DigM n)"
2.350 - "sub One (Dig1 n) = - of_num (Dig0 n)"
2.351 - "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
2.352 - "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
2.353 - "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
2.354 - "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
2.355 - apply (simp_all add: dup_def algebra_simps)
2.356 - apply (simp_all add: of_num_plus one_plus_DigM)[4]
2.357 - apply (simp_all add: of_num.simps)
2.358 - done
2.359 -
2.360 -lemma dup_code [code]:
2.361 - "dup 0 = 0"
2.362 - "dup (Pls n) = Pls (Dig0 n)"
2.363 - "dup (Mns n) = Mns (Dig0 n)"
2.364 - by (simp_all add: dup_def of_num.simps)
2.365 -
2.366 -lemma [code, code del]:
2.367 - "(1 :: int) = 1"
2.368 - "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
2.369 - "(uminus :: int \<Rightarrow> int) = uminus"
2.370 - "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
2.371 - "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
2.372 - "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
2.373 - "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
2.374 - "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
2.375 - by rule+
2.376 -
2.377 -lemma one_int_code [code]:
2.378 - "1 = Pls One"
2.379 - by (simp add: of_num_One)
2.380 -
2.381 -lemma plus_int_code [code]:
2.382 - "k + 0 = (k::int)"
2.383 - "0 + l = (l::int)"
2.384 - "Pls m + Pls n = Pls (m + n)"
2.385 - "Pls m - Pls n = sub m n"
2.386 - "Mns m + Mns n = Mns (m + n)"
2.387 - "Mns m - Mns n = sub n m"
2.388 - by (simp_all add: of_num_add)
2.389 -
2.390 -lemma uminus_int_code [code]:
2.391 - "uminus 0 = (0::int)"
2.392 - "uminus (Pls m) = Mns m"
2.393 - "uminus (Mns m) = Pls m"
2.394 - by simp_all
2.395 -
2.396 -lemma minus_int_code [code]:
2.397 - "k - 0 = (k::int)"
2.398 - "0 - l = uminus (l::int)"
2.399 - "Pls m - Pls n = sub m n"
2.400 - "Pls m - Mns n = Pls (m + n)"
2.401 - "Mns m - Pls n = Mns (m + n)"
2.402 - "Mns m - Mns n = sub n m"
2.403 - by (simp_all add: of_num_add)
2.404 -
2.405 -lemma times_int_code [code]:
2.406 - "k * 0 = (0::int)"
2.407 - "0 * l = (0::int)"
2.408 - "Pls m * Pls n = Pls (m * n)"
2.409 - "Pls m * Mns n = Mns (m * n)"
2.410 - "Mns m * Pls n = Mns (m * n)"
2.411 - "Mns m * Mns n = Pls (m * n)"
2.412 - by (simp_all add: of_num_mult)
2.413 -
2.414 -lemma eq_int_code [code]:
2.415 - "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
2.416 - "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
2.417 - "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
2.418 - "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
2.419 - "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
2.420 - "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
2.421 - "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
2.422 - "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
2.423 - "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
2.424 - using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
2.425 - by (simp_all add: of_num_eq_iff eq)
2.426 -
2.427 -lemma less_eq_int_code [code]:
2.428 - "0 \<le> (0::int) \<longleftrightarrow> True"
2.429 - "0 \<le> Pls l \<longleftrightarrow> True"
2.430 - "0 \<le> Mns l \<longleftrightarrow> False"
2.431 - "Pls k \<le> 0 \<longleftrightarrow> False"
2.432 - "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"
2.433 - "Pls k \<le> Mns l \<longleftrightarrow> False"
2.434 - "Mns k \<le> 0 \<longleftrightarrow> True"
2.435 - "Mns k \<le> Pls l \<longleftrightarrow> True"
2.436 - "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"
2.437 - using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
2.438 - by (simp_all add: of_num_less_eq_iff)
2.439 -
2.440 -lemma less_int_code [code]:
2.441 - "0 < (0::int) \<longleftrightarrow> False"
2.442 - "0 < Pls l \<longleftrightarrow> True"
2.443 - "0 < Mns l \<longleftrightarrow> False"
2.444 - "Pls k < 0 \<longleftrightarrow> False"
2.445 - "Pls k < Pls l \<longleftrightarrow> k < l"
2.446 - "Pls k < Mns l \<longleftrightarrow> False"
2.447 - "Mns k < 0 \<longleftrightarrow> True"
2.448 - "Mns k < Pls l \<longleftrightarrow> True"
2.449 - "Mns k < Mns l \<longleftrightarrow> l < k"
2.450 - using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
2.451 - by (simp_all add: of_num_less_iff)
2.452 -
2.453 -lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
2.454 -lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
2.455 -declare zero_is_num_zero [code_unfold del]
2.456 -declare one_is_num_one [code_unfold del]
2.457 -
2.458 -hide_const (open) sub dup
2.459 -
2.460 -
2.461 -subsection {* Numeral equations as default simplification rules *}
2.462 +subsubsection {* Numeral equations as default simplification rules *}
2.463
2.464 declare (in semiring_numeral) of_num_One [simp]
2.465 declare (in semiring_numeral) of_num_plus_one [simp]
2.466 @@ -897,6 +743,7 @@
2.467 declare (in semiring_char_0) one_eq_of_num_iff [simp]
2.468
2.469 declare (in linordered_semidom) of_num_pos [simp]
2.470 +declare (in linordered_semidom) of_num_not_zero [simp]
2.471 declare (in linordered_semidom) of_num_less_eq_iff [simp]
2.472 declare (in linordered_semidom) of_num_less_eq_one_iff [simp]
2.473 declare (in linordered_semidom) one_less_eq_of_num_iff [simp]
2.474 @@ -924,8 +771,6 @@
2.475 declare Suc_of_num [simp]
2.476
2.477
2.478 -subsection {* Simplification Procedures *}
2.479 -
2.480 subsubsection {* Reorientation of equalities *}
2.481
2.482 setup {*
2.483 @@ -985,12 +830,282 @@
2.484 Semiring_Times_Assoc.proc ss (Thm.term_of ct) *}
2.485
2.486
2.487 +subsection {* Code generator setup for @{typ int} *}
2.488 +
2.489 +text {* Reversing standard setup *}
2.490 +
2.491 +lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
2.492 +lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
2.493 +declare zero_is_num_zero [code_unfold del]
2.494 +declare one_is_num_one [code_unfold del]
2.495 +
2.496 +lemma [code, code del]:
2.497 + "(1 :: int) = 1"
2.498 + "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
2.499 + "(uminus :: int \<Rightarrow> int) = uminus"
2.500 + "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
2.501 + "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
2.502 + "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
2.503 + "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
2.504 + "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
2.505 + by rule+
2.506 +
2.507 +text {* Constructors *}
2.508 +
2.509 +definition Pls :: "num \<Rightarrow> int" where
2.510 + [simp, code_post]: "Pls n = of_num n"
2.511 +
2.512 +definition Mns :: "num \<Rightarrow> int" where
2.513 + [simp, code_post]: "Mns n = - of_num n"
2.514 +
2.515 +code_datatype "0::int" Pls Mns
2.516 +
2.517 +lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
2.518 +
2.519 +text {* Auxiliary operations *}
2.520 +
2.521 +definition dup :: "int \<Rightarrow> int" where
2.522 + [simp]: "dup k = k + k"
2.523 +
2.524 +lemma Dig_dup [code]:
2.525 + "dup 0 = 0"
2.526 + "dup (Pls n) = Pls (Dig0 n)"
2.527 + "dup (Mns n) = Mns (Dig0 n)"
2.528 + by (simp_all add: of_num.simps)
2.529 +
2.530 +definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
2.531 + [simp]: "sub m n = (of_num m - of_num n)"
2.532 +
2.533 +lemma Dig_sub [code]:
2.534 + "sub One One = 0"
2.535 + "sub (Dig0 m) One = of_num (DigM m)"
2.536 + "sub (Dig1 m) One = of_num (Dig0 m)"
2.537 + "sub One (Dig0 n) = - of_num (DigM n)"
2.538 + "sub One (Dig1 n) = - of_num (Dig0 n)"
2.539 + "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
2.540 + "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
2.541 + "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
2.542 + "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
2.543 + by (simp_all add: algebra_simps num_eq_iff nat_of_num_add)
2.544 +
2.545 +text {* Implementations *}
2.546 +
2.547 +lemma one_int_code [code]:
2.548 + "1 = Pls One"
2.549 + by (simp add: of_num_One)
2.550 +
2.551 +lemma plus_int_code [code]:
2.552 + "k + 0 = (k::int)"
2.553 + "0 + l = (l::int)"
2.554 + "Pls m + Pls n = Pls (m + n)"
2.555 + "Pls m + Mns n = sub m n"
2.556 + "Mns m + Pls n = sub n m"
2.557 + "Mns m + Mns n = Mns (m + n)"
2.558 + by simp_all
2.559 +
2.560 +lemma uminus_int_code [code]:
2.561 + "uminus 0 = (0::int)"
2.562 + "uminus (Pls m) = Mns m"
2.563 + "uminus (Mns m) = Pls m"
2.564 + by simp_all
2.565 +
2.566 +lemma minus_int_code [code]:
2.567 + "k - 0 = (k::int)"
2.568 + "0 - l = uminus (l::int)"
2.569 + "Pls m - Pls n = sub m n"
2.570 + "Pls m - Mns n = Pls (m + n)"
2.571 + "Mns m - Pls n = Mns (m + n)"
2.572 + "Mns m - Mns n = sub n m"
2.573 + by simp_all
2.574 +
2.575 +lemma times_int_code [code]:
2.576 + "k * 0 = (0::int)"
2.577 + "0 * l = (0::int)"
2.578 + "Pls m * Pls n = Pls (m * n)"
2.579 + "Pls m * Mns n = Mns (m * n)"
2.580 + "Mns m * Pls n = Mns (m * n)"
2.581 + "Mns m * Mns n = Pls (m * n)"
2.582 + by simp_all
2.583 +
2.584 +lemma eq_int_code [code]:
2.585 + "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
2.586 + "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
2.587 + "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
2.588 + "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
2.589 + "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
2.590 + "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
2.591 + "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
2.592 + "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
2.593 + "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
2.594 + by (auto simp add: eq dest: sym)
2.595 +
2.596 +lemma less_eq_int_code [code]:
2.597 + "0 \<le> (0::int) \<longleftrightarrow> True"
2.598 + "0 \<le> Pls l \<longleftrightarrow> True"
2.599 + "0 \<le> Mns l \<longleftrightarrow> False"
2.600 + "Pls k \<le> 0 \<longleftrightarrow> False"
2.601 + "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"
2.602 + "Pls k \<le> Mns l \<longleftrightarrow> False"
2.603 + "Mns k \<le> 0 \<longleftrightarrow> True"
2.604 + "Mns k \<le> Pls l \<longleftrightarrow> True"
2.605 + "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"
2.606 + by simp_all
2.607 +
2.608 +lemma less_int_code [code]:
2.609 + "0 < (0::int) \<longleftrightarrow> False"
2.610 + "0 < Pls l \<longleftrightarrow> True"
2.611 + "0 < Mns l \<longleftrightarrow> False"
2.612 + "Pls k < 0 \<longleftrightarrow> False"
2.613 + "Pls k < Pls l \<longleftrightarrow> k < l"
2.614 + "Pls k < Mns l \<longleftrightarrow> False"
2.615 + "Mns k < 0 \<longleftrightarrow> True"
2.616 + "Mns k < Pls l \<longleftrightarrow> True"
2.617 + "Mns k < Mns l \<longleftrightarrow> l < k"
2.618 + by simp_all
2.619 +
2.620 +hide_const (open) sub dup
2.621 +
2.622 +text {* Pretty literals *}
2.623 +
2.624 +ML {*
2.625 +local open Code_Thingol in
2.626 +
2.627 +fun add_code print target =
2.628 + let
2.629 + fun dest_num one' dig0' dig1' thm =
2.630 + let
2.631 + fun dest_dig (IConst (c, _)) = if c = dig0' then 0
2.632 + else if c = dig1' then 1
2.633 + else Code_Printer.eqn_error thm "Illegal numeral expression: illegal dig"
2.634 + | dest_dig _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal digit";
2.635 + fun dest_num (IConst (c, _)) = if c = one' then 1
2.636 + else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
2.637 + | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_dig t1
2.638 + | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
2.639 + in dest_num end;
2.640 + fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] =
2.641 + (Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t
2.642 + fun add_syntax (c, sgn) = Code_Target.add_syntax_const target c
2.643 + (SOME (Code_Printer.complex_const_syntax
2.644 + (1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}],
2.645 + pretty sgn))));
2.646 + in
2.647 + add_syntax (@{const_name Pls}, I)
2.648 + #> add_syntax (@{const_name Mns}, (fn k => ~ k))
2.649 + end;
2.650 +
2.651 +end
2.652 +*}
2.653 +
2.654 +hide_const (open) One Dig0 Dig1
2.655 +
2.656 +
2.657 subsection {* Toy examples *}
2.658
2.659 -definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
2.660 +definition "foo \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat)"
2.661 +definition "bar \<longleftrightarrow> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
2.662
2.663 -code_thms bar
2.664 +code_thms foo bar
2.665 +export_code foo bar checking SML OCaml? Haskell? Scala?
2.666
2.667 -export_code bar checking SML OCaml? Haskell?
2.668 +text {* This is an ad-hoc @{text Code_Integer} setup. *}
2.669 +
2.670 +setup {*
2.671 + fold (add_code Code_Printer.literal_numeral)
2.672 + [Code_ML.target_SML, Code_ML.target_OCaml, Code_Haskell.target, Code_Scala.target]
2.673 +*}
2.674 +
2.675 +code_type int
2.676 + (SML "IntInf.int")
2.677 + (OCaml "Big'_int.big'_int")
2.678 + (Haskell "Integer")
2.679 + (Scala "BigInt")
2.680 + (Eval "int")
2.681 +
2.682 +code_const "0::int"
2.683 + (SML "0/ :/ IntInf.int")
2.684 + (OCaml "Big'_int.zero")
2.685 + (Haskell "0")
2.686 + (Scala "BigInt(0)")
2.687 + (Eval "0/ :/ int")
2.688 +
2.689 +code_const Int.pred
2.690 + (SML "IntInf.- ((_), 1)")
2.691 + (OCaml "Big'_int.pred'_big'_int")
2.692 + (Haskell "!(_/ -/ 1)")
2.693 + (Scala "!(_/ -/ 1)")
2.694 + (Eval "!(_/ -/ 1)")
2.695 +
2.696 +code_const Int.succ
2.697 + (SML "IntInf.+ ((_), 1)")
2.698 + (OCaml "Big'_int.succ'_big'_int")
2.699 + (Haskell "!(_/ +/ 1)")
2.700 + (Scala "!(_/ +/ 1)")
2.701 + (Eval "!(_/ +/ 1)")
2.702 +
2.703 +code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
2.704 + (SML "IntInf.+ ((_), (_))")
2.705 + (OCaml "Big'_int.add'_big'_int")
2.706 + (Haskell infixl 6 "+")
2.707 + (Scala infixl 7 "+")
2.708 + (Eval infixl 8 "+")
2.709 +
2.710 +code_const "uminus \<Colon> int \<Rightarrow> int"
2.711 + (SML "IntInf.~")
2.712 + (OCaml "Big'_int.minus'_big'_int")
2.713 + (Haskell "negate")
2.714 + (Scala "!(- _)")
2.715 + (Eval "~/ _")
2.716 +
2.717 +code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
2.718 + (SML "IntInf.- ((_), (_))")
2.719 + (OCaml "Big'_int.sub'_big'_int")
2.720 + (Haskell infixl 6 "-")
2.721 + (Scala infixl 7 "-")
2.722 + (Eval infixl 8 "-")
2.723 +
2.724 +code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
2.725 + (SML "IntInf.* ((_), (_))")
2.726 + (OCaml "Big'_int.mult'_big'_int")
2.727 + (Haskell infixl 7 "*")
2.728 + (Scala infixl 8 "*")
2.729 + (Eval infixl 9 "*")
2.730 +
2.731 +code_const pdivmod
2.732 + (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
2.733 + (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
2.734 + (Haskell "divMod/ (abs _)/ (abs _)")
2.735 + (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
2.736 + (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
2.737 +
2.738 +code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.739 + (SML "!((_ : IntInf.int) = _)")
2.740 + (OCaml "Big'_int.eq'_big'_int")
2.741 + (Haskell infixl 4 "==")
2.742 + (Scala infixl 5 "==")
2.743 + (Eval infixl 6 "=")
2.744 +
2.745 +code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.746 + (SML "IntInf.<= ((_), (_))")
2.747 + (OCaml "Big'_int.le'_big'_int")
2.748 + (Haskell infix 4 "<=")
2.749 + (Scala infixl 4 "<=")
2.750 + (Eval infixl 6 "<=")
2.751 +
2.752 +code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.753 + (SML "IntInf.< ((_), (_))")
2.754 + (OCaml "Big'_int.lt'_big'_int")
2.755 + (Haskell infix 4 "<")
2.756 + (Scala infixl 4 "<")
2.757 + (Eval infixl 6 "<")
2.758 +
2.759 +code_const Code_Numeral.int_of
2.760 + (SML "IntInf.fromInt")
2.761 + (OCaml "_")
2.762 + (Haskell "toInteger")
2.763 + (Scala "!_.as'_BigInt")
2.764 + (Eval "_")
2.765 +
2.766 +export_code foo bar checking SML OCaml? Haskell? Scala?
2.767
2.768 end