1(* Title: HOL/Code_Numeral.thy 2 Author: Florian Haftmann, TU Muenchen 3*) 4 5section \<open>Numeric types for code generation onto target language numerals only\<close> 6 7theory Code_Numeral 8imports Divides Lifting 9begin 10 11subsection \<open>Type of target language integers\<close> 12 13typedef integer = "UNIV :: int set" 14 morphisms int_of_integer integer_of_int .. 15 16setup_lifting type_definition_integer 17 18lemma integer_eq_iff: 19 "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l" 20 by transfer rule 21 22lemma integer_eqI: 23 "int_of_integer k = int_of_integer l \<Longrightarrow> k = l" 24 using integer_eq_iff [of k l] by simp 25 26lemma int_of_integer_integer_of_int [simp]: 27 "int_of_integer (integer_of_int k) = k" 28 by transfer rule 29 30lemma integer_of_int_int_of_integer [simp]: 31 "integer_of_int (int_of_integer k) = k" 32 by transfer rule 33 34instantiation integer :: ring_1 35begin 36 37lift_definition zero_integer :: integer 38 is "0 :: int" 39 . 40 41declare zero_integer.rep_eq [simp] 42 43lift_definition one_integer :: integer 44 is "1 :: int" 45 . 46 47declare one_integer.rep_eq [simp] 48 49lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 50 is "plus :: int \<Rightarrow> int \<Rightarrow> int" 51 . 52 53declare plus_integer.rep_eq [simp] 54 55lift_definition uminus_integer :: "integer \<Rightarrow> integer" 56 is "uminus :: int \<Rightarrow> int" 57 . 58 59declare uminus_integer.rep_eq [simp] 60 61lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 62 is "minus :: int \<Rightarrow> int \<Rightarrow> int" 63 . 64 65declare minus_integer.rep_eq [simp] 66 67lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 68 is "times :: int \<Rightarrow> int \<Rightarrow> int" 69 . 70 71declare times_integer.rep_eq [simp] 72 73instance proof 74qed (transfer, simp add: algebra_simps)+ 75 76end 77 78instance integer :: Rings.dvd .. 79 80lemma [transfer_rule]: 81 "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd" 82 unfolding dvd_def by transfer_prover 83 84lemma [transfer_rule]: 85 "rel_fun (=) pcr_integer (of_bool :: bool \<Rightarrow> int) (of_bool :: bool \<Rightarrow> integer)" 86 by (unfold of_bool_def [abs_def]) transfer_prover 87 88lemma [transfer_rule]: 89 "rel_fun (=) pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)" 90 by (rule transfer_rule_of_nat) transfer_prover+ 91 92lemma [transfer_rule]: 93 "rel_fun (=) pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)" 94proof - 95 have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)" 96 by (rule transfer_rule_of_int) transfer_prover+ 97 then show ?thesis by (simp add: id_def) 98qed 99 100lemma [transfer_rule]: 101 "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)" 102 by (rule transfer_rule_numeral) transfer_prover+ 103 104lemma [transfer_rule]: 105 "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)" 106 by (unfold Num.sub_def [abs_def]) transfer_prover 107 108lemma [transfer_rule]: 109 "rel_fun pcr_integer (rel_fun (=) pcr_integer) (power :: _ \<Rightarrow> _ \<Rightarrow> int) (power :: _ \<Rightarrow> _ \<Rightarrow> integer)" 110 by (unfold power_def [abs_def]) transfer_prover 111 112lemma int_of_integer_of_nat [simp]: 113 "int_of_integer (of_nat n) = of_nat n" 114 by transfer rule 115 116lift_definition integer_of_nat :: "nat \<Rightarrow> integer" 117 is "of_nat :: nat \<Rightarrow> int" 118 . 119 120lemma integer_of_nat_eq_of_nat [code]: 121 "integer_of_nat = of_nat" 122 by transfer rule 123 124lemma int_of_integer_integer_of_nat [simp]: 125 "int_of_integer (integer_of_nat n) = of_nat n" 126 by transfer rule 127 128lift_definition nat_of_integer :: "integer \<Rightarrow> nat" 129 is Int.nat 130 . 131 132lemma nat_of_integer_of_nat [simp]: 133 "nat_of_integer (of_nat n) = n" 134 by transfer simp 135 136lemma int_of_integer_of_int [simp]: 137 "int_of_integer (of_int k) = k" 138 by transfer simp 139 140lemma nat_of_integer_integer_of_nat [simp]: 141 "nat_of_integer (integer_of_nat n) = n" 142 by transfer simp 143 144lemma integer_of_int_eq_of_int [simp, code_abbrev]: 145 "integer_of_int = of_int" 146 by transfer (simp add: fun_eq_iff) 147 148lemma of_int_integer_of [simp]: 149 "of_int (int_of_integer k) = (k :: integer)" 150 by transfer rule 151 152lemma int_of_integer_numeral [simp]: 153 "int_of_integer (numeral k) = numeral k" 154 by transfer rule 155 156lemma int_of_integer_sub [simp]: 157 "int_of_integer (Num.sub k l) = Num.sub k l" 158 by transfer rule 159 160definition integer_of_num :: "num \<Rightarrow> integer" 161 where [simp]: "integer_of_num = numeral" 162 163lemma integer_of_num [code]: 164 "integer_of_num Num.One = 1" 165 "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)" 166 "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" 167 by (simp_all only: integer_of_num_def numeral.simps Let_def) 168 169lemma integer_of_num_triv: 170 "integer_of_num Num.One = 1" 171 "integer_of_num (Num.Bit0 Num.One) = 2" 172 by simp_all 173 174instantiation integer :: "{linordered_idom, equal}" 175begin 176 177lift_definition abs_integer :: "integer \<Rightarrow> integer" 178 is "abs :: int \<Rightarrow> int" 179 . 180 181declare abs_integer.rep_eq [simp] 182 183lift_definition sgn_integer :: "integer \<Rightarrow> integer" 184 is "sgn :: int \<Rightarrow> int" 185 . 186 187declare sgn_integer.rep_eq [simp] 188 189lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool" 190 is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool" 191 . 192 193 194lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool" 195 is "less :: int \<Rightarrow> int \<Rightarrow> bool" 196 . 197 198lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool" 199 is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool" 200 . 201 202instance 203 by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+ 204 205end 206 207lemma [transfer_rule]: 208 "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)" 209 by (unfold min_def [abs_def]) transfer_prover 210 211lemma [transfer_rule]: 212 "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)" 213 by (unfold max_def [abs_def]) transfer_prover 214 215lemma int_of_integer_min [simp]: 216 "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" 217 by transfer rule 218 219lemma int_of_integer_max [simp]: 220 "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" 221 by transfer rule 222 223lemma nat_of_integer_non_positive [simp]: 224 "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0" 225 by transfer simp 226 227lemma of_nat_of_integer [simp]: 228 "of_nat (nat_of_integer k) = max 0 k" 229 by transfer auto 230 231instantiation integer :: unique_euclidean_ring 232begin 233 234lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 235 is "divide :: int \<Rightarrow> int \<Rightarrow> int" 236 . 237 238declare divide_integer.rep_eq [simp] 239 240lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 241 is "modulo :: int \<Rightarrow> int \<Rightarrow> int" 242 . 243 244declare modulo_integer.rep_eq [simp] 245 246lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat" 247 is "euclidean_size :: int \<Rightarrow> nat" 248 . 249 250declare euclidean_size_integer.rep_eq [simp] 251 252lift_definition division_segment_integer :: "integer \<Rightarrow> integer" 253 is "division_segment :: int \<Rightarrow> int" 254 . 255 256declare division_segment_integer.rep_eq [simp] 257 258instance 259 by (standard; transfer) 260 (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib 261 division_segment_mult division_segment_mod intro: div_eqI\<close>) 262 263end 264 265lemma [code]: 266 "euclidean_size = nat_of_integer \<circ> abs" 267 by (simp add: fun_eq_iff nat_of_integer.rep_eq) 268 269lemma [code]: 270 "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)" 271 by transfer (simp add: division_segment_int_def) 272 273instance integer :: ring_parity 274 by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def) 275 276lemma [transfer_rule]: 277 "rel_fun (=) (rel_fun pcr_integer pcr_integer) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)" 278 by (unfold push_bit_eq_mult [abs_def]) transfer_prover 279 280lemma [transfer_rule]: 281 "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)" 282 by (unfold take_bit_eq_mod [abs_def]) transfer_prover 283 284lemma [transfer_rule]: 285 "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)" 286 by (unfold drop_bit_eq_div [abs_def]) transfer_prover 287 288instantiation integer :: unique_euclidean_semiring_numeral 289begin 290 291definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer" 292where 293 divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)" 294 295definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer" 296where 297 "divmod_step_integer l qr = (let (q, r) = qr 298 in if r \<ge> numeral l then (2 * q + 1, r - numeral l) 299 else (2 * q, r))" 300 301instance proof 302 show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)" 303 for m n by (fact divmod_integer'_def) 304 show "divmod_step l qr = (let (q, r) = qr 305 in if r \<ge> numeral l then (2 * q + 1, r - numeral l) 306 else (2 * q, r))" for l and qr :: "integer \<times> integer" 307 by (fact divmod_step_integer_def) 308qed (transfer, 309 fact le_add_diff_inverse2 310 unique_euclidean_semiring_numeral_class.div_less 311 unique_euclidean_semiring_numeral_class.mod_less 312 unique_euclidean_semiring_numeral_class.div_positive 313 unique_euclidean_semiring_numeral_class.mod_less_eq_dividend 314 unique_euclidean_semiring_numeral_class.pos_mod_bound 315 unique_euclidean_semiring_numeral_class.pos_mod_sign 316 unique_euclidean_semiring_numeral_class.mod_mult2_eq 317 unique_euclidean_semiring_numeral_class.div_mult2_eq 318 unique_euclidean_semiring_numeral_class.discrete)+ 319 320end 321 322declare divmod_algorithm_code [where ?'a = integer, 323 folded integer_of_num_def, unfolded integer_of_num_triv, 324 code] 325 326lemma integer_of_nat_0: "integer_of_nat 0 = 0" 327by transfer simp 328 329lemma integer_of_nat_1: "integer_of_nat 1 = 1" 330by transfer simp 331 332lemma integer_of_nat_numeral: 333 "integer_of_nat (numeral n) = numeral n" 334by transfer simp 335 336 337subsection \<open>Code theorems for target language integers\<close> 338 339text \<open>Constructors\<close> 340 341definition Pos :: "num \<Rightarrow> integer" 342where 343 [simp, code_post]: "Pos = numeral" 344 345lemma [transfer_rule]: 346 "rel_fun HOL.eq pcr_integer numeral Pos" 347 by simp transfer_prover 348 349lemma Pos_fold [code_unfold]: 350 "numeral Num.One = Pos Num.One" 351 "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)" 352 "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)" 353 by simp_all 354 355definition Neg :: "num \<Rightarrow> integer" 356where 357 [simp, code_abbrev]: "Neg n = - Pos n" 358 359lemma [transfer_rule]: 360 "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg" 361 by (simp add: Neg_def [abs_def]) transfer_prover 362 363code_datatype "0::integer" Pos Neg 364 365 366text \<open>A further pair of constructors for generated computations\<close> 367 368context 369begin 370 371qualified definition positive :: "num \<Rightarrow> integer" 372 where [simp]: "positive = numeral" 373 374qualified definition negative :: "num \<Rightarrow> integer" 375 where [simp]: "negative = uminus \<circ> numeral" 376 377lemma [code_computation_unfold]: 378 "numeral = positive" 379 "Pos = positive" 380 "Neg = negative" 381 by (simp_all add: fun_eq_iff) 382 383end 384 385 386text \<open>Auxiliary operations\<close> 387 388lift_definition dup :: "integer \<Rightarrow> integer" 389 is "\<lambda>k::int. k + k" 390 . 391 392lemma dup_code [code]: 393 "dup 0 = 0" 394 "dup (Pos n) = Pos (Num.Bit0 n)" 395 "dup (Neg n) = Neg (Num.Bit0 n)" 396 by (transfer, simp only: numeral_Bit0 minus_add_distrib)+ 397 398lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer" 399 is "\<lambda>m n. numeral m - numeral n :: int" 400 . 401 402lemma sub_code [code]: 403 "sub Num.One Num.One = 0" 404 "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" 405 "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" 406 "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" 407 "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" 408 "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" 409 "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" 410 "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" 411 "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" 412 by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+ 413 414 415text \<open>Implementations\<close> 416 417lemma one_integer_code [code, code_unfold]: 418 "1 = Pos Num.One" 419 by simp 420 421lemma plus_integer_code [code]: 422 "k + 0 = (k::integer)" 423 "0 + l = (l::integer)" 424 "Pos m + Pos n = Pos (m + n)" 425 "Pos m + Neg n = sub m n" 426 "Neg m + Pos n = sub n m" 427 "Neg m + Neg n = Neg (m + n)" 428 by (transfer, simp)+ 429 430lemma uminus_integer_code [code]: 431 "uminus 0 = (0::integer)" 432 "uminus (Pos m) = Neg m" 433 "uminus (Neg m) = Pos m" 434 by simp_all 435 436lemma minus_integer_code [code]: 437 "k - 0 = (k::integer)" 438 "0 - l = uminus (l::integer)" 439 "Pos m - Pos n = sub m n" 440 "Pos m - Neg n = Pos (m + n)" 441 "Neg m - Pos n = Neg (m + n)" 442 "Neg m - Neg n = sub n m" 443 by (transfer, simp)+ 444 445lemma abs_integer_code [code]: 446 "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)" 447 by simp 448 449lemma sgn_integer_code [code]: 450 "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" 451 by simp 452 453lemma times_integer_code [code]: 454 "k * 0 = (0::integer)" 455 "0 * l = (0::integer)" 456 "Pos m * Pos n = Pos (m * n)" 457 "Pos m * Neg n = Neg (m * n)" 458 "Neg m * Pos n = Neg (m * n)" 459 "Neg m * Neg n = Pos (m * n)" 460 by simp_all 461 462definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" 463where 464 "divmod_integer k l = (k div l, k mod l)" 465 466lemma fst_divmod_integer [simp]: 467 "fst (divmod_integer k l) = k div l" 468 by (simp add: divmod_integer_def) 469 470lemma snd_divmod_integer [simp]: 471 "snd (divmod_integer k l) = k mod l" 472 by (simp add: divmod_integer_def) 473 474definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" 475where 476 "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" 477 478lemma fst_divmod_abs [simp]: 479 "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>" 480 by (simp add: divmod_abs_def) 481 482lemma snd_divmod_abs [simp]: 483 "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>" 484 by (simp add: divmod_abs_def) 485 486lemma divmod_abs_code [code]: 487 "divmod_abs (Pos k) (Pos l) = divmod k l" 488 "divmod_abs (Neg k) (Neg l) = divmod k l" 489 "divmod_abs (Neg k) (Pos l) = divmod k l" 490 "divmod_abs (Pos k) (Neg l) = divmod k l" 491 "divmod_abs j 0 = (0, \<bar>j\<bar>)" 492 "divmod_abs 0 j = (0, 0)" 493 by (simp_all add: prod_eq_iff) 494 495lemma divmod_integer_code [code]: 496 "divmod_integer k l = 497 (if k = 0 then (0, 0) else if l = 0 then (0, k) else 498 (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l 499 then divmod_abs k l 500 else (let (r, s) = divmod_abs k l in 501 if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))" 502proof - 503 have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0" 504 by (auto simp add: sgn_if) 505 have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto 506 show ?thesis 507 by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1) 508 (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) 509qed 510 511lemma div_integer_code [code]: 512 "k div l = fst (divmod_integer k l)" 513 by simp 514 515lemma mod_integer_code [code]: 516 "k mod l = snd (divmod_integer k l)" 517 by simp 518 519definition bit_cut_integer :: "integer \<Rightarrow> integer \<times> bool" 520 where "bit_cut_integer k = (k div 2, odd k)" 521 522lemma bit_cut_integer_code [code]: 523 "bit_cut_integer k = (if k = 0 then (0, False) 524 else let (r, s) = Code_Numeral.divmod_abs k 2 525 in (if k > 0 then r else - r - s, s = 1))" 526proof - 527 have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))" 528 by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one) 529 then show ?thesis 530 by (simp add: divmod_integer_code) (auto simp add: split_def) 531qed 532 533lemma equal_integer_code [code]: 534 "HOL.equal 0 (0::integer) \<longleftrightarrow> True" 535 "HOL.equal 0 (Pos l) \<longleftrightarrow> False" 536 "HOL.equal 0 (Neg l) \<longleftrightarrow> False" 537 "HOL.equal (Pos k) 0 \<longleftrightarrow> False" 538 "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" 539 "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" 540 "HOL.equal (Neg k) 0 \<longleftrightarrow> False" 541 "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" 542 "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" 543 by (simp_all add: equal) 544 545lemma equal_integer_refl [code nbe]: 546 "HOL.equal (k::integer) k \<longleftrightarrow> True" 547 by (fact equal_refl) 548 549lemma less_eq_integer_code [code]: 550 "0 \<le> (0::integer) \<longleftrightarrow> True" 551 "0 \<le> Pos l \<longleftrightarrow> True" 552 "0 \<le> Neg l \<longleftrightarrow> False" 553 "Pos k \<le> 0 \<longleftrightarrow> False" 554 "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" 555 "Pos k \<le> Neg l \<longleftrightarrow> False" 556 "Neg k \<le> 0 \<longleftrightarrow> True" 557 "Neg k \<le> Pos l \<longleftrightarrow> True" 558 "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" 559 by simp_all 560 561lemma less_integer_code [code]: 562 "0 < (0::integer) \<longleftrightarrow> False" 563 "0 < Pos l \<longleftrightarrow> True" 564 "0 < Neg l \<longleftrightarrow> False" 565 "Pos k < 0 \<longleftrightarrow> False" 566 "Pos k < Pos l \<longleftrightarrow> k < l" 567 "Pos k < Neg l \<longleftrightarrow> False" 568 "Neg k < 0 \<longleftrightarrow> True" 569 "Neg k < Pos l \<longleftrightarrow> True" 570 "Neg k < Neg l \<longleftrightarrow> l < k" 571 by simp_all 572 573lift_definition num_of_integer :: "integer \<Rightarrow> num" 574 is "num_of_nat \<circ> nat" 575 . 576 577lemma num_of_integer_code [code]: 578 "num_of_integer k = (if k \<le> 1 then Num.One 579 else let 580 (l, j) = divmod_integer k 2; 581 l' = num_of_integer l; 582 l'' = l' + l' 583 in if j = 0 then l'' else l'' + Num.One)" 584proof - 585 { 586 assume "int_of_integer k mod 2 = 1" 587 then have "nat (int_of_integer k mod 2) = nat 1" by simp 588 moreover assume *: "1 < int_of_integer k" 589 ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib) 590 have "num_of_nat (nat (int_of_integer k)) = 591 num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" 592 by simp 593 then have "num_of_nat (nat (int_of_integer k)) = 594 num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" 595 by (simp add: mult_2) 596 with ** have "num_of_nat (nat (int_of_integer k)) = 597 num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" 598 by simp 599 } 600 note aux = this 601 show ?thesis 602 by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta 603 not_le integer_eq_iff less_eq_integer_def 604 nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib 605 mult_2 [where 'a=nat] aux add_One) 606qed 607 608lemma nat_of_integer_code [code]: 609 "nat_of_integer k = (if k \<le> 0 then 0 610 else let 611 (l, j) = divmod_integer k 2; 612 l' = nat_of_integer l; 613 l'' = l' + l' 614 in if j = 0 then l'' else l'' + 1)" 615proof - 616 obtain j where k: "k = integer_of_int j" 617 proof 618 show "k = integer_of_int (int_of_integer k)" by simp 619 qed 620 have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)" if "j \<ge> 0" 621 using that by transfer (simp add: nat_mod_distrib) 622 from k show ?thesis 623 by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric] 624 minus_mod_eq_mult_div [symmetric] *) 625qed 626 627lemma int_of_integer_code [code]: 628 "int_of_integer k = (if k < 0 then - (int_of_integer (- k)) 629 else if k = 0 then 0 630 else let 631 (l, j) = divmod_integer k 2; 632 l' = 2 * int_of_integer l 633 in if j = 0 then l' else l' + 1)" 634 by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric]) 635 636lemma integer_of_int_code [code]: 637 "integer_of_int k = (if k < 0 then - (integer_of_int (- k)) 638 else if k = 0 then 0 639 else let 640 l = 2 * integer_of_int (k div 2); 641 j = k mod 2 642 in if j = 0 then l else l + 1)" 643 by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric]) 644 645hide_const (open) Pos Neg sub dup divmod_abs 646 647 648subsection \<open>Serializer setup for target language integers\<close> 649 650code_reserved Eval int Integer abs 651 652code_printing 653 type_constructor integer \<rightharpoonup> 654 (SML) "IntInf.int" 655 and (OCaml) "Big'_int.big'_int" 656 and (Haskell) "Integer" 657 and (Scala) "BigInt" 658 and (Eval) "int" 659| class_instance integer :: equal \<rightharpoonup> 660 (Haskell) - 661 662code_printing 663 constant "0::integer" \<rightharpoonup> 664 (SML) "!(0/ :/ IntInf.int)" 665 and (OCaml) "Big'_int.zero'_big'_int" 666 and (Haskell) "!(0/ ::/ Integer)" 667 and (Scala) "BigInt(0)" 668 669setup \<open> 670 fold (fn target => 671 Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target 672 #> Numeral.add_code @{const_name Code_Numeral.Neg} (~) Code_Printer.literal_numeral target) 673 ["SML", "OCaml", "Haskell", "Scala"] 674\<close> 675 676code_printing 677 constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup> 678 (SML) "IntInf.+ ((_), (_))" 679 and (OCaml) "Big'_int.add'_big'_int" 680 and (Haskell) infixl 6 "+" 681 and (Scala) infixl 7 "+" 682 and (Eval) infixl 8 "+" 683| constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup> 684 (SML) "IntInf.~" 685 and (OCaml) "Big'_int.minus'_big'_int" 686 and (Haskell) "negate" 687 and (Scala) "!(- _)" 688 and (Eval) "~/ _" 689| constant "minus :: integer \<Rightarrow> _" \<rightharpoonup> 690 (SML) "IntInf.- ((_), (_))" 691 and (OCaml) "Big'_int.sub'_big'_int" 692 and (Haskell) infixl 6 "-" 693 and (Scala) infixl 7 "-" 694 and (Eval) infixl 8 "-" 695| constant Code_Numeral.dup \<rightharpoonup> 696 (SML) "IntInf.*/ (2,/ (_))" 697 and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)" 698 and (Haskell) "!(2 * _)" 699 and (Scala) "!(2 * _)" 700 and (Eval) "!(2 * _)" 701| constant Code_Numeral.sub \<rightharpoonup> 702 (SML) "!(raise/ Fail/ \"sub\")" 703 and (OCaml) "failwith/ \"sub\"" 704 and (Haskell) "error/ \"sub\"" 705 and (Scala) "!sys.error(\"sub\")" 706| constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup> 707 (SML) "IntInf.* ((_), (_))" 708 and (OCaml) "Big'_int.mult'_big'_int" 709 and (Haskell) infixl 7 "*" 710 and (Scala) infixl 8 "*" 711 and (Eval) infixl 9 "*" 712| constant Code_Numeral.divmod_abs \<rightharpoonup> 713 (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)" 714 and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)" 715 and (Haskell) "divMod/ (abs _)/ (abs _)" 716 and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))" 717 and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)" 718| constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup> 719 (SML) "!((_ : IntInf.int) = _)" 720 and (OCaml) "Big'_int.eq'_big'_int" 721 and (Haskell) infix 4 "==" 722 and (Scala) infixl 5 "==" 723 and (Eval) infixl 6 "=" 724| constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup> 725 (SML) "IntInf.<= ((_), (_))" 726 and (OCaml) "Big'_int.le'_big'_int" 727 and (Haskell) infix 4 "<=" 728 and (Scala) infixl 4 "<=" 729 and (Eval) infixl 6 "<=" 730| constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup> 731 (SML) "IntInf.< ((_), (_))" 732 and (OCaml) "Big'_int.lt'_big'_int" 733 and (Haskell) infix 4 "<" 734 and (Scala) infixl 4 "<" 735 and (Eval) infixl 6 "<" 736| constant "abs :: integer \<Rightarrow> _" \<rightharpoonup> 737 (SML) "IntInf.abs" 738 and (OCaml) "Big'_int.abs'_big'_int" 739 and (Haskell) "Prelude.abs" 740 and (Scala) "_.abs" 741 and (Eval) "abs" 742 743code_identifier 744 code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 745 746 747subsection \<open>Type of target language naturals\<close> 748 749typedef natural = "UNIV :: nat set" 750 morphisms nat_of_natural natural_of_nat .. 751 752setup_lifting type_definition_natural 753 754lemma natural_eq_iff [termination_simp]: 755 "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n" 756 by transfer rule 757 758lemma natural_eqI: 759 "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n" 760 using natural_eq_iff [of m n] by simp 761 762lemma nat_of_natural_of_nat_inverse [simp]: 763 "nat_of_natural (natural_of_nat n) = n" 764 by transfer rule 765 766lemma natural_of_nat_of_natural_inverse [simp]: 767 "natural_of_nat (nat_of_natural n) = n" 768 by transfer rule 769 770instantiation natural :: "{comm_monoid_diff, semiring_1}" 771begin 772 773lift_definition zero_natural :: natural 774 is "0 :: nat" 775 . 776 777declare zero_natural.rep_eq [simp] 778 779lift_definition one_natural :: natural 780 is "1 :: nat" 781 . 782 783declare one_natural.rep_eq [simp] 784 785lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 786 is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 787 . 788 789declare plus_natural.rep_eq [simp] 790 791lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 792 is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat" 793 . 794 795declare minus_natural.rep_eq [simp] 796 797lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 798 is "times :: nat \<Rightarrow> nat \<Rightarrow> nat" 799 . 800 801declare times_natural.rep_eq [simp] 802 803instance proof 804qed (transfer, simp add: algebra_simps)+ 805 806end 807 808instance natural :: Rings.dvd .. 809 810lemma [transfer_rule]: 811 "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd" 812 unfolding dvd_def by transfer_prover 813 814lemma [transfer_rule]: 815 "rel_fun (=) pcr_natural (of_bool :: bool \<Rightarrow> nat) (of_bool :: bool \<Rightarrow> natural)" 816 by (unfold of_bool_def [abs_def]) transfer_prover 817 818lemma [transfer_rule]: 819 "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)" 820proof - 821 have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)" 822 by (unfold of_nat_def [abs_def]) transfer_prover 823 then show ?thesis by (simp add: id_def) 824qed 825 826lemma [transfer_rule]: 827 "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)" 828proof - 829 have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))" 830 by transfer_prover 831 then show ?thesis by simp 832qed 833 834lemma [transfer_rule]: 835 "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \<Rightarrow> _ \<Rightarrow> nat) (power :: _ \<Rightarrow> _ \<Rightarrow> natural)" 836 by (unfold power_def [abs_def]) transfer_prover 837 838lemma nat_of_natural_of_nat [simp]: 839 "nat_of_natural (of_nat n) = n" 840 by transfer rule 841 842lemma natural_of_nat_of_nat [simp, code_abbrev]: 843 "natural_of_nat = of_nat" 844 by transfer rule 845 846lemma of_nat_of_natural [simp]: 847 "of_nat (nat_of_natural n) = n" 848 by transfer rule 849 850lemma nat_of_natural_numeral [simp]: 851 "nat_of_natural (numeral k) = numeral k" 852 by transfer rule 853 854instantiation natural :: "{linordered_semiring, equal}" 855begin 856 857lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool" 858 is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool" 859 . 860 861declare less_eq_natural.rep_eq [termination_simp] 862 863lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool" 864 is "less :: nat \<Rightarrow> nat \<Rightarrow> bool" 865 . 866 867declare less_natural.rep_eq [termination_simp] 868 869lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool" 870 is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool" 871 . 872 873instance proof 874qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+ 875 876end 877 878lemma [transfer_rule]: 879 "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)" 880 by (unfold min_def [abs_def]) transfer_prover 881 882lemma [transfer_rule]: 883 "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)" 884 by (unfold max_def [abs_def]) transfer_prover 885 886lemma nat_of_natural_min [simp]: 887 "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" 888 by transfer rule 889 890lemma nat_of_natural_max [simp]: 891 "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" 892 by transfer rule 893 894instantiation natural :: unique_euclidean_semiring 895begin 896 897lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 898 is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat" 899 . 900 901declare divide_natural.rep_eq [simp] 902 903lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 904 is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat" 905 . 906 907declare modulo_natural.rep_eq [simp] 908 909lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat" 910 is "euclidean_size :: nat \<Rightarrow> nat" 911 . 912 913declare euclidean_size_natural.rep_eq [simp] 914 915lift_definition division_segment_natural :: "natural \<Rightarrow> natural" 916 is "division_segment :: nat \<Rightarrow> nat" 917 . 918 919declare division_segment_natural.rep_eq [simp] 920 921instance 922 by (standard; transfer) 923 (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc) 924 925end 926 927lemma [code]: 928 "euclidean_size = nat_of_natural" 929 by (simp add: fun_eq_iff) 930 931lemma [code]: 932 "division_segment (n::natural) = 1" 933 by (simp add: natural_eq_iff) 934 935instance natural :: linordered_semidom 936 by (standard; transfer) simp_all 937 938instance natural :: semiring_parity 939 by (standard; transfer) simp_all 940 941lemma [transfer_rule]: 942 "rel_fun (=) (rel_fun pcr_natural pcr_natural) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)" 943 by (unfold push_bit_eq_mult [abs_def]) transfer_prover 944 945lemma [transfer_rule]: 946 "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)" 947 by (unfold take_bit_eq_mod [abs_def]) transfer_prover 948 949lemma [transfer_rule]: 950 "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)" 951 by (unfold drop_bit_eq_div [abs_def]) transfer_prover 952 953lift_definition natural_of_integer :: "integer \<Rightarrow> natural" 954 is "nat :: int \<Rightarrow> nat" 955 . 956 957lift_definition integer_of_natural :: "natural \<Rightarrow> integer" 958 is "of_nat :: nat \<Rightarrow> int" 959 . 960 961lemma natural_of_integer_of_natural [simp]: 962 "natural_of_integer (integer_of_natural n) = n" 963 by transfer simp 964 965lemma integer_of_natural_of_integer [simp]: 966 "integer_of_natural (natural_of_integer k) = max 0 k" 967 by transfer auto 968 969lemma int_of_integer_of_natural [simp]: 970 "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" 971 by transfer rule 972 973lemma integer_of_natural_of_nat [simp]: 974 "integer_of_natural (of_nat n) = of_nat n" 975 by transfer rule 976 977lemma [measure_function]: 978 "is_measure nat_of_natural" 979 by (rule is_measure_trivial) 980 981 982subsection \<open>Inductive representation of target language naturals\<close> 983 984lift_definition Suc :: "natural \<Rightarrow> natural" 985 is Nat.Suc 986 . 987 988declare Suc.rep_eq [simp] 989 990old_rep_datatype "0::natural" Suc 991 by (transfer, fact nat.induct nat.inject nat.distinct)+ 992 993lemma natural_cases [case_names nat, cases type: natural]: 994 fixes m :: natural 995 assumes "\<And>n. m = of_nat n \<Longrightarrow> P" 996 shows P 997 using assms by transfer blast 998 999instantiation natural :: size 1000begin 1001 1002definition size_nat where [simp, code]: "size_nat = nat_of_natural" 1003 1004instance .. 1005 1006end 1007 1008lemma natural_decr [termination_simp]: 1009 "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n" 1010 by transfer simp 1011 1012lemma natural_zero_minus_one: "(0::natural) - 1 = 0" 1013 by (rule zero_diff) 1014 1015lemma Suc_natural_minus_one: "Suc n - 1 = n" 1016 by transfer simp 1017 1018hide_const (open) Suc 1019 1020 1021subsection \<open>Code refinement for target language naturals\<close> 1022 1023lift_definition Nat :: "integer \<Rightarrow> natural" 1024 is nat 1025 . 1026 1027lemma [code_post]: 1028 "Nat 0 = 0" 1029 "Nat 1 = 1" 1030 "Nat (numeral k) = numeral k" 1031 by (transfer, simp)+ 1032 1033lemma [code abstype]: 1034 "Nat (integer_of_natural n) = n" 1035 by transfer simp 1036 1037lemma [code]: 1038 "natural_of_nat n = natural_of_integer (integer_of_nat n)" 1039 by transfer simp 1040 1041lemma [code abstract]: 1042 "integer_of_natural (natural_of_integer k) = max 0 k" 1043 by simp 1044 1045lemma [code_abbrev]: 1046 "natural_of_integer (Code_Numeral.Pos k) = numeral k" 1047 by transfer simp 1048 1049lemma [code abstract]: 1050 "integer_of_natural 0 = 0" 1051 by transfer simp 1052 1053lemma [code abstract]: 1054 "integer_of_natural 1 = 1" 1055 by transfer simp 1056 1057lemma [code abstract]: 1058 "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1" 1059 by transfer simp 1060 1061lemma [code]: 1062 "nat_of_natural = nat_of_integer \<circ> integer_of_natural" 1063 by transfer (simp add: fun_eq_iff) 1064 1065lemma [code, code_unfold]: 1066 "case_natural f g n = (if n = 0 then f else g (n - 1))" 1067 by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) 1068 1069declare natural.rec [code del] 1070 1071lemma [code abstract]: 1072 "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" 1073 by transfer simp 1074 1075lemma [code abstract]: 1076 "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" 1077 by transfer simp 1078 1079lemma [code abstract]: 1080 "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" 1081 by transfer simp 1082 1083lemma [code abstract]: 1084 "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" 1085 by transfer (simp add: zdiv_int) 1086 1087lemma [code abstract]: 1088 "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" 1089 by transfer (simp add: zmod_int) 1090 1091lemma [code]: 1092 "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)" 1093 by transfer (simp add: equal) 1094 1095lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True" 1096 by (rule equal_class.equal_refl) 1097 1098lemma [code]: "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n" 1099 by transfer simp 1100 1101lemma [code]: "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n" 1102 by transfer simp 1103 1104hide_const (open) Nat 1105 1106lifting_update integer.lifting 1107lifting_forget integer.lifting 1108 1109lifting_update natural.lifting 1110lifting_forget natural.lifting 1111 1112code_reflect Code_Numeral 1113 datatypes natural 1114 functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural" 1115 "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _" 1116 "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _" 1117 "modulo :: natural \<Rightarrow> _" 1118 integer_of_natural natural_of_integer 1119 1120end 1121