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