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)
1 (*  Title:      HOL/Library/Code_Target_Int.thy
2     Author:     Florian Haftmann, TU Muenchen
3 *)
5 header {* Implementation of integer numbers by target-language integers *}
7 theory Code_Target_Int
8 imports Main
9 begin
11 code_datatype int_of_integer
13 lemma [code, code del]:
14   "integer_of_int = integer_of_int" ..
16 lemma [code]:
17   "integer_of_int (int_of_integer k) = k"
18   by transfer rule
20 lemma [code]:
21   "Int.Pos = int_of_integer \<circ> integer_of_num"
22   by transfer (simp add: fun_eq_iff)
24 lemma [code]:
25   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
26   by transfer (simp add: fun_eq_iff)
28 lemma [code_abbrev]:
29   "int_of_integer (numeral k) = Int.Pos k"
30   by transfer simp
32 lemma [code_abbrev]:
33   "int_of_integer (neg_numeral k) = Int.Neg k"
34   by transfer simp
36 lemma [code, symmetric, code_post]:
37   "0 = int_of_integer 0"
38   by transfer simp
40 lemma [code, symmetric, code_post]:
41   "1 = int_of_integer 1"
42   by transfer simp
44 lemma [code]:
45   "k + l = int_of_integer (of_int k + of_int l)"
46   by transfer simp
48 lemma [code]:
49   "- k = int_of_integer (- of_int k)"
50   by transfer simp
52 lemma [code]:
53   "k - l = int_of_integer (of_int k - of_int l)"
54   by transfer simp
56 lemma [code]:
57   "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
58   by transfer simp
60 lemma [code, code del]:
61   "Int.sub = Int.sub" ..
63 lemma [code]:
64   "k * l = int_of_integer (of_int k * of_int l)"
65   by simp
67 lemma [code]:
68   "pdivmod k l = map_pair int_of_integer int_of_integer
69     (Code_Numeral.divmod_abs (of_int k) (of_int l))"
70   by (simp add: prod_eq_iff pdivmod_def)
72 lemma [code]:
73   "k div l = int_of_integer (of_int k div of_int l)"
74   by simp
76 lemma [code]:
77   "k mod l = int_of_integer (of_int k mod of_int l)"
78   by simp
80 lemma [code]:
81   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
82   by transfer (simp add: equal)
84 lemma [code]:
85   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
86   by transfer rule
88 lemma [code]:
89   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
90   by transfer rule
92 lemma (in ring_1) of_int_code:
93   "of_int k = (if k = 0 then 0
94      else if k < 0 then - of_int (- k)
95      else let
96        (l, j) = divmod_int k 2;
97        l' = 2 * of_int l
98      in if j = 0 then l' else l' + 1)"
99 proof -
100   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
101   show ?thesis
102     by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
103       of_int_add [symmetric]) (simp add: * mult_commute)
104 qed
106 declare of_int_code [code]
108 lemma [code]:
109   "nat = nat_of_integer \<circ> of_int"
110   by transfer (simp add: fun_eq_iff)
112 code_modulename SML
113   Code_Target_Int Arith
115 code_modulename OCaml
116   Code_Target_Int Arith