src/HOL/Library/Code_Target_Int.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 60868 dd18c33c001e
child 61275 053ec04ea866
permissions -rw-r--r--
tuned references
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
haftmann@51143
     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"
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@50023
    82
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
haftmann@51114
    83
  by transfer (simp add: equal)
haftmann@50023
    84
haftmann@50023
    85
lemma [code]:
haftmann@50023
    86
  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
haftmann@51114
    87
  by transfer rule
haftmann@50023
    88
haftmann@50023
    89
lemma [code]:
haftmann@50023
    90
  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
haftmann@51114
    91
  by transfer rule
kuncar@55736
    92
end
haftmann@50023
    93
haftmann@54796
    94
lemma (in ring_1) of_int_code_if:
haftmann@50023
    95
  "of_int k = (if k = 0 then 0
haftmann@50023
    96
     else if k < 0 then - of_int (- k)
haftmann@50023
    97
     else let
haftmann@60868
    98
       l = 2 * of_int (k div 2);
haftmann@60868
    99
       j = k mod 2
haftmann@60868
   100
     in if j = 0 then l else l + 1)"
haftmann@50023
   101
proof -
haftmann@50023
   102
  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
haftmann@50023
   103
  show ?thesis
haftmann@60868
   104
    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
haftmann@50023
   105
qed
haftmann@50023
   106
haftmann@54796
   107
declare of_int_code_if [code]
haftmann@50023
   108
haftmann@50023
   109
lemma [code]:
haftmann@50023
   110
  "nat = nat_of_integer \<circ> of_int"
kuncar@55736
   111
  including integer.lifting by transfer (simp add: fun_eq_iff)
haftmann@50023
   112
haftmann@52435
   113
code_identifier
haftmann@52435
   114
  code_module Code_Target_Int \<rightharpoonup>
haftmann@52435
   115
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@50023
   116
haftmann@50023
   117
end