src/HOL/Library/Code_Target_Int.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61856 4b1b85f38944
child 63351 e5d08b1d8fea
permissions -rw-r--r--
more symbols;
haftmann@50023
     1
(*  Title:      HOL/Library/Code_Target_Int.thy
haftmann@50023
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@50023
     3
*)
haftmann@50023
     4
wenzelm@60500
     5
section \<open>Implementation of integer numbers by target-language integers\<close>
haftmann@50023
     6
haftmann@50023
     7
theory Code_Target_Int
Andreas@61856
     8
imports "../GCD"
haftmann@50023
     9
begin
haftmann@50023
    10
haftmann@50023
    11
code_datatype int_of_integer
haftmann@50023
    12
haftmann@54891
    13
declare [[code drop: integer_of_int]]
haftmann@50023
    14
kuncar@55736
    15
context
kuncar@55736
    16
includes integer.lifting
kuncar@55736
    17
begin
kuncar@55736
    18
haftmann@50023
    19
lemma [code]:
haftmann@50023
    20
  "integer_of_int (int_of_integer k) = k"
haftmann@51114
    21
  by transfer rule
haftmann@50023
    22
haftmann@50023
    23
lemma [code]:
haftmann@50023
    24
  "Int.Pos = int_of_integer \<circ> integer_of_num"
haftmann@51114
    25
  by transfer (simp add: fun_eq_iff) 
haftmann@50023
    26
haftmann@50023
    27
lemma [code]:
haftmann@50023
    28
  "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
haftmann@51114
    29
  by transfer (simp add: fun_eq_iff) 
haftmann@50023
    30
haftmann@50023
    31
lemma [code_abbrev]:
haftmann@51095
    32
  "int_of_integer (numeral k) = Int.Pos k"
haftmann@51114
    33
  by transfer simp
haftmann@50023
    34
haftmann@50023
    35
lemma [code_abbrev]:
haftmann@54489
    36
  "int_of_integer (- numeral k) = Int.Neg k"
haftmann@51114
    37
  by transfer simp
haftmann@51095
    38
  
haftmann@51095
    39
lemma [code, symmetric, code_post]:
haftmann@50023
    40
  "0 = int_of_integer 0"
haftmann@51114
    41
  by transfer simp
haftmann@50023
    42
haftmann@51095
    43
lemma [code, symmetric, code_post]:
haftmann@50023
    44
  "1 = int_of_integer 1"
haftmann@51114
    45
  by transfer simp
haftmann@50023
    46
haftmann@58099
    47
lemma [code_post]:
haftmann@58099
    48
  "int_of_integer (- 1) = - 1"
haftmann@58099
    49
  by simp
haftmann@58099
    50
haftmann@50023
    51
lemma [code]:
haftmann@50023
    52
  "k + l = int_of_integer (of_int k + of_int l)"
haftmann@51114
    53
  by transfer simp
haftmann@50023
    54
haftmann@50023
    55
lemma [code]:
haftmann@50023
    56
  "- k = int_of_integer (- of_int k)"
haftmann@51114
    57
  by transfer simp
haftmann@50023
    58
haftmann@50023
    59
lemma [code]:
haftmann@50023
    60
  "k - l = int_of_integer (of_int k - of_int l)"
haftmann@51114
    61
  by transfer simp
haftmann@50023
    62
haftmann@50023
    63
lemma [code]:
haftmann@51143
    64
  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
haftmann@51114
    65
  by transfer simp
haftmann@50023
    66
haftmann@54891
    67
declare [[code drop: Int.sub]]
haftmann@50023
    68
haftmann@50023
    69
lemma [code]:
haftmann@50023
    70
  "k * l = int_of_integer (of_int k * of_int l)"
haftmann@50023
    71
  by simp
haftmann@50023
    72
haftmann@50023
    73
lemma [code]:
haftmann@50023
    74
  "k div l = int_of_integer (of_int k div of_int l)"
haftmann@50023
    75
  by simp
haftmann@50023
    76
haftmann@50023
    77
lemma [code]:
haftmann@50023
    78
  "k mod l = int_of_integer (of_int k mod of_int l)"
haftmann@50023
    79
  by simp
haftmann@50023
    80
haftmann@50023
    81
lemma [code]:
haftmann@61275
    82
  "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
haftmann@61275
    83
  unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
haftmann@61275
    84
  by transfer simp
haftmann@61275
    85
haftmann@61275
    86
lemma [code]:
haftmann@50023
    87
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
haftmann@51114
    88
  by transfer (simp add: equal)
haftmann@50023
    89
haftmann@50023
    90
lemma [code]:
haftmann@50023
    91
  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
haftmann@51114
    92
  by transfer rule
haftmann@50023
    93
haftmann@50023
    94
lemma [code]:
haftmann@50023
    95
  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
haftmann@51114
    96
  by transfer rule
Andreas@61856
    97
Andreas@61856
    98
lemma gcd_int_of_integer [code]:
Andreas@61856
    99
  "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
Andreas@61856
   100
by transfer rule
Andreas@61856
   101
Andreas@61856
   102
lemma lcm_int_of_integer [code]:
Andreas@61856
   103
  "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
Andreas@61856
   104
by transfer rule
Andreas@61856
   105
kuncar@55736
   106
end
haftmann@50023
   107
haftmann@54796
   108
lemma (in ring_1) of_int_code_if:
haftmann@50023
   109
  "of_int k = (if k = 0 then 0
haftmann@50023
   110
     else if k < 0 then - of_int (- k)
haftmann@50023
   111
     else let
haftmann@60868
   112
       l = 2 * of_int (k div 2);
haftmann@60868
   113
       j = k mod 2
haftmann@60868
   114
     in if j = 0 then l else l + 1)"
haftmann@50023
   115
proof -
haftmann@50023
   116
  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
haftmann@50023
   117
  show ?thesis
haftmann@60868
   118
    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
haftmann@50023
   119
qed
haftmann@50023
   120
haftmann@54796
   121
declare of_int_code_if [code]
haftmann@50023
   122
haftmann@50023
   123
lemma [code]:
haftmann@50023
   124
  "nat = nat_of_integer \<circ> of_int"
kuncar@55736
   125
  including integer.lifting by transfer (simp add: fun_eq_iff)
haftmann@50023
   126
haftmann@52435
   127
code_identifier
haftmann@52435
   128
  code_module Code_Target_Int \<rightharpoonup>
haftmann@52435
   129
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@50023
   130
haftmann@50023
   131
end