src/HOL/Library/Code_Target_Int.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68028 1f9f973eed2a
permissions -rw-r--r--
tuned equation
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
wenzelm@65552
     8
imports Main
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"
wenzelm@65552
    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"
wenzelm@65552
    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@64997
    38
haftmann@64997
    39
context
wenzelm@65552
    40
begin
haftmann@64997
    41
haftmann@64997
    42
qualified definition positive :: "num \<Rightarrow> int"
haftmann@64997
    43
  where [simp]: "positive = numeral"
haftmann@64997
    44
haftmann@64997
    45
qualified definition negative :: "num \<Rightarrow> int"
haftmann@64997
    46
  where [simp]: "negative = uminus \<circ> numeral"
haftmann@64997
    47
haftmann@64997
    48
lemma [code_computation_unfold]:
haftmann@64997
    49
  "numeral = positive"
haftmann@64997
    50
  "Int.Pos = positive"
haftmann@64997
    51
  "Int.Neg = negative"
haftmann@64997
    52
  by (simp_all add: fun_eq_iff)
haftmann@64997
    53
haftmann@64997
    54
end
haftmann@64997
    55
haftmann@51095
    56
lemma [code, symmetric, code_post]:
haftmann@50023
    57
  "0 = int_of_integer 0"
haftmann@51114
    58
  by transfer simp
haftmann@50023
    59
haftmann@51095
    60
lemma [code, symmetric, code_post]:
haftmann@50023
    61
  "1 = int_of_integer 1"
haftmann@51114
    62
  by transfer simp
haftmann@50023
    63
haftmann@58099
    64
lemma [code_post]:
haftmann@58099
    65
  "int_of_integer (- 1) = - 1"
haftmann@58099
    66
  by simp
haftmann@58099
    67
haftmann@50023
    68
lemma [code]:
haftmann@50023
    69
  "k + l = int_of_integer (of_int k + of_int l)"
haftmann@51114
    70
  by transfer simp
haftmann@50023
    71
haftmann@50023
    72
lemma [code]:
haftmann@50023
    73
  "- k = int_of_integer (- of_int k)"
haftmann@51114
    74
  by transfer simp
haftmann@50023
    75
haftmann@50023
    76
lemma [code]:
haftmann@50023
    77
  "k - l = int_of_integer (of_int k - of_int l)"
haftmann@51114
    78
  by transfer simp
haftmann@50023
    79
haftmann@50023
    80
lemma [code]:
haftmann@51143
    81
  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
haftmann@51114
    82
  by transfer simp
haftmann@50023
    83
haftmann@54891
    84
declare [[code drop: Int.sub]]
haftmann@50023
    85
haftmann@50023
    86
lemma [code]:
haftmann@50023
    87
  "k * l = int_of_integer (of_int k * of_int l)"
haftmann@50023
    88
  by simp
haftmann@50023
    89
haftmann@50023
    90
lemma [code]:
haftmann@50023
    91
  "k div l = int_of_integer (of_int k div of_int l)"
haftmann@50023
    92
  by simp
haftmann@50023
    93
haftmann@50023
    94
lemma [code]:
haftmann@50023
    95
  "k mod l = int_of_integer (of_int k mod of_int l)"
haftmann@50023
    96
  by simp
haftmann@50023
    97
haftmann@50023
    98
lemma [code]:
haftmann@61275
    99
  "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
haftmann@61275
   100
  unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
haftmann@61275
   101
  by transfer simp
haftmann@61275
   102
haftmann@61275
   103
lemma [code]:
haftmann@50023
   104
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
haftmann@51114
   105
  by transfer (simp add: equal)
haftmann@50023
   106
haftmann@50023
   107
lemma [code]:
haftmann@50023
   108
  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
haftmann@51114
   109
  by transfer rule
haftmann@50023
   110
haftmann@50023
   111
lemma [code]:
haftmann@50023
   112
  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
haftmann@51114
   113
  by transfer rule
Andreas@61856
   114
haftmann@63351
   115
declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
haftmann@63351
   116
Andreas@61856
   117
lemma gcd_int_of_integer [code]:
Andreas@61856
   118
  "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
Andreas@61856
   119
by transfer rule
Andreas@61856
   120
Andreas@61856
   121
lemma lcm_int_of_integer [code]:
Andreas@61856
   122
  "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
Andreas@61856
   123
by transfer rule
Andreas@61856
   124
kuncar@55736
   125
end
haftmann@50023
   126
haftmann@54796
   127
lemma (in ring_1) of_int_code_if:
haftmann@50023
   128
  "of_int k = (if k = 0 then 0
haftmann@50023
   129
     else if k < 0 then - of_int (- k)
haftmann@50023
   130
     else let
haftmann@60868
   131
       l = 2 * of_int (k div 2);
haftmann@60868
   132
       j = k mod 2
haftmann@60868
   133
     in if j = 0 then l else l + 1)"
haftmann@50023
   134
proof -
haftmann@64242
   135
  from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
haftmann@50023
   136
  show ?thesis
haftmann@60868
   137
    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
haftmann@50023
   138
qed
haftmann@50023
   139
haftmann@54796
   140
declare of_int_code_if [code]
haftmann@50023
   141
haftmann@50023
   142
lemma [code]:
haftmann@50023
   143
  "nat = nat_of_integer \<circ> of_int"
kuncar@55736
   144
  including integer.lifting by transfer (simp add: fun_eq_iff)
haftmann@50023
   145
haftmann@68028
   146
definition char_of_int :: "int \<Rightarrow> char"
haftmann@68028
   147
  where [code_abbrev]: "char_of_int = char_of"
haftmann@68028
   148
haftmann@68028
   149
definition int_of_char :: "char \<Rightarrow> int"
haftmann@68028
   150
  where [code_abbrev]: "int_of_char = of_char"
haftmann@68028
   151
haftmann@68028
   152
lemma [code]:
haftmann@68028
   153
  "char_of_int = char_of_integer \<circ> integer_of_int"
haftmann@68028
   154
  including integer.lifting unfolding char_of_integer_def char_of_int_def
haftmann@68028
   155
  by transfer (simp add: fun_eq_iff)
haftmann@68028
   156
haftmann@68028
   157
lemma [code]:
haftmann@68028
   158
  "int_of_char = int_of_integer \<circ> integer_of_char"
haftmann@68028
   159
  including integer.lifting unfolding integer_of_char_def int_of_char_def
haftmann@68028
   160
  by transfer (simp add: fun_eq_iff)
haftmann@68028
   161
haftmann@52435
   162
code_identifier
haftmann@52435
   163
  code_module Code_Target_Int \<rightharpoonup>
haftmann@52435
   164
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@50023
   165
haftmann@50023
   166
end