1.1 --- a/src/HOL/ex/Numeral.thy Wed Jul 28 12:12:29 2010 +0200
1.2 +++ b/src/HOL/ex/Numeral.thy Wed Jul 28 12:12:32 2010 +0200
1.3 @@ -55,10 +55,11 @@
1.4 by (induct n) (simp_all add: nat_of_num_inc)
1.5
1.6 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
1.7 - apply safe
1.8 - apply (drule arg_cong [where f=num_of_nat])
1.9 - apply (simp add: nat_of_num_inverse)
1.10 - done
1.11 +proof
1.12 + assume "nat_of_num x = nat_of_num y"
1.13 + then have "num_of_nat (nat_of_num x) = num_of_nat (nat_of_num y)" by simp
1.14 + then show "x = y" by (simp add: nat_of_num_inverse)
1.15 +qed simp
1.16
1.17 lemma num_induct [case_names One inc]:
1.18 fixes P :: "num \<Rightarrow> bool"
1.19 @@ -81,12 +82,12 @@
1.20 qed
1.21
1.22 text {*
1.23 - From now on, there are two possible models for @{typ num}:
1.24 - as positive naturals (rule @{text "num_induct"})
1.25 - and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
1.26 + From now on, there are two possible models for @{typ num}: as
1.27 + positive naturals (rule @{text "num_induct"}) and as digit
1.28 + representation (rules @{text "num.induct"}, @{text "num.cases"}).
1.29
1.30 - It is not entirely clear in which context it is better to use
1.31 - the one or the other, or whether the construction should be reversed.
1.32 + It is not entirely clear in which context it is better to use the
1.33 + one or the other, or whether the construction should be reversed.
1.34 *}
1.35
1.36
1.37 @@ -154,18 +155,6 @@
1.38 by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
1.39 left_distrib right_distrib)
1.40
1.41 -lemma Dig_eq:
1.42 - "One = One \<longleftrightarrow> True"
1.43 - "One = Dig0 n \<longleftrightarrow> False"
1.44 - "One = Dig1 n \<longleftrightarrow> False"
1.45 - "Dig0 m = One \<longleftrightarrow> False"
1.46 - "Dig1 m = One \<longleftrightarrow> False"
1.47 - "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
1.48 - "Dig0 m = Dig1 n \<longleftrightarrow> False"
1.49 - "Dig1 m = Dig0 n \<longleftrightarrow> False"
1.50 - "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
1.51 - by simp_all
1.52 -
1.53 lemma less_eq_num_code [numeral, simp, code]:
1.54 "One \<le> n \<longleftrightarrow> True"
1.55 "Dig0 m \<le> One \<longleftrightarrow> False"
1.56 @@ -207,8 +196,8 @@
1.57
1.58 primrec DigM :: "num \<Rightarrow> num" where
1.59 "DigM One = One"
1.60 - | "DigM (Dig0 n) = Dig1 (DigM n)"
1.61 - | "DigM (Dig1 n) = Dig1 (Dig0 n)"
1.62 +| "DigM (Dig0 n) = Dig1 (DigM n)"
1.63 +| "DigM (Dig1 n) = Dig1 (Dig0 n)"
1.64
1.65 lemma DigM_plus_one: "DigM n + One = Dig0 n"
1.66 by (induct n) simp_all
1.67 @@ -217,7 +206,7 @@
1.68 by (induct n) simp_all
1.69
1.70 lemma one_plus_DigM: "One + DigM n = Dig0 n"
1.71 - unfolding add_One_commute DigM_plus_one ..
1.72 + by (simp add: add_One_commute DigM_plus_one)
1.73
1.74 text {* Squaring and exponentiation *}
1.75
1.76 @@ -226,8 +215,7 @@
1.77 | "square (Dig0 n) = Dig0 (Dig0 (square n))"
1.78 | "square (Dig1 n) = Dig1 (Dig0 (square n + n))"
1.79
1.80 -primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
1.81 -where
1.82 +primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where
1.83 "pow x One = x"
1.84 | "pow x (Dig0 y) = square (pow x y)"
1.85 | "pow x (Dig1 y) = x * square (pow x y)"
1.86 @@ -245,31 +233,22 @@
1.87
1.88 primrec of_num :: "num \<Rightarrow> 'a" where
1.89 of_num_One [numeral]: "of_num One = 1"
1.90 - | "of_num (Dig0 n) = of_num n + of_num n"
1.91 - | "of_num (Dig1 n) = of_num n + of_num n + 1"
1.92 +| "of_num (Dig0 n) = of_num n + of_num n"
1.93 +| "of_num (Dig1 n) = of_num n + of_num n + 1"
1.94
1.95 -lemma of_num_inc: "of_num (inc x) = of_num x + 1"
1.96 - by (induct x) (simp_all add: add_ac)
1.97 +lemma of_num_inc: "of_num (inc n) = of_num n + 1"
1.98 + by (induct n) (simp_all add: add_ac)
1.99
1.100 lemma of_num_add: "of_num (m + n) = of_num m + of_num n"
1.101 - apply (induct n rule: num_induct)
1.102 - apply (simp_all add: add_One add_inc of_num_inc add_ac)
1.103 - done
1.104 + by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac)
1.105
1.106 lemma of_num_mult: "of_num (m * n) = of_num m * of_num n"
1.107 - apply (induct n rule: num_induct)
1.108 - apply (simp add: mult_One)
1.109 - apply (simp add: mult_inc of_num_add of_num_inc right_distrib)
1.110 - done
1.111 + by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib)
1.112
1.113 declare of_num.simps [simp del]
1.114
1.115 end
1.116
1.117 -text {*
1.118 - ML stuff and syntax.
1.119 -*}
1.120 -
1.121 ML {*
1.122 fun mk_num k =
1.123 if k > 1 then
1.124 @@ -285,13 +264,13 @@
1.125 | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1
1.126 | dest_num t = raise TERM ("dest_num", [t]);
1.127
1.128 -(*FIXME these have to gain proper context via morphisms phi*)
1.129 -
1.130 -fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T)
1.131 +fun mk_numeral phi T k = Morphism.term phi (Const (@{const_name of_num}, @{typ num} --> T))
1.132 $ mk_num k
1.133
1.134 -fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) =
1.135 - (T, dest_num t)
1.136 +fun dest_numeral phi (u $ t) =
1.137 + if Term.aconv_untyped (u, Morphism.term phi (Const (@{const_name of_num}, dummyT)))
1.138 + then (range_type (fastype_of u), dest_num t)
1.139 + else raise TERM ("dest_numeral", [u, t]);
1.140 *}
1.141
1.142 syntax
1.143 @@ -335,12 +314,9 @@
1.144 in [(@{const_syntax of_num}, num_tr')] end
1.145 *}
1.146
1.147 +
1.148 subsection {* Class-specific numeral rules *}
1.149
1.150 -text {*
1.151 - @{const of_num} is a morphism.
1.152 -*}
1.153 -
1.154 subsubsection {* Class @{text semiring_numeral} *}
1.155
1.156 context semiring_numeral
1.157 @@ -349,11 +325,10 @@
1.158 abbreviation "Num1 \<equiv> of_num One"
1.159
1.160 text {*
1.161 - Alas, there is still the duplication of @{term 1},
1.162 - thought the duplicated @{term 0} has disappeared.
1.163 - We could get rid of it by replacing the constructor
1.164 - @{term 1} in @{typ num} by two constructors
1.165 - @{text two} and @{text three}, resulting in a further
1.166 + Alas, there is still the duplication of @{term 1}, although the
1.167 + duplicated @{term 0} has disappeared. We could get rid of it by
1.168 + replacing the constructor @{term 1} in @{typ num} by two
1.169 + constructors @{text two} and @{text three}, resulting in a further
1.170 blow-up. But it could be worth the effort.
1.171 *}
1.172
1.173 @@ -367,7 +342,7 @@
1.174
1.175 lemma of_num_plus [numeral]:
1.176 "of_num m + of_num n = of_num (m + n)"
1.177 - unfolding of_num_add ..
1.178 + by (simp only: of_num_add)
1.179
1.180 lemma of_num_times_one [numeral]:
1.181 "of_num n * 1 = of_num n"
1.182 @@ -383,9 +358,8 @@
1.183
1.184 end
1.185
1.186 -subsubsection {*
1.187 - Structures with a zero: class @{text semiring_1}
1.188 -*}
1.189 +
1.190 +subsubsection {* Structures with a zero: class @{text semiring_1} *}
1.191
1.192 context semiring_1
1.193 begin
1.194 @@ -422,9 +396,8 @@
1.195 then show "nat_of_num n = of_num n" by simp
1.196 qed
1.197
1.198 -subsubsection {*
1.199 - Equality: class @{text semiring_char_0}
1.200 -*}
1.201 +
1.202 +subsubsection {* Equality: class @{text semiring_char_0} *}
1.203
1.204 context semiring_char_0
1.205 begin
1.206 @@ -441,18 +414,23 @@
1.207
1.208 end
1.209
1.210 -subsubsection {*
1.211 - Comparisons: class @{text linordered_semidom}
1.212 +
1.213 +subsubsection {* Comparisons: class @{text linordered_semidom} *}
1.214 +
1.215 +text {*
1.216 + Perhaps the underlying structure could even
1.217 + be more general than @{text linordered_semidom}.
1.218 *}
1.219
1.220 -text {* Could be perhaps more general than here. *}
1.221 -
1.222 context linordered_semidom
1.223 begin
1.224
1.225 lemma of_num_pos [numeral]: "0 < of_num n"
1.226 by (induct n) (simp_all add: of_num.simps add_pos_pos)
1.227
1.228 +lemma of_num_not_zero [numeral]: "of_num n \<noteq> 0"
1.229 + using of_num_pos [of n] by simp
1.230 +
1.231 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n"
1.232 proof -
1.233 have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n"
1.234 @@ -500,6 +478,9 @@
1.235 finally show ?thesis .
1.236 qed
1.237
1.238 +lemma minus_of_num_not_equal_of_num: "- of_num m \<noteq> of_num n"
1.239 + using minus_of_num_less_of_num_iff [of m n] by simp
1.240 +
1.241 lemma minus_of_num_less_one_iff: "- of_num n < 1"
1.242 using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One)
1.243
1.244 @@ -557,6 +538,7 @@
1.245
1.246 lemmas less_signed_numeral_special [numeral] =
1.247 minus_of_num_less_of_num_iff
1.248 + minus_of_num_not_equal_of_num
1.249 minus_of_num_less_one_iff
1.250 minus_one_less_of_num_iff
1.251 minus_one_less_one_iff
1.252 @@ -567,9 +549,7 @@
1.253
1.254 end
1.255
1.256 -subsubsection {*
1.257 - Structures with subtraction: class @{text semiring_1_minus}
1.258 -*}
1.259 +subsubsection {* Structures with subtraction: class @{text semiring_1_minus} *}
1.260
1.261 class semiring_minus = semiring + minus + zero +
1.262 assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
1.263 @@ -612,8 +592,9 @@
1.264 fun attach_num ct = (dest_num (Thm.term_of ct), ct);
1.265 fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;
1.266 val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
1.267 - fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
1.268 - [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
1.269 + fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq}
1.270 + OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
1.271 + [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
1.272 in fn phi => fn _ => fn ct => case try cdifference ct
1.273 of NONE => (NONE)
1.274 | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0
1.275 @@ -651,15 +632,14 @@
1.276
1.277 end
1.278
1.279 -subsubsection {*
1.280 - Structures with negation: class @{text ring_1}
1.281 -*}
1.282 +
1.283 +subsubsection {* Structures with negation: class @{text ring_1} *}
1.284
1.285 context ring_1
1.286 begin
1.287
1.288 -subclass semiring_1_minus
1.289 - proof qed (simp_all add: algebra_simps)
1.290 +subclass semiring_1_minus proof
1.291 +qed (simp_all add: algebra_simps)
1.292
1.293 lemma Dig_zero_minus_of_num [numeral]:
1.294 "0 - of_num n = - of_num n"
1.295 @@ -696,9 +676,8 @@
1.296
1.297 end
1.298
1.299 -subsubsection {*
1.300 - Structures with exponentiation
1.301 -*}
1.302 +
1.303 +subsubsection {* Structures with exponentiation *}
1.304
1.305 lemma of_num_square: "of_num (square x) = of_num x * of_num x"
1.306 by (induct x)
1.307 @@ -729,11 +708,10 @@
1.308 declare power_one [numeral]
1.309
1.310
1.311 -subsubsection {*
1.312 - Greetings to @{typ nat}.
1.313 -*}
1.314 +subsubsection {* Greetings to @{typ nat}. *}
1.315
1.316 -instance nat :: semiring_1_minus proof qed simp_all
1.317 +instance nat :: semiring_1_minus proof
1.318 +qed simp_all
1.319
1.320 lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)"
1.321 unfolding of_num_plus_one [symmetric] by simp
1.322 @@ -748,141 +726,9 @@
1.323 declare diff_0_eq_0 [numeral]
1.324
1.325
1.326 -subsection {* Code generator setup for @{typ int} *}
1.327 +subsection {* Proof tools setup *}
1.328
1.329 -definition Pls :: "num \<Rightarrow> int" where
1.330 - [simp, code_post]: "Pls n = of_num n"
1.331 -
1.332 -definition Mns :: "num \<Rightarrow> int" where
1.333 - [simp, code_post]: "Mns n = - of_num n"
1.334 -
1.335 -code_datatype "0::int" Pls Mns
1.336 -
1.337 -lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
1.338 -
1.339 -definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1.340 - [simp]: "sub m n = (of_num m - of_num n)"
1.341 -
1.342 -definition dup :: "int \<Rightarrow> int" where
1.343 - "dup k = 2 * k"
1.344 -
1.345 -lemma Dig_sub [code]:
1.346 - "sub One One = 0"
1.347 - "sub (Dig0 m) One = of_num (DigM m)"
1.348 - "sub (Dig1 m) One = of_num (Dig0 m)"
1.349 - "sub One (Dig0 n) = - of_num (DigM n)"
1.350 - "sub One (Dig1 n) = - of_num (Dig0 n)"
1.351 - "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
1.352 - "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
1.353 - "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
1.354 - "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
1.355 - apply (simp_all add: dup_def algebra_simps)
1.356 - apply (simp_all add: of_num_plus one_plus_DigM)[4]
1.357 - apply (simp_all add: of_num.simps)
1.358 - done
1.359 -
1.360 -lemma dup_code [code]:
1.361 - "dup 0 = 0"
1.362 - "dup (Pls n) = Pls (Dig0 n)"
1.363 - "dup (Mns n) = Mns (Dig0 n)"
1.364 - by (simp_all add: dup_def of_num.simps)
1.365 -
1.366 -lemma [code, code del]:
1.367 - "(1 :: int) = 1"
1.368 - "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
1.369 - "(uminus :: int \<Rightarrow> int) = uminus"
1.370 - "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
1.371 - "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
1.372 - "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
1.373 - "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
1.374 - "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
1.375 - by rule+
1.376 -
1.377 -lemma one_int_code [code]:
1.378 - "1 = Pls One"
1.379 - by (simp add: of_num_One)
1.380 -
1.381 -lemma plus_int_code [code]:
1.382 - "k + 0 = (k::int)"
1.383 - "0 + l = (l::int)"
1.384 - "Pls m + Pls n = Pls (m + n)"
1.385 - "Pls m - Pls n = sub m n"
1.386 - "Mns m + Mns n = Mns (m + n)"
1.387 - "Mns m - Mns n = sub n m"
1.388 - by (simp_all add: of_num_add)
1.389 -
1.390 -lemma uminus_int_code [code]:
1.391 - "uminus 0 = (0::int)"
1.392 - "uminus (Pls m) = Mns m"
1.393 - "uminus (Mns m) = Pls m"
1.394 - by simp_all
1.395 -
1.396 -lemma minus_int_code [code]:
1.397 - "k - 0 = (k::int)"
1.398 - "0 - l = uminus (l::int)"
1.399 - "Pls m - Pls n = sub m n"
1.400 - "Pls m - Mns n = Pls (m + n)"
1.401 - "Mns m - Pls n = Mns (m + n)"
1.402 - "Mns m - Mns n = sub n m"
1.403 - by (simp_all add: of_num_add)
1.404 -
1.405 -lemma times_int_code [code]:
1.406 - "k * 0 = (0::int)"
1.407 - "0 * l = (0::int)"
1.408 - "Pls m * Pls n = Pls (m * n)"
1.409 - "Pls m * Mns n = Mns (m * n)"
1.410 - "Mns m * Pls n = Mns (m * n)"
1.411 - "Mns m * Mns n = Pls (m * n)"
1.412 - by (simp_all add: of_num_mult)
1.413 -
1.414 -lemma eq_int_code [code]:
1.415 - "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
1.416 - "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
1.417 - "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
1.418 - "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
1.419 - "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
1.420 - "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
1.421 - "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
1.422 - "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
1.423 - "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
1.424 - using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
1.425 - by (simp_all add: of_num_eq_iff eq)
1.426 -
1.427 -lemma less_eq_int_code [code]:
1.428 - "0 \<le> (0::int) \<longleftrightarrow> True"
1.429 - "0 \<le> Pls l \<longleftrightarrow> True"
1.430 - "0 \<le> Mns l \<longleftrightarrow> False"
1.431 - "Pls k \<le> 0 \<longleftrightarrow> False"
1.432 - "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"
1.433 - "Pls k \<le> Mns l \<longleftrightarrow> False"
1.434 - "Mns k \<le> 0 \<longleftrightarrow> True"
1.435 - "Mns k \<le> Pls l \<longleftrightarrow> True"
1.436 - "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"
1.437 - using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
1.438 - by (simp_all add: of_num_less_eq_iff)
1.439 -
1.440 -lemma less_int_code [code]:
1.441 - "0 < (0::int) \<longleftrightarrow> False"
1.442 - "0 < Pls l \<longleftrightarrow> True"
1.443 - "0 < Mns l \<longleftrightarrow> False"
1.444 - "Pls k < 0 \<longleftrightarrow> False"
1.445 - "Pls k < Pls l \<longleftrightarrow> k < l"
1.446 - "Pls k < Mns l \<longleftrightarrow> False"
1.447 - "Mns k < 0 \<longleftrightarrow> True"
1.448 - "Mns k < Pls l \<longleftrightarrow> True"
1.449 - "Mns k < Mns l \<longleftrightarrow> l < k"
1.450 - using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
1.451 - by (simp_all add: of_num_less_iff)
1.452 -
1.453 -lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
1.454 -lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
1.455 -declare zero_is_num_zero [code_unfold del]
1.456 -declare one_is_num_one [code_unfold del]
1.457 -
1.458 -hide_const (open) sub dup
1.459 -
1.460 -
1.461 -subsection {* Numeral equations as default simplification rules *}
1.462 +subsubsection {* Numeral equations as default simplification rules *}
1.463
1.464 declare (in semiring_numeral) of_num_One [simp]
1.465 declare (in semiring_numeral) of_num_plus_one [simp]
1.466 @@ -897,6 +743,7 @@
1.467 declare (in semiring_char_0) one_eq_of_num_iff [simp]
1.468
1.469 declare (in linordered_semidom) of_num_pos [simp]
1.470 +declare (in linordered_semidom) of_num_not_zero [simp]
1.471 declare (in linordered_semidom) of_num_less_eq_iff [simp]
1.472 declare (in linordered_semidom) of_num_less_eq_one_iff [simp]
1.473 declare (in linordered_semidom) one_less_eq_of_num_iff [simp]
1.474 @@ -924,8 +771,6 @@
1.475 declare Suc_of_num [simp]
1.476
1.477
1.478 -subsection {* Simplification Procedures *}
1.479 -
1.480 subsubsection {* Reorientation of equalities *}
1.481
1.482 setup {*
1.483 @@ -985,12 +830,282 @@
1.484 Semiring_Times_Assoc.proc ss (Thm.term_of ct) *}
1.485
1.486
1.487 +subsection {* Code generator setup for @{typ int} *}
1.488 +
1.489 +text {* Reversing standard setup *}
1.490 +
1.491 +lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
1.492 +lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
1.493 +declare zero_is_num_zero [code_unfold del]
1.494 +declare one_is_num_one [code_unfold del]
1.495 +
1.496 +lemma [code, code del]:
1.497 + "(1 :: int) = 1"
1.498 + "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
1.499 + "(uminus :: int \<Rightarrow> int) = uminus"
1.500 + "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
1.501 + "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
1.502 + "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
1.503 + "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
1.504 + "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
1.505 + by rule+
1.506 +
1.507 +text {* Constructors *}
1.508 +
1.509 +definition Pls :: "num \<Rightarrow> int" where
1.510 + [simp, code_post]: "Pls n = of_num n"
1.511 +
1.512 +definition Mns :: "num \<Rightarrow> int" where
1.513 + [simp, code_post]: "Mns n = - of_num n"
1.514 +
1.515 +code_datatype "0::int" Pls Mns
1.516 +
1.517 +lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
1.518 +
1.519 +text {* Auxiliary operations *}
1.520 +
1.521 +definition dup :: "int \<Rightarrow> int" where
1.522 + [simp]: "dup k = k + k"
1.523 +
1.524 +lemma Dig_dup [code]:
1.525 + "dup 0 = 0"
1.526 + "dup (Pls n) = Pls (Dig0 n)"
1.527 + "dup (Mns n) = Mns (Dig0 n)"
1.528 + by (simp_all add: of_num.simps)
1.529 +
1.530 +definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
1.531 + [simp]: "sub m n = (of_num m - of_num n)"
1.532 +
1.533 +lemma Dig_sub [code]:
1.534 + "sub One One = 0"
1.535 + "sub (Dig0 m) One = of_num (DigM m)"
1.536 + "sub (Dig1 m) One = of_num (Dig0 m)"
1.537 + "sub One (Dig0 n) = - of_num (DigM n)"
1.538 + "sub One (Dig1 n) = - of_num (Dig0 n)"
1.539 + "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
1.540 + "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
1.541 + "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
1.542 + "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
1.543 + by (simp_all add: algebra_simps num_eq_iff nat_of_num_add)
1.544 +
1.545 +text {* Implementations *}
1.546 +
1.547 +lemma one_int_code [code]:
1.548 + "1 = Pls One"
1.549 + by (simp add: of_num_One)
1.550 +
1.551 +lemma plus_int_code [code]:
1.552 + "k + 0 = (k::int)"
1.553 + "0 + l = (l::int)"
1.554 + "Pls m + Pls n = Pls (m + n)"
1.555 + "Pls m + Mns n = sub m n"
1.556 + "Mns m + Pls n = sub n m"
1.557 + "Mns m + Mns n = Mns (m + n)"
1.558 + by simp_all
1.559 +
1.560 +lemma uminus_int_code [code]:
1.561 + "uminus 0 = (0::int)"
1.562 + "uminus (Pls m) = Mns m"
1.563 + "uminus (Mns m) = Pls m"
1.564 + by simp_all
1.565 +
1.566 +lemma minus_int_code [code]:
1.567 + "k - 0 = (k::int)"
1.568 + "0 - l = uminus (l::int)"
1.569 + "Pls m - Pls n = sub m n"
1.570 + "Pls m - Mns n = Pls (m + n)"
1.571 + "Mns m - Pls n = Mns (m + n)"
1.572 + "Mns m - Mns n = sub n m"
1.573 + by simp_all
1.574 +
1.575 +lemma times_int_code [code]:
1.576 + "k * 0 = (0::int)"
1.577 + "0 * l = (0::int)"
1.578 + "Pls m * Pls n = Pls (m * n)"
1.579 + "Pls m * Mns n = Mns (m * n)"
1.580 + "Mns m * Pls n = Mns (m * n)"
1.581 + "Mns m * Mns n = Pls (m * n)"
1.582 + by simp_all
1.583 +
1.584 +lemma eq_int_code [code]:
1.585 + "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
1.586 + "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
1.587 + "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
1.588 + "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
1.589 + "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
1.590 + "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
1.591 + "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
1.592 + "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
1.593 + "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
1.594 + by (auto simp add: eq dest: sym)
1.595 +
1.596 +lemma less_eq_int_code [code]:
1.597 + "0 \<le> (0::int) \<longleftrightarrow> True"
1.598 + "0 \<le> Pls l \<longleftrightarrow> True"
1.599 + "0 \<le> Mns l \<longleftrightarrow> False"
1.600 + "Pls k \<le> 0 \<longleftrightarrow> False"
1.601 + "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l"
1.602 + "Pls k \<le> Mns l \<longleftrightarrow> False"
1.603 + "Mns k \<le> 0 \<longleftrightarrow> True"
1.604 + "Mns k \<le> Pls l \<longleftrightarrow> True"
1.605 + "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k"
1.606 + by simp_all
1.607 +
1.608 +lemma less_int_code [code]:
1.609 + "0 < (0::int) \<longleftrightarrow> False"
1.610 + "0 < Pls l \<longleftrightarrow> True"
1.611 + "0 < Mns l \<longleftrightarrow> False"
1.612 + "Pls k < 0 \<longleftrightarrow> False"
1.613 + "Pls k < Pls l \<longleftrightarrow> k < l"
1.614 + "Pls k < Mns l \<longleftrightarrow> False"
1.615 + "Mns k < 0 \<longleftrightarrow> True"
1.616 + "Mns k < Pls l \<longleftrightarrow> True"
1.617 + "Mns k < Mns l \<longleftrightarrow> l < k"
1.618 + by simp_all
1.619 +
1.620 +hide_const (open) sub dup
1.621 +
1.622 +text {* Pretty literals *}
1.623 +
1.624 +ML {*
1.625 +local open Code_Thingol in
1.626 +
1.627 +fun add_code print target =
1.628 + let
1.629 + fun dest_num one' dig0' dig1' thm =
1.630 + let
1.631 + fun dest_dig (IConst (c, _)) = if c = dig0' then 0
1.632 + else if c = dig1' then 1
1.633 + else Code_Printer.eqn_error thm "Illegal numeral expression: illegal dig"
1.634 + | dest_dig _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal digit";
1.635 + fun dest_num (IConst (c, _)) = if c = one' then 1
1.636 + else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
1.637 + | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_dig t1
1.638 + | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
1.639 + in dest_num end;
1.640 + fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] =
1.641 + (Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t
1.642 + fun add_syntax (c, sgn) = Code_Target.add_syntax_const target c
1.643 + (SOME (Code_Printer.complex_const_syntax
1.644 + (1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}],
1.645 + pretty sgn))));
1.646 + in
1.647 + add_syntax (@{const_name Pls}, I)
1.648 + #> add_syntax (@{const_name Mns}, (fn k => ~ k))
1.649 + end;
1.650 +
1.651 +end
1.652 +*}
1.653 +
1.654 +hide_const (open) One Dig0 Dig1
1.655 +
1.656 +
1.657 subsection {* Toy examples *}
1.658
1.659 -definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
1.660 +definition "foo \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat)"
1.661 +definition "bar \<longleftrightarrow> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
1.662
1.663 -code_thms bar
1.664 +code_thms foo bar
1.665 +export_code foo bar checking SML OCaml? Haskell? Scala?
1.666
1.667 -export_code bar checking SML OCaml? Haskell?
1.668 +text {* This is an ad-hoc @{text Code_Integer} setup. *}
1.669 +
1.670 +setup {*
1.671 + fold (add_code Code_Printer.literal_numeral)
1.672 + [Code_ML.target_SML, Code_ML.target_OCaml, Code_Haskell.target, Code_Scala.target]
1.673 +*}
1.674 +
1.675 +code_type int
1.676 + (SML "IntInf.int")
1.677 + (OCaml "Big'_int.big'_int")
1.678 + (Haskell "Integer")
1.679 + (Scala "BigInt")
1.680 + (Eval "int")
1.681 +
1.682 +code_const "0::int"
1.683 + (SML "0/ :/ IntInf.int")
1.684 + (OCaml "Big'_int.zero")
1.685 + (Haskell "0")
1.686 + (Scala "BigInt(0)")
1.687 + (Eval "0/ :/ int")
1.688 +
1.689 +code_const Int.pred
1.690 + (SML "IntInf.- ((_), 1)")
1.691 + (OCaml "Big'_int.pred'_big'_int")
1.692 + (Haskell "!(_/ -/ 1)")
1.693 + (Scala "!(_/ -/ 1)")
1.694 + (Eval "!(_/ -/ 1)")
1.695 +
1.696 +code_const Int.succ
1.697 + (SML "IntInf.+ ((_), 1)")
1.698 + (OCaml "Big'_int.succ'_big'_int")
1.699 + (Haskell "!(_/ +/ 1)")
1.700 + (Scala "!(_/ +/ 1)")
1.701 + (Eval "!(_/ +/ 1)")
1.702 +
1.703 +code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
1.704 + (SML "IntInf.+ ((_), (_))")
1.705 + (OCaml "Big'_int.add'_big'_int")
1.706 + (Haskell infixl 6 "+")
1.707 + (Scala infixl 7 "+")
1.708 + (Eval infixl 8 "+")
1.709 +
1.710 +code_const "uminus \<Colon> int \<Rightarrow> int"
1.711 + (SML "IntInf.~")
1.712 + (OCaml "Big'_int.minus'_big'_int")
1.713 + (Haskell "negate")
1.714 + (Scala "!(- _)")
1.715 + (Eval "~/ _")
1.716 +
1.717 +code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
1.718 + (SML "IntInf.- ((_), (_))")
1.719 + (OCaml "Big'_int.sub'_big'_int")
1.720 + (Haskell infixl 6 "-")
1.721 + (Scala infixl 7 "-")
1.722 + (Eval infixl 8 "-")
1.723 +
1.724 +code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
1.725 + (SML "IntInf.* ((_), (_))")
1.726 + (OCaml "Big'_int.mult'_big'_int")
1.727 + (Haskell infixl 7 "*")
1.728 + (Scala infixl 8 "*")
1.729 + (Eval infixl 9 "*")
1.730 +
1.731 +code_const pdivmod
1.732 + (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
1.733 + (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
1.734 + (Haskell "divMod/ (abs _)/ (abs _)")
1.735 + (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
1.736 + (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
1.737 +
1.738 +code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
1.739 + (SML "!((_ : IntInf.int) = _)")
1.740 + (OCaml "Big'_int.eq'_big'_int")
1.741 + (Haskell infixl 4 "==")
1.742 + (Scala infixl 5 "==")
1.743 + (Eval infixl 6 "=")
1.744 +
1.745 +code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
1.746 + (SML "IntInf.<= ((_), (_))")
1.747 + (OCaml "Big'_int.le'_big'_int")
1.748 + (Haskell infix 4 "<=")
1.749 + (Scala infixl 4 "<=")
1.750 + (Eval infixl 6 "<=")
1.751 +
1.752 +code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
1.753 + (SML "IntInf.< ((_), (_))")
1.754 + (OCaml "Big'_int.lt'_big'_int")
1.755 + (Haskell infix 4 "<")
1.756 + (Scala infixl 4 "<")
1.757 + (Eval infixl 6 "<")
1.758 +
1.759 +code_const Code_Numeral.int_of
1.760 + (SML "IntInf.fromInt")
1.761 + (OCaml "_")
1.762 + (Haskell "toInteger")
1.763 + (Scala "!_.as'_BigInt")
1.764 + (Eval "_")
1.765 +
1.766 +export_code foo bar checking SML OCaml? Haskell? Scala?
1.767
1.768 end