equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 code_datatype int_of_integer |
11 code_datatype int_of_integer |
12 |
12 |
13 declare [[code drop: integer_of_int]] |
13 declare [[code drop: integer_of_int]] |
|
14 |
|
15 context |
|
16 includes integer.lifting |
|
17 begin |
14 |
18 |
15 lemma [code]: |
19 lemma [code]: |
16 "integer_of_int (int_of_integer k) = k" |
20 "integer_of_int (int_of_integer k) = k" |
17 by transfer rule |
21 by transfer rule |
18 |
22 |
84 by transfer rule |
88 by transfer rule |
85 |
89 |
86 lemma [code]: |
90 lemma [code]: |
87 "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l" |
91 "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l" |
88 by transfer rule |
92 by transfer rule |
|
93 end |
89 |
94 |
90 lemma (in ring_1) of_int_code_if: |
95 lemma (in ring_1) of_int_code_if: |
91 "of_int k = (if k = 0 then 0 |
96 "of_int k = (if k = 0 then 0 |
92 else if k < 0 then - of_int (- k) |
97 else if k < 0 then - of_int (- k) |
93 else let |
98 else let |
103 |
108 |
104 declare of_int_code_if [code] |
109 declare of_int_code_if [code] |
105 |
110 |
106 lemma [code]: |
111 lemma [code]: |
107 "nat = nat_of_integer \<circ> of_int" |
112 "nat = nat_of_integer \<circ> of_int" |
108 by transfer (simp add: fun_eq_iff) |
113 including integer.lifting by transfer (simp add: fun_eq_iff) |
109 |
114 |
110 code_identifier |
115 code_identifier |
111 code_module Code_Target_Int \<rightharpoonup> |
116 code_module Code_Target_Int \<rightharpoonup> |
112 (SML) Arith and (OCaml) Arith and (Haskell) Arith |
117 (SML) Arith and (OCaml) Arith and (Haskell) Arith |
113 |
118 |