src/HOL/Library/Code_Target_Int.thy
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 51143 0a2371e7ced3
child 52435 6646bb548c6b
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
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@50023
    13
lemma [code, code del]:
haftmann@50023
    14
  "integer_of_int = integer_of_int" ..
haftmann@50023
    15
haftmann@50023
    16
lemma [code]:
haftmann@50023
    17
  "integer_of_int (int_of_integer k) = k"
haftmann@51114
    18
  by transfer rule
haftmann@50023
    19
haftmann@50023
    20
lemma [code]:
haftmann@50023
    21
  "Int.Pos = int_of_integer \<circ> integer_of_num"
haftmann@51114
    22
  by transfer (simp add: fun_eq_iff) 
haftmann@50023
    23
haftmann@50023
    24
lemma [code]:
haftmann@50023
    25
  "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
haftmann@51114
    26
  by transfer (simp add: fun_eq_iff) 
haftmann@50023
    27
haftmann@50023
    28
lemma [code_abbrev]:
haftmann@51095
    29
  "int_of_integer (numeral k) = Int.Pos k"
haftmann@51114
    30
  by transfer simp
haftmann@50023
    31
haftmann@50023
    32
lemma [code_abbrev]:
haftmann@51095
    33
  "int_of_integer (neg_numeral k) = Int.Neg k"
haftmann@51114
    34
  by transfer simp
haftmann@51095
    35
  
haftmann@51095
    36
lemma [code, symmetric, code_post]:
haftmann@50023
    37
  "0 = int_of_integer 0"
haftmann@51114
    38
  by transfer simp
haftmann@50023
    39
haftmann@51095
    40
lemma [code, symmetric, code_post]:
haftmann@50023
    41
  "1 = int_of_integer 1"
haftmann@51114
    42
  by transfer simp
haftmann@50023
    43
haftmann@50023
    44
lemma [code]:
haftmann@50023
    45
  "k + l = int_of_integer (of_int k + of_int l)"
haftmann@51114
    46
  by transfer simp
haftmann@50023
    47
haftmann@50023
    48
lemma [code]:
haftmann@50023
    49
  "- k = int_of_integer (- of_int k)"
haftmann@51114
    50
  by transfer simp
haftmann@50023
    51
haftmann@50023
    52
lemma [code]:
haftmann@50023
    53
  "k - l = int_of_integer (of_int k - of_int l)"
haftmann@51114
    54
  by transfer simp
haftmann@50023
    55
haftmann@50023
    56
lemma [code]:
haftmann@51143
    57
  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
haftmann@51114
    58
  by transfer simp
haftmann@50023
    59
haftmann@50023
    60
lemma [code, code del]:
haftmann@50023
    61
  "Int.sub = Int.sub" ..
haftmann@50023
    62
haftmann@50023
    63
lemma [code]:
haftmann@50023
    64
  "k * l = int_of_integer (of_int k * of_int l)"
haftmann@50023
    65
  by simp
haftmann@50023
    66
haftmann@50023
    67
lemma [code]:
haftmann@50023
    68
  "pdivmod k l = map_pair int_of_integer int_of_integer
haftmann@51143
    69
    (Code_Numeral.divmod_abs (of_int k) (of_int l))"
haftmann@50023
    70
  by (simp add: prod_eq_iff pdivmod_def)
haftmann@50023
    71
haftmann@50023
    72
lemma [code]:
haftmann@50023
    73
  "k div l = int_of_integer (of_int k div of_int l)"
haftmann@50023
    74
  by simp
haftmann@50023
    75
haftmann@50023
    76
lemma [code]:
haftmann@50023
    77
  "k mod l = int_of_integer (of_int k mod of_int l)"
haftmann@50023
    78
  by simp
haftmann@50023
    79
haftmann@50023
    80
lemma [code]:
haftmann@50023
    81
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
haftmann@51114
    82
  by transfer (simp add: equal)
haftmann@50023
    83
haftmann@50023
    84
lemma [code]:
haftmann@50023
    85
  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
haftmann@51114
    86
  by transfer rule
haftmann@50023
    87
haftmann@50023
    88
lemma [code]:
haftmann@50023
    89
  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
haftmann@51114
    90
  by transfer rule
haftmann@50023
    91
haftmann@50023
    92
lemma (in ring_1) of_int_code:
haftmann@50023
    93
  "of_int k = (if k = 0 then 0
haftmann@50023
    94
     else if k < 0 then - of_int (- k)
haftmann@50023
    95
     else let
haftmann@50023
    96
       (l, j) = divmod_int k 2;
haftmann@50023
    97
       l' = 2 * of_int l
haftmann@50023
    98
     in if j = 0 then l' else l' + 1)"
haftmann@50023
    99
proof -
haftmann@50023
   100
  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
haftmann@50023
   101
  show ?thesis
haftmann@50023
   102
    by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
haftmann@50023
   103
      of_int_add [symmetric]) (simp add: * mult_commute)
haftmann@50023
   104
qed
haftmann@50023
   105
haftmann@50023
   106
declare of_int_code [code]
haftmann@50023
   107
haftmann@50023
   108
lemma [code]:
haftmann@50023
   109
  "nat = nat_of_integer \<circ> of_int"
haftmann@51114
   110
  by transfer (simp add: fun_eq_iff)
haftmann@50023
   111
haftmann@50023
   112
code_modulename SML
haftmann@50023
   113
  Code_Target_Int Arith
haftmann@50023
   114
haftmann@50023
   115
code_modulename OCaml
haftmann@50023
   116
  Code_Target_Int Arith
haftmann@50023
   117
haftmann@50023
   118
code_modulename Haskell
haftmann@50023
   119
  Code_Target_Int Arith
haftmann@50023
   120
haftmann@50023
   121
end
haftmann@50023
   122