src/HOL/Library/Code_Target_Int.thy
 changeset 51114 3e913a575dc6 parent 51095 7ae79f2e3cc7 child 51143 0a2371e7ced3
```     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 12:24:56 2013 +0100
1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 12:24:56 2013 +0100
1.3 @@ -15,47 +15,47 @@
1.4
1.5  lemma [code]:
1.6    "integer_of_int (int_of_integer k) = k"
1.7 -  by (simp add: integer_eq_iff)
1.8 +  by transfer rule
1.9
1.10  lemma [code]:
1.11    "Int.Pos = int_of_integer \<circ> integer_of_num"
1.12 -  by (simp add: integer_of_num_def fun_eq_iff)
1.13 +  by transfer (simp add: fun_eq_iff)
1.14
1.15  lemma [code]:
1.16    "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
1.17 -  by (simp add: integer_of_num_def fun_eq_iff)
1.18 +  by transfer (simp add: fun_eq_iff)
1.19
1.20  lemma [code_abbrev]:
1.21    "int_of_integer (numeral k) = Int.Pos k"
1.22 -  by simp
1.23 +  by transfer simp
1.24
1.25  lemma [code_abbrev]:
1.26    "int_of_integer (neg_numeral k) = Int.Neg k"
1.27 -  by simp
1.28 +  by transfer simp
1.29
1.30  lemma [code, symmetric, code_post]:
1.31    "0 = int_of_integer 0"
1.32 -  by simp
1.33 +  by transfer simp
1.34
1.35  lemma [code, symmetric, code_post]:
1.36    "1 = int_of_integer 1"
1.37 -  by simp
1.38 +  by transfer simp
1.39
1.40  lemma [code]:
1.41    "k + l = int_of_integer (of_int k + of_int l)"
1.42 -  by simp
1.43 +  by transfer simp
1.44
1.45  lemma [code]:
1.46    "- k = int_of_integer (- of_int k)"
1.47 -  by simp
1.48 +  by transfer simp
1.49
1.50  lemma [code]:
1.51    "k - l = int_of_integer (of_int k - of_int l)"
1.52 -  by simp
1.53 +  by transfer simp
1.54
1.55  lemma [code]:
1.56    "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
1.57 -  by simp
1.58 +  by transfer simp
1.59
1.60  lemma [code, code del]:
1.61    "Int.sub = Int.sub" ..
1.62 @@ -79,15 +79,15 @@
1.63
1.64  lemma [code]:
1.65    "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
1.66 -  by (simp add: equal integer_eq_iff)
1.67 +  by transfer (simp add: equal)
1.68
1.69  lemma [code]:
1.70    "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
1.71 -  by (simp add: less_eq_int_def)
1.72 +  by transfer rule
1.73
1.74  lemma [code]:
1.75    "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
1.76 -  by (simp add: less_int_def)
1.77 +  by transfer rule
1.78
1.79  lemma (in ring_1) of_int_code:
1.80    "of_int k = (if k = 0 then 0
1.81 @@ -107,7 +107,7 @@
1.82
1.83  lemma [code]:
1.84    "nat = nat_of_integer \<circ> of_int"
1.85 -  by (simp add: fun_eq_iff nat_of_integer_def)
1.86 +  by transfer (simp add: fun_eq_iff)
1.87
1.88  code_modulename SML
1.89    Code_Target_Int Arith
```