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