src/HOL/Library/Code_Target_Int.thy
author haftmann
Fri Jul 04 20:18:47 2014 +0200 (2014-07-04)
changeset 57512 cc97b347b301
parent 55932 68c5104d2204
child 58099 7f232ae7de7c
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
haftmann@50023
     1
(*  Title:      HOL/Library/Code_Target_Int.thy
haftmann@50023
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@50023
     3
*)
haftmann@50023
     4
haftmann@50023
     5
header {* Implementation of integer numbers by target-language integers *}
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@50023
    47
lemma [code]:
haftmann@50023
    48
  "k + l = int_of_integer (of_int k + of_int l)"
haftmann@51114
    49
  by transfer simp
haftmann@50023
    50
haftmann@50023
    51
lemma [code]:
haftmann@50023
    52
  "- k = int_of_integer (- of_int k)"
haftmann@51114
    53
  by transfer simp
haftmann@50023
    54
haftmann@50023
    55
lemma [code]:
haftmann@50023
    56
  "k - l = int_of_integer (of_int k - of_int l)"
haftmann@51114
    57
  by transfer simp
haftmann@50023
    58
haftmann@50023
    59
lemma [code]:
haftmann@51143
    60
  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
haftmann@51114
    61
  by transfer simp
haftmann@50023
    62
haftmann@54891
    63
declare [[code drop: Int.sub]]
haftmann@50023
    64
haftmann@50023
    65
lemma [code]:
haftmann@50023
    66
  "k * l = int_of_integer (of_int k * of_int l)"
haftmann@50023
    67
  by simp
haftmann@50023
    68
haftmann@50023
    69
lemma [code]:
blanchet@55932
    70
  "Divides.divmod_abs k l = map_prod int_of_integer int_of_integer
haftmann@51143
    71
    (Code_Numeral.divmod_abs (of_int k) (of_int l))"
haftmann@53069
    72
  by (simp add: prod_eq_iff)
haftmann@50023
    73
haftmann@50023
    74
lemma [code]:
haftmann@50023
    75
  "k div l = int_of_integer (of_int k div of_int l)"
haftmann@50023
    76
  by simp
haftmann@50023
    77
haftmann@50023
    78
lemma [code]:
haftmann@50023
    79
  "k mod l = int_of_integer (of_int k mod of_int l)"
haftmann@50023
    80
  by simp
haftmann@50023
    81
haftmann@50023
    82
lemma [code]:
haftmann@50023
    83
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
haftmann@51114
    84
  by transfer (simp add: equal)
haftmann@50023
    85
haftmann@50023
    86
lemma [code]:
haftmann@50023
    87
  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
haftmann@51114
    88
  by transfer rule
haftmann@50023
    89
haftmann@50023
    90
lemma [code]:
haftmann@50023
    91
  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
haftmann@51114
    92
  by transfer rule
kuncar@55736
    93
end
haftmann@50023
    94
haftmann@54796
    95
lemma (in ring_1) of_int_code_if:
haftmann@50023
    96
  "of_int k = (if k = 0 then 0
haftmann@50023
    97
     else if k < 0 then - of_int (- k)
haftmann@50023
    98
     else let
haftmann@50023
    99
       (l, j) = divmod_int k 2;
haftmann@50023
   100
       l' = 2 * of_int l
haftmann@50023
   101
     in if j = 0 then l' else l' + 1)"
haftmann@50023
   102
proof -
haftmann@50023
   103
  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
haftmann@50023
   104
  show ?thesis
haftmann@54796
   105
    by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
haftmann@57512
   106
      (simp add: * mult.commute)
haftmann@50023
   107
qed
haftmann@50023
   108
haftmann@54796
   109
declare of_int_code_if [code]
haftmann@50023
   110
haftmann@50023
   111
lemma [code]:
haftmann@50023
   112
  "nat = nat_of_integer \<circ> of_int"
kuncar@55736
   113
  including integer.lifting by transfer (simp add: fun_eq_iff)
haftmann@50023
   114
haftmann@52435
   115
code_identifier
haftmann@52435
   116
  code_module Code_Target_Int \<rightharpoonup>
haftmann@52435
   117
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@50023
   118
haftmann@50023
   119
end
haftmann@50023
   120