type lifting setup for code numeral types
authorhaftmann
Thu Feb 14 12:24:56 2013 +0100 (2013-02-14)
changeset 511143e913a575dc6
parent 51113 222fb6cb2c3e
child 51115 7dbd6832a689
child 51116 0dac0158b8d4
type lifting setup for code numeral types
src/HOL/Library/Code_Numeral_Types.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Numeral_Types.thy	Thu Feb 14 12:24:56 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Numeral_Types.thy	Thu Feb 14 12:24:56 2013 +0100
     1.3 @@ -13,9 +13,11 @@
     1.4  typedef integer = "UNIV \<Colon> int set"
     1.5    morphisms int_of_integer integer_of_int ..
     1.6  
     1.7 +setup_lifting (no_code) type_definition_integer
     1.8 +
     1.9  lemma integer_eq_iff:
    1.10    "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
    1.11 -  using int_of_integer_inject [of k l] ..
    1.12 +  by transfer rule
    1.13  
    1.14  lemma integer_eqI:
    1.15    "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
    1.16 @@ -23,172 +25,199 @@
    1.17  
    1.18  lemma int_of_integer_integer_of_int [simp]:
    1.19    "int_of_integer (integer_of_int k) = k"
    1.20 -  using integer_of_int_inverse [of k] by simp
    1.21 +  by transfer rule
    1.22  
    1.23  lemma integer_of_int_int_of_integer [simp]:
    1.24    "integer_of_int (int_of_integer k) = k"
    1.25 -  using int_of_integer_inverse [of k] by simp
    1.26 +  by transfer rule
    1.27  
    1.28  instantiation integer :: ring_1
    1.29  begin
    1.30  
    1.31 -definition
    1.32 -  "0 = integer_of_int 0"
    1.33 +lift_definition zero_integer :: integer
    1.34 +  is "0 :: int"
    1.35 +  .
    1.36  
    1.37 -lemma int_of_integer_zero [simp]:
    1.38 -  "int_of_integer 0 = 0"
    1.39 -  by (simp add: zero_integer_def)
    1.40 -
    1.41 -definition
    1.42 -  "1 = integer_of_int 1"
    1.43 +declare zero_integer.rep_eq [simp]
    1.44  
    1.45 -lemma int_of_integer_one [simp]:
    1.46 -  "int_of_integer 1 = 1"
    1.47 -  by (simp add: one_integer_def)
    1.48 +lift_definition one_integer :: integer
    1.49 +  is "1 :: int"
    1.50 +  .
    1.51 +
    1.52 +declare one_integer.rep_eq [simp]
    1.53  
    1.54 -definition
    1.55 -  "k + l = integer_of_int (int_of_integer k + int_of_integer l)"
    1.56 +lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.57 +  is "plus :: int \<Rightarrow> int \<Rightarrow> int"
    1.58 +  .
    1.59  
    1.60 -lemma int_of_integer_plus [simp]:
    1.61 -  "int_of_integer (k + l) = int_of_integer k + int_of_integer l"
    1.62 -  by (simp add: plus_integer_def)
    1.63 +declare plus_integer.rep_eq [simp]
    1.64  
    1.65 -definition
    1.66 -  "- k = integer_of_int (- int_of_integer k)"
    1.67 +lift_definition uminus_integer :: "integer \<Rightarrow> integer"
    1.68 +  is "uminus :: int \<Rightarrow> int"
    1.69 +  .
    1.70  
    1.71 -lemma int_of_integer_uminus [simp]:
    1.72 -  "int_of_integer (- k) = - int_of_integer k"
    1.73 -  by (simp add: uminus_integer_def)
    1.74 -
    1.75 -definition
    1.76 -  "k - l = integer_of_int (int_of_integer k - int_of_integer l)"
    1.77 +declare uminus_integer.rep_eq [simp]
    1.78  
    1.79 -lemma int_of_integer_minus [simp]:
    1.80 -  "int_of_integer (k - l) = int_of_integer k - int_of_integer l"
    1.81 -  by (simp add: minus_integer_def)
    1.82 +lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.83 +  is "minus :: int \<Rightarrow> int \<Rightarrow> int"
    1.84 +  .
    1.85 +
    1.86 +declare minus_integer.rep_eq [simp]
    1.87  
    1.88 -definition
    1.89 -  "k * l = integer_of_int (int_of_integer k * int_of_integer l)"
    1.90 +lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.91 +  is "times :: int \<Rightarrow> int \<Rightarrow> int"
    1.92 +  .
    1.93  
    1.94 -lemma int_of_integer_times [simp]:
    1.95 -  "int_of_integer (k * l) = int_of_integer k * int_of_integer l"
    1.96 -  by (simp add: times_integer_def)
    1.97 +declare times_integer.rep_eq [simp]
    1.98  
    1.99  instance proof
   1.100 -qed (auto simp add: integer_eq_iff algebra_simps)
   1.101 +qed (transfer, simp add: algebra_simps)+
   1.102  
   1.103  end
   1.104  
   1.105 +lemma [transfer_rule]:
   1.106 +  "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
   1.107 +  by (unfold of_nat_def [abs_def])  transfer_prover
   1.108 +
   1.109 +lemma [transfer_rule]:
   1.110 +  "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
   1.111 +proof -
   1.112 +  have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
   1.113 +    by (unfold of_int_of_nat [abs_def]) transfer_prover
   1.114 +  then show ?thesis by (simp add: id_def)
   1.115 +qed
   1.116 +
   1.117 +lemma [transfer_rule]:
   1.118 +  "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
   1.119 +proof -
   1.120 +  have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
   1.121 +    by transfer_prover
   1.122 +  then show ?thesis by simp
   1.123 +qed
   1.124 +
   1.125 +lemma [transfer_rule]:
   1.126 +  "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
   1.127 +  by (unfold neg_numeral_def [abs_def]) transfer_prover
   1.128 +
   1.129 +lemma [transfer_rule]:
   1.130 +  "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   1.131 +  by (unfold Num.sub_def [abs_def]) transfer_prover
   1.132 +
   1.133  lemma int_of_integer_of_nat [simp]:
   1.134    "int_of_integer (of_nat n) = of_nat n"
   1.135 -  by (induct n) simp_all
   1.136 +  by transfer rule
   1.137  
   1.138 -definition integer_of_nat :: "nat \<Rightarrow> integer"
   1.139 -where
   1.140 -  "integer_of_nat = of_nat"
   1.141 +lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
   1.142 +  is "of_nat :: nat \<Rightarrow> int"
   1.143 +  .
   1.144  
   1.145  lemma int_of_integer_integer_of_nat [simp]:
   1.146    "int_of_integer (integer_of_nat n) = of_nat n"
   1.147 -  by (simp add: integer_of_nat_def)
   1.148 -  
   1.149 -definition nat_of_integer :: "integer \<Rightarrow> nat"
   1.150 -where
   1.151 -  "nat_of_integer k = Int.nat (int_of_integer k)"
   1.152 +  by transfer rule
   1.153 +
   1.154 +lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
   1.155 +  is Int.nat
   1.156 +  .
   1.157  
   1.158  lemma nat_of_integer_of_nat [simp]:
   1.159    "nat_of_integer (of_nat n) = n"
   1.160 -  by (simp add: nat_of_integer_def)
   1.161 +  by transfer simp
   1.162  
   1.163  lemma int_of_integer_of_int [simp]:
   1.164    "int_of_integer (of_int k) = k"
   1.165 -  by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
   1.166 +  by transfer simp
   1.167  
   1.168  lemma nat_of_integer_integer_of_nat [simp]:
   1.169    "nat_of_integer (integer_of_nat n) = n"
   1.170 -  by (simp add: integer_of_nat_def)
   1.171 +  by transfer simp
   1.172  
   1.173  lemma integer_of_int_eq_of_int [simp, code_abbrev]:
   1.174    "integer_of_int = of_int"
   1.175 -  by rule (simp add: integer_eq_iff)
   1.176 +  by transfer (simp add: fun_eq_iff)
   1.177  
   1.178  lemma of_int_integer_of [simp]:
   1.179    "of_int (int_of_integer k) = (k :: integer)"
   1.180 -  by (simp add: integer_eq_iff)
   1.181 +  by transfer rule
   1.182  
   1.183  lemma int_of_integer_numeral [simp]:
   1.184    "int_of_integer (numeral k) = numeral k"
   1.185 -  using int_of_integer_of_int [of "numeral k"] by simp
   1.186 +  by transfer rule
   1.187  
   1.188  lemma int_of_integer_neg_numeral [simp]:
   1.189    "int_of_integer (neg_numeral k) = neg_numeral k"
   1.190 -  by (simp only: neg_numeral_def int_of_integer_uminus) simp
   1.191 +  by transfer rule
   1.192  
   1.193  lemma int_of_integer_sub [simp]:
   1.194    "int_of_integer (Num.sub k l) = Num.sub k l"
   1.195 -  by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral)
   1.196 +  by transfer rule
   1.197  
   1.198  instantiation integer :: "{ring_div, equal, linordered_idom}"
   1.199  begin
   1.200  
   1.201 -definition
   1.202 -  "k div l = of_int (int_of_integer k div int_of_integer l)"
   1.203 +lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   1.204 +  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
   1.205 +  .
   1.206  
   1.207 -lemma int_of_integer_div [simp]:
   1.208 -  "int_of_integer (k div l) = int_of_integer k div int_of_integer l"
   1.209 -  by (simp add: div_integer_def)
   1.210 +declare div_integer.rep_eq [simp]
   1.211  
   1.212 -definition
   1.213 -  "k mod l = of_int (int_of_integer k mod int_of_integer l)"
   1.214 +lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   1.215 +  is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
   1.216 +  .
   1.217 +
   1.218 +declare mod_integer.rep_eq [simp]
   1.219  
   1.220 -lemma int_of_integer_mod [simp]:
   1.221 -  "int_of_integer (k mod l) = int_of_integer k mod int_of_integer l"
   1.222 -  by (simp add: mod_integer_def)
   1.223 +lift_definition abs_integer :: "integer \<Rightarrow> integer"
   1.224 +  is "abs :: int \<Rightarrow> int"
   1.225 +  .
   1.226  
   1.227 -definition
   1.228 -  "\<bar>k\<bar> = of_int \<bar>int_of_integer k\<bar>"
   1.229 +declare abs_integer.rep_eq [simp]
   1.230  
   1.231 -lemma int_of_integer_abs [simp]:
   1.232 -  "int_of_integer \<bar>k\<bar> = \<bar>int_of_integer k\<bar>"
   1.233 -  by (simp add: abs_integer_def)
   1.234 +lift_definition sgn_integer :: "integer \<Rightarrow> integer"
   1.235 +  is "sgn :: int \<Rightarrow> int"
   1.236 +  .
   1.237  
   1.238 -definition
   1.239 -  "sgn k = of_int (sgn (int_of_integer k))"
   1.240 +declare sgn_integer.rep_eq [simp]
   1.241  
   1.242 -lemma int_of_integer_sgn [simp]:
   1.243 -  "int_of_integer (sgn k) = sgn (int_of_integer k)"
   1.244 -  by (simp add: sgn_integer_def)
   1.245 +lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   1.246 +  is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
   1.247 +  .
   1.248  
   1.249 -definition
   1.250 -  "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
   1.251 +lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   1.252 +  is "less :: int \<Rightarrow> int \<Rightarrow> bool"
   1.253 +  .
   1.254  
   1.255 -definition
   1.256 -  "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
   1.257 -
   1.258 -definition
   1.259 -  "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of_integer k) (int_of_integer l)"
   1.260 +lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   1.261 +  is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
   1.262 +  .
   1.263  
   1.264  instance proof
   1.265 -qed (auto simp add: integer_eq_iff algebra_simps
   1.266 -  less_eq_integer_def less_integer_def equal_integer_def equal
   1.267 -  intro: mult_strict_right_mono)
   1.268 +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
   1.269  
   1.270  end
   1.271  
   1.272 +lemma [transfer_rule]:
   1.273 +  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   1.274 +  by (unfold min_def [abs_def]) transfer_prover
   1.275 +
   1.276 +lemma [transfer_rule]:
   1.277 +  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   1.278 +  by (unfold max_def [abs_def]) transfer_prover
   1.279 +
   1.280  lemma int_of_integer_min [simp]:
   1.281    "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
   1.282 -  by (simp add: min_def less_eq_integer_def)
   1.283 +  by transfer rule
   1.284  
   1.285  lemma int_of_integer_max [simp]:
   1.286    "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
   1.287 -  by (simp add: max_def less_eq_integer_def)
   1.288 +  by transfer rule
   1.289  
   1.290  lemma nat_of_integer_non_positive [simp]:
   1.291    "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
   1.292 -  by (simp add: nat_of_integer_def less_eq_integer_def)
   1.293 +  by transfer simp
   1.294  
   1.295  lemma of_nat_of_integer [simp]:
   1.296    "of_nat (nat_of_integer k) = max 0 k"
   1.297 -  by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def)
   1.298 +  by transfer auto
   1.299  
   1.300  
   1.301  subsection {* Code theorems for target language integers *}
   1.302 @@ -199,29 +228,36 @@
   1.303  where
   1.304    [simp, code_abbrev]: "Pos = numeral"
   1.305  
   1.306 +lemma [transfer_rule]:
   1.307 +  "fun_rel HOL.eq cr_integer numeral Pos"
   1.308 +  by simp transfer_prover
   1.309 +
   1.310  definition Neg :: "num \<Rightarrow> integer"
   1.311  where
   1.312    [simp, code_abbrev]: "Neg = neg_numeral"
   1.313  
   1.314 +lemma [transfer_rule]:
   1.315 +  "fun_rel HOL.eq cr_integer neg_numeral Neg"
   1.316 +  by simp transfer_prover
   1.317 +
   1.318  code_datatype "0::integer" Pos Neg
   1.319  
   1.320  
   1.321  text {* Auxiliary operations *}
   1.322  
   1.323 -definition dup :: "integer \<Rightarrow> integer"
   1.324 -where
   1.325 -  [simp]: "dup k = k + k"
   1.326 +lift_definition dup :: "integer \<Rightarrow> integer"
   1.327 +  is "\<lambda>k::int. k + k"
   1.328 +  .
   1.329  
   1.330  lemma dup_code [code]:
   1.331    "dup 0 = 0"
   1.332    "dup (Pos n) = Pos (Num.Bit0 n)"
   1.333    "dup (Neg n) = Neg (Num.Bit0 n)"
   1.334 -  unfolding Pos_def Neg_def neg_numeral_def
   1.335 -  by (simp_all add: numeral_Bit0)
   1.336 +  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
   1.337  
   1.338 -definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
   1.339 -where
   1.340 -  [simp]: "sub m n = numeral m - numeral n"
   1.341 +lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
   1.342 +  is "\<lambda>m n. numeral m - numeral n :: int"
   1.343 +  .
   1.344  
   1.345  lemma sub_code [code]:
   1.346    "sub Num.One Num.One = 0"
   1.347 @@ -233,9 +269,7 @@
   1.348    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   1.349    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   1.350    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   1.351 -  unfolding sub_def dup_def numeral.simps Pos_def Neg_def
   1.352 -    neg_numeral_def numeral_BitM
   1.353 -  by (simp_all only: algebra_simps add.comm_neutral)
   1.354 +  by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
   1.355  
   1.356  
   1.357  text {* Implementations *}
   1.358 @@ -251,7 +285,7 @@
   1.359    "Pos m + Neg n = sub m n"
   1.360    "Neg m + Pos n = sub n m"
   1.361    "Neg m + Neg n = Neg (m + n)"
   1.362 -  by simp_all
   1.363 +  by (transfer, simp)+
   1.364  
   1.365  lemma uminus_integer_code [code]:
   1.366    "uminus 0 = (0::integer)"
   1.367 @@ -266,7 +300,7 @@
   1.368    "Pos m - Neg n = Pos (m + n)"
   1.369    "Neg m - Pos n = Neg (m + n)"
   1.370    "Neg m - Neg n = sub n m"
   1.371 -  by simp_all
   1.372 +  by (transfer, simp)+
   1.373  
   1.374  lemma abs_integer_code [code]:
   1.375    "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
   1.376 @@ -322,15 +356,18 @@
   1.377      (let j = sub k l in
   1.378         if j < 0 then (0, Pos k)
   1.379         else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
   1.380 -  by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta
   1.381 -    sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
   1.382 +  apply (simp add: prod_eq_iff Let_def prod_case_beta)
   1.383 +  apply transfer
   1.384 +  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
   1.385 +  done
   1.386  
   1.387 -lemma divmod_integer_code [code]: "divmod_integer k l =
   1.388 -  (if k = 0 then (0, 0) else if l = 0 then (0, k) else
   1.389 -  (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
   1.390 -    then divmod_abs k l
   1.391 -    else (let (r, s) = divmod_abs k l in
   1.392 -      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.393 +lemma divmod_integer_code [code]:
   1.394 +  "divmod_integer k l =
   1.395 +    (if k = 0 then (0, 0) else if l = 0 then (0, k) else
   1.396 +    (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
   1.397 +      then divmod_abs k l
   1.398 +      else (let (r, s) = divmod_abs k l in
   1.399 +        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.400  proof -
   1.401    have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
   1.402      by (auto simp add: sgn_if)
   1.403 @@ -358,7 +395,7 @@
   1.404    "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
   1.405    "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
   1.406    "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
   1.407 -  by (simp_all add: equal integer_eq_iff)
   1.408 +  by (simp_all add: equal)
   1.409  
   1.410  lemma equal_integer_refl [code nbe]:
   1.411    "HOL.equal (k::integer) k \<longleftrightarrow> True"
   1.412 @@ -374,7 +411,7 @@
   1.413    "Neg k \<le> 0 \<longleftrightarrow> True"
   1.414    "Neg k \<le> Pos l \<longleftrightarrow> True"
   1.415    "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
   1.416 -  by (simp_all add: less_eq_integer_def)
   1.417 +  by simp_all
   1.418  
   1.419  lemma less_integer_code [code]:
   1.420    "0 < (0::integer) \<longleftrightarrow> False"
   1.421 @@ -386,21 +423,21 @@
   1.422    "Neg k < 0 \<longleftrightarrow> True"
   1.423    "Neg k < Pos l \<longleftrightarrow> True"
   1.424    "Neg k < Neg l \<longleftrightarrow> l < k"
   1.425 -  by (simp_all add: less_integer_def)
   1.426 +  by simp_all
   1.427  
   1.428 -definition integer_of_num :: "num \<Rightarrow> integer"
   1.429 -where
   1.430 -  "integer_of_num = numeral"
   1.431 +lift_definition integer_of_num :: "num \<Rightarrow> integer"
   1.432 +  is "numeral :: num \<Rightarrow> int"
   1.433 +  .
   1.434  
   1.435  lemma integer_of_num [code]:
   1.436    "integer_of_num num.One = 1"
   1.437    "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
   1.438    "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
   1.439 -  by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps)
   1.440 +  by (transfer, simp only: numeral.simps Let_def)+
   1.441  
   1.442 -definition num_of_integer :: "integer \<Rightarrow> num"
   1.443 -where
   1.444 -  "num_of_integer = num_of_nat \<circ> nat_of_integer"
   1.445 +lift_definition num_of_integer :: "integer \<Rightarrow> num"
   1.446 +  is "num_of_nat \<circ> nat"
   1.447 +  .
   1.448  
   1.449  lemma num_of_integer_code [code]:
   1.450    "num_of_integer k = (if k \<le> 1 then Num.One
   1.451 @@ -587,9 +624,11 @@
   1.452  typedef natural = "UNIV \<Colon> nat set"
   1.453    morphisms nat_of_natural natural_of_nat ..
   1.454  
   1.455 +setup_lifting (no_code) type_definition_natural
   1.456 +
   1.457  lemma natural_eq_iff [termination_simp]:
   1.458    "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
   1.459 -  using nat_of_natural_inject [of m n] ..
   1.460 +  by transfer rule
   1.461  
   1.462  lemma natural_eqI:
   1.463    "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
   1.464 @@ -597,168 +636,179 @@
   1.465  
   1.466  lemma nat_of_natural_of_nat_inverse [simp]:
   1.467    "nat_of_natural (natural_of_nat n) = n"
   1.468 -  using natural_of_nat_inverse [of n] by simp
   1.469 +  by transfer rule
   1.470  
   1.471  lemma natural_of_nat_of_natural_inverse [simp]:
   1.472    "natural_of_nat (nat_of_natural n) = n"
   1.473 -  using nat_of_natural_inverse [of n] by simp
   1.474 +  by transfer rule
   1.475  
   1.476  instantiation natural :: "{comm_monoid_diff, semiring_1}"
   1.477  begin
   1.478  
   1.479 -definition
   1.480 -  "0 = natural_of_nat 0"
   1.481 +lift_definition zero_natural :: natural
   1.482 +  is "0 :: nat"
   1.483 +  .
   1.484  
   1.485 -lemma nat_of_natural_zero [simp]:
   1.486 -  "nat_of_natural 0 = 0"
   1.487 -  by (simp add: zero_natural_def)
   1.488 +declare zero_natural.rep_eq [simp]
   1.489  
   1.490 -definition
   1.491 -  "1 = natural_of_nat 1"
   1.492 +lift_definition one_natural :: natural
   1.493 +  is "1 :: nat"
   1.494 +  .
   1.495  
   1.496 -lemma nat_of_natural_one [simp]:
   1.497 -  "nat_of_natural 1 = 1"
   1.498 -  by (simp add: one_natural_def)
   1.499 -
   1.500 -definition
   1.501 -  "m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)"
   1.502 +declare one_natural.rep_eq [simp]
   1.503  
   1.504 -lemma nat_of_natural_plus [simp]:
   1.505 -  "nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n"
   1.506 -  by (simp add: plus_natural_def)
   1.507 +lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.508 +  is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.509 +  .
   1.510  
   1.511 -definition
   1.512 -  "m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)"
   1.513 +declare plus_natural.rep_eq [simp]
   1.514  
   1.515 -lemma nat_of_natural_minus [simp]:
   1.516 -  "nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n"
   1.517 -  by (simp add: minus_natural_def)
   1.518 +lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.519 +  is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.520 +  .
   1.521 +
   1.522 +declare minus_natural.rep_eq [simp]
   1.523  
   1.524 -definition
   1.525 -  "m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)"
   1.526 +lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.527 +  is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.528 +  .
   1.529  
   1.530 -lemma nat_of_natural_times [simp]:
   1.531 -  "nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n"
   1.532 -  by (simp add: times_natural_def)
   1.533 +declare times_natural.rep_eq [simp]
   1.534  
   1.535  instance proof
   1.536 -qed (auto simp add: natural_eq_iff algebra_simps)
   1.537 +qed (transfer, simp add: algebra_simps)+
   1.538  
   1.539  end
   1.540  
   1.541 +lemma [transfer_rule]:
   1.542 +  "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
   1.543 +proof -
   1.544 +  have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
   1.545 +    by (unfold of_nat_def [abs_def]) transfer_prover
   1.546 +  then show ?thesis by (simp add: id_def)
   1.547 +qed
   1.548 +
   1.549 +lemma [transfer_rule]:
   1.550 +  "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
   1.551 +proof -
   1.552 +  have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
   1.553 +    by transfer_prover
   1.554 +  then show ?thesis by simp
   1.555 +qed
   1.556 +
   1.557  lemma nat_of_natural_of_nat [simp]:
   1.558    "nat_of_natural (of_nat n) = n"
   1.559 -  by (induct n) simp_all
   1.560 +  by transfer rule
   1.561  
   1.562  lemma natural_of_nat_of_nat [simp, code_abbrev]:
   1.563    "natural_of_nat = of_nat"
   1.564 -  by rule (simp add: natural_eq_iff)
   1.565 +  by transfer rule
   1.566  
   1.567  lemma of_nat_of_natural [simp]:
   1.568    "of_nat (nat_of_natural n) = n"
   1.569 -  using natural_of_nat_of_natural_inverse [of n] by simp
   1.570 +  by transfer rule
   1.571  
   1.572  lemma nat_of_natural_numeral [simp]:
   1.573    "nat_of_natural (numeral k) = numeral k"
   1.574 -  using nat_of_natural_of_nat [of "numeral k"] by simp
   1.575 +  by transfer rule
   1.576  
   1.577  instantiation natural :: "{semiring_div, equal, linordered_semiring}"
   1.578  begin
   1.579  
   1.580 -definition
   1.581 -  "m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)"
   1.582 +lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.583 +  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.584 +  .
   1.585 +
   1.586 +declare div_natural.rep_eq [simp]
   1.587  
   1.588 -lemma nat_of_natural_div [simp]:
   1.589 -  "nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n"
   1.590 -  by (simp add: div_natural_def)
   1.591 +lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.592 +  is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.593 +  .
   1.594  
   1.595 -definition
   1.596 -  "m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)"
   1.597 +declare mod_natural.rep_eq [simp]
   1.598  
   1.599 -lemma nat_of_natural_mod [simp]:
   1.600 -  "nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n"
   1.601 -  by (simp add: mod_natural_def)
   1.602 +lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.603 +  is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.604 +  .
   1.605 +
   1.606 +declare less_eq_natural.rep_eq [termination_simp]
   1.607  
   1.608 -definition
   1.609 -  [termination_simp]: "m \<le> n \<longleftrightarrow> nat_of_natural m \<le> nat_of_natural n"
   1.610 +lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.611 +  is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.612 +  .
   1.613  
   1.614 -definition
   1.615 -  [termination_simp]: "m < n \<longleftrightarrow> nat_of_natural m < nat_of_natural n"
   1.616 +declare less_natural.rep_eq [termination_simp]
   1.617  
   1.618 -definition
   1.619 -  "HOL.equal m n \<longleftrightarrow> HOL.equal (nat_of_natural m) (nat_of_natural n)"
   1.620 +lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.621 +  is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.622 +  .
   1.623  
   1.624  instance proof
   1.625 -qed (auto simp add: natural_eq_iff algebra_simps
   1.626 -  less_eq_natural_def less_natural_def equal_natural_def equal)
   1.627 +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
   1.628  
   1.629  end
   1.630  
   1.631 +lemma [transfer_rule]:
   1.632 +  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   1.633 +  by (unfold min_def [abs_def]) transfer_prover
   1.634 +
   1.635 +lemma [transfer_rule]:
   1.636 +  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   1.637 +  by (unfold max_def [abs_def]) transfer_prover
   1.638 +
   1.639  lemma nat_of_natural_min [simp]:
   1.640    "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
   1.641 -  by (simp add: min_def less_eq_natural_def)
   1.642 +  by transfer rule
   1.643  
   1.644  lemma nat_of_natural_max [simp]:
   1.645    "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
   1.646 -  by (simp add: max_def less_eq_natural_def)
   1.647 +  by transfer rule
   1.648  
   1.649 -definition natural_of_integer :: "integer \<Rightarrow> natural"
   1.650 -where
   1.651 -  "natural_of_integer = of_nat \<circ> nat_of_integer"
   1.652 +lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   1.653 +  is "nat :: int \<Rightarrow> nat"
   1.654 +  .
   1.655  
   1.656 -definition integer_of_natural :: "natural \<Rightarrow> integer"
   1.657 -where
   1.658 -  "integer_of_natural = of_nat \<circ> nat_of_natural"
   1.659 +lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
   1.660 +  is "of_nat :: nat \<Rightarrow> int"
   1.661 +  .
   1.662  
   1.663  lemma natural_of_integer_of_natural [simp]:
   1.664    "natural_of_integer (integer_of_natural n) = n"
   1.665 -  by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff)
   1.666 +  by transfer simp
   1.667  
   1.668  lemma integer_of_natural_of_integer [simp]:
   1.669    "integer_of_natural (natural_of_integer k) = max 0 k"
   1.670 -  by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff)
   1.671 +  by transfer auto
   1.672  
   1.673  lemma int_of_integer_of_natural [simp]:
   1.674    "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
   1.675 -  by (simp add: integer_of_natural_def)
   1.676 +  by transfer rule
   1.677  
   1.678  lemma integer_of_natural_of_nat [simp]:
   1.679    "integer_of_natural (of_nat n) = of_nat n"
   1.680 -  by (simp add: integer_eq_iff)
   1.681 +  by transfer rule
   1.682  
   1.683  lemma [measure_function]:
   1.684 -  "is_measure nat_of_natural" by (rule is_measure_trivial)
   1.685 +  "is_measure nat_of_natural"
   1.686 +  by (rule is_measure_trivial)
   1.687  
   1.688  
   1.689  subsection {* Inductive represenation of target language naturals *}
   1.690  
   1.691 -definition Suc :: "natural \<Rightarrow> natural"
   1.692 -where
   1.693 -  "Suc = natural_of_nat \<circ> Nat.Suc \<circ> nat_of_natural"
   1.694 +lift_definition Suc :: "natural \<Rightarrow> natural"
   1.695 +  is Nat.Suc
   1.696 +  .
   1.697  
   1.698 -lemma nat_of_natural_Suc [simp]:
   1.699 -  "nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)"
   1.700 -  by (simp add: Suc_def)
   1.701 +declare Suc.rep_eq [simp]
   1.702  
   1.703  rep_datatype "0::natural" Suc
   1.704 -proof -
   1.705 -  fix P :: "natural \<Rightarrow> bool"
   1.706 -  fix n :: natural
   1.707 -  assume "P 0" then have init: "P (natural_of_nat 0)" by simp
   1.708 -  assume "\<And>n. P n \<Longrightarrow> P (Suc n)"
   1.709 -    then have "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (Suc (natural_of_nat n))" .
   1.710 -    then have step: "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (natural_of_nat (Nat.Suc n))"
   1.711 -      by (simp add: Suc_def)
   1.712 -  from init step have "P (natural_of_nat (nat_of_natural n))"
   1.713 -    by (rule nat.induct)
   1.714 -  with natural_of_nat_of_natural_inverse show "P n" by simp
   1.715 -qed (simp_all add: natural_eq_iff)
   1.716 +  by (transfer, fact nat.induct nat.inject nat.distinct)+
   1.717  
   1.718  lemma natural_case [case_names nat, cases type: natural]:
   1.719    fixes m :: natural
   1.720    assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   1.721    shows P
   1.722 -  by (rule assms [of "nat_of_natural m"]) simp
   1.723 +  using assms by transfer blast
   1.724  
   1.725  lemma [simp, code]:
   1.726    "natural_size = nat_of_natural"
   1.727 @@ -778,7 +828,7 @@
   1.728  
   1.729  lemma natural_decr [termination_simp]:
   1.730    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
   1.731 -  by (simp add: natural_eq_iff)
   1.732 +  by transfer simp
   1.733  
   1.734  lemma natural_zero_minus_one:
   1.735    "(0::natural) - 1 = 0"
   1.736 @@ -786,26 +836,26 @@
   1.737  
   1.738  lemma Suc_natural_minus_one:
   1.739    "Suc n - 1 = n"
   1.740 -  by (simp add: natural_eq_iff)
   1.741 +  by transfer simp
   1.742  
   1.743  hide_const (open) Suc
   1.744  
   1.745  
   1.746  subsection {* Code refinement for target language naturals *}
   1.747  
   1.748 -definition Nat :: "integer \<Rightarrow> natural"
   1.749 -where
   1.750 -  "Nat = natural_of_integer"
   1.751 +lift_definition Nat :: "integer \<Rightarrow> natural"
   1.752 +  is nat
   1.753 +  .
   1.754  
   1.755  lemma [code_post]:
   1.756    "Nat 0 = 0"
   1.757    "Nat 1 = 1"
   1.758    "Nat (numeral k) = numeral k"
   1.759 -  by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
   1.760 +  by (transfer, simp)+
   1.761  
   1.762  lemma [code abstype]:
   1.763    "Nat (integer_of_natural n) = n"
   1.764 -  by (unfold Nat_def) (fact natural_of_integer_of_natural)
   1.765 +  by transfer simp
   1.766  
   1.767  lemma [code abstract]:
   1.768    "integer_of_natural (natural_of_nat n) = of_nat n"
   1.769 @@ -817,23 +867,23 @@
   1.770  
   1.771  lemma [code_abbrev]:
   1.772    "natural_of_integer (Code_Numeral_Types.Pos k) = numeral k"
   1.773 -  by (simp add: nat_of_integer_def natural_of_integer_def)
   1.774 +  by transfer simp
   1.775  
   1.776  lemma [code abstract]:
   1.777    "integer_of_natural 0 = 0"
   1.778 -  by (simp add: integer_eq_iff)
   1.779 +  by transfer simp
   1.780  
   1.781  lemma [code abstract]:
   1.782    "integer_of_natural 1 = 1"
   1.783 -  by (simp add: integer_eq_iff)
   1.784 +  by transfer simp
   1.785  
   1.786  lemma [code abstract]:
   1.787    "integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1"
   1.788 -  by (simp add: integer_eq_iff)
   1.789 +  by transfer simp
   1.790  
   1.791  lemma [code]:
   1.792    "nat_of_natural = nat_of_integer \<circ> integer_of_natural"
   1.793 -  by (simp add: integer_of_natural_def fun_eq_iff)
   1.794 +  by transfer (simp add: fun_eq_iff)
   1.795  
   1.796  lemma [code, code_unfold]:
   1.797    "natural_case f g n = (if n = 0 then f else g (n - 1))"
   1.798 @@ -843,39 +893,39 @@
   1.799  
   1.800  lemma [code abstract]:
   1.801    "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
   1.802 -  by (simp add: integer_eq_iff)
   1.803 +  by transfer simp
   1.804  
   1.805  lemma [code abstract]:
   1.806    "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
   1.807 -  by (simp add: integer_eq_iff)
   1.808 +  by transfer simp
   1.809  
   1.810  lemma [code abstract]:
   1.811    "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
   1.812 -  by (simp add: integer_eq_iff of_nat_mult)
   1.813 +  by transfer (simp add: of_nat_mult)
   1.814  
   1.815  lemma [code abstract]:
   1.816    "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
   1.817 -  by (simp add: integer_eq_iff zdiv_int)
   1.818 +  by transfer (simp add: zdiv_int)
   1.819  
   1.820  lemma [code abstract]:
   1.821    "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
   1.822 -  by (simp add: integer_eq_iff zmod_int)
   1.823 +  by transfer (simp add: zmod_int)
   1.824  
   1.825  lemma [code]:
   1.826    "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
   1.827 -  by (simp add: equal natural_eq_iff integer_eq_iff)
   1.828 +  by transfer (simp add: equal)
   1.829  
   1.830  lemma [code nbe]:
   1.831    "HOL.equal n (n::natural) \<longleftrightarrow> True"
   1.832    by (simp add: equal)
   1.833  
   1.834  lemma [code]:
   1.835 -  "m \<le> n \<longleftrightarrow> (integer_of_natural m) \<le> integer_of_natural n"
   1.836 -  by (simp add: less_eq_natural_def less_eq_integer_def)
   1.837 +  "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
   1.838 +  by transfer simp
   1.839  
   1.840  lemma [code]:
   1.841 -  "m < n \<longleftrightarrow> (integer_of_natural m) < integer_of_natural n"
   1.842 -  by (simp add: less_natural_def less_integer_def)
   1.843 +  "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
   1.844 +  by transfer simp
   1.845  
   1.846  hide_const (open) Nat
   1.847  
     2.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 12:24:56 2013 +0100
     2.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 12:24:56 2013 +0100
     2.3 @@ -15,47 +15,47 @@
     2.4  
     2.5  lemma [code]:
     2.6    "integer_of_int (int_of_integer k) = k"
     2.7 -  by (simp add: integer_eq_iff)
     2.8 +  by transfer rule
     2.9  
    2.10  lemma [code]:
    2.11    "Int.Pos = int_of_integer \<circ> integer_of_num"
    2.12 -  by (simp add: integer_of_num_def fun_eq_iff)
    2.13 +  by transfer (simp add: fun_eq_iff) 
    2.14  
    2.15  lemma [code]:
    2.16    "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
    2.17 -  by (simp add: integer_of_num_def fun_eq_iff)
    2.18 +  by transfer (simp add: fun_eq_iff) 
    2.19  
    2.20  lemma [code_abbrev]:
    2.21    "int_of_integer (numeral k) = Int.Pos k"
    2.22 -  by simp
    2.23 +  by transfer simp
    2.24  
    2.25  lemma [code_abbrev]:
    2.26    "int_of_integer (neg_numeral k) = Int.Neg k"
    2.27 -  by simp
    2.28 +  by transfer simp
    2.29    
    2.30  lemma [code, symmetric, code_post]:
    2.31    "0 = int_of_integer 0"
    2.32 -  by simp
    2.33 +  by transfer simp
    2.34  
    2.35  lemma [code, symmetric, code_post]:
    2.36    "1 = int_of_integer 1"
    2.37 -  by simp
    2.38 +  by transfer simp
    2.39  
    2.40  lemma [code]:
    2.41    "k + l = int_of_integer (of_int k + of_int l)"
    2.42 -  by simp
    2.43 +  by transfer simp
    2.44  
    2.45  lemma [code]:
    2.46    "- k = int_of_integer (- of_int k)"
    2.47 -  by simp
    2.48 +  by transfer simp
    2.49  
    2.50  lemma [code]:
    2.51    "k - l = int_of_integer (of_int k - of_int l)"
    2.52 -  by simp
    2.53 +  by transfer simp
    2.54  
    2.55  lemma [code]:
    2.56    "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
    2.57 -  by simp
    2.58 +  by transfer simp
    2.59  
    2.60  lemma [code, code del]:
    2.61    "Int.sub = Int.sub" ..
    2.62 @@ -79,15 +79,15 @@
    2.63  
    2.64  lemma [code]:
    2.65    "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
    2.66 -  by (simp add: equal integer_eq_iff)
    2.67 +  by transfer (simp add: equal)
    2.68  
    2.69  lemma [code]:
    2.70    "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
    2.71 -  by (simp add: less_eq_int_def)
    2.72 +  by transfer rule
    2.73  
    2.74  lemma [code]:
    2.75    "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    2.76 -  by (simp add: less_int_def)
    2.77 +  by transfer rule
    2.78  
    2.79  lemma (in ring_1) of_int_code:
    2.80    "of_int k = (if k = 0 then 0
    2.81 @@ -107,7 +107,7 @@
    2.82  
    2.83  lemma [code]:
    2.84    "nat = nat_of_integer \<circ> of_int"
    2.85 -  by (simp add: fun_eq_iff nat_of_integer_def)
    2.86 +  by transfer (simp add: fun_eq_iff)
    2.87  
    2.88  code_modulename SML
    2.89    Code_Target_Int Arith
     3.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Thu Feb 14 12:24:56 2013 +0100
     3.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Feb 14 12:24:56 2013 +0100
     3.3 @@ -10,47 +10,47 @@
     3.4  
     3.5  subsection {* Implementation for @{typ nat} *}
     3.6  
     3.7 -definition Nat :: "integer \<Rightarrow> nat"
     3.8 -where
     3.9 -  "Nat = nat_of_integer"
    3.10 +lift_definition Nat :: "integer \<Rightarrow> nat"
    3.11 +  is nat
    3.12 +  .
    3.13  
    3.14  lemma [code_post]:
    3.15    "Nat 0 = 0"
    3.16    "Nat 1 = 1"
    3.17    "Nat (numeral k) = numeral k"
    3.18 -  by (simp_all add: Nat_def nat_of_integer_def)
    3.19 +  by (transfer, simp)+
    3.20  
    3.21  lemma [code_abbrev]:
    3.22    "integer_of_nat = of_nat"
    3.23 -  by (fact integer_of_nat_def)
    3.24 +  by transfer rule
    3.25  
    3.26  lemma [code_unfold]:
    3.27    "Int.nat (int_of_integer k) = nat_of_integer k"
    3.28 -  by (simp add: nat_of_integer_def)
    3.29 +  by transfer rule
    3.30  
    3.31  lemma [code abstype]:
    3.32    "Code_Target_Nat.Nat (integer_of_nat n) = n"
    3.33 -  by (simp add: Nat_def integer_of_nat_def)
    3.34 +  by transfer simp
    3.35  
    3.36  lemma [code abstract]:
    3.37    "integer_of_nat (nat_of_integer k) = max 0 k"
    3.38 -  by (simp add: integer_of_nat_def)
    3.39 +  by transfer auto
    3.40  
    3.41  lemma [code_abbrev]:
    3.42    "nat_of_integer (numeral k) = nat_of_num k"
    3.43 -  by (simp add: nat_of_integer_def nat_of_num_numeral)
    3.44 +  by transfer (simp add: nat_of_num_numeral)
    3.45  
    3.46  lemma [code abstract]:
    3.47    "integer_of_nat (nat_of_num n) = integer_of_num n"
    3.48 -  by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
    3.49 +  by transfer (simp add: nat_of_num_numeral)
    3.50  
    3.51  lemma [code abstract]:
    3.52    "integer_of_nat 0 = 0"
    3.53 -  by (simp add: integer_eq_iff integer_of_nat_def)
    3.54 +  by transfer simp
    3.55  
    3.56  lemma [code abstract]:
    3.57    "integer_of_nat 1 = 1"
    3.58 -  by (simp add: integer_eq_iff integer_of_nat_def)
    3.59 +  by transfer simp
    3.60  
    3.61  lemma [code]:
    3.62    "Suc n = n + 1"
    3.63 @@ -58,23 +58,23 @@
    3.64  
    3.65  lemma [code abstract]:
    3.66    "integer_of_nat (m + n) = of_nat m + of_nat n"
    3.67 -  by (simp add: integer_eq_iff integer_of_nat_def)
    3.68 +  by transfer simp
    3.69  
    3.70  lemma [code abstract]:
    3.71    "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
    3.72 -  by (simp add: integer_eq_iff integer_of_nat_def)
    3.73 +  by transfer simp
    3.74  
    3.75  lemma [code abstract]:
    3.76    "integer_of_nat (m * n) = of_nat m * of_nat n"
    3.77 -  by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
    3.78 +  by transfer (simp add: of_nat_mult)
    3.79  
    3.80  lemma [code abstract]:
    3.81    "integer_of_nat (m div n) = of_nat m div of_nat n"
    3.82 -  by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
    3.83 +  by transfer (simp add: zdiv_int)
    3.84  
    3.85  lemma [code abstract]:
    3.86    "integer_of_nat (m mod n) = of_nat m mod of_nat n"
    3.87 -  by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
    3.88 +  by transfer (simp add: zmod_int)
    3.89  
    3.90  lemma [code]:
    3.91    "Divides.divmod_nat m n = (m div n, m mod n)"
    3.92 @@ -82,7 +82,7 @@
    3.93  
    3.94  lemma [code]:
    3.95    "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
    3.96 -  by (simp add: equal integer_eq_iff)
    3.97 +  by transfer (simp add: equal)
    3.98  
    3.99  lemma [code]:
   3.100    "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
   3.101 @@ -94,7 +94,7 @@
   3.102  
   3.103  lemma num_of_nat_code [code]:
   3.104    "num_of_nat = num_of_integer \<circ> of_nat"
   3.105 -  by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
   3.106 +  by transfer (simp add: fun_eq_iff)
   3.107  
   3.108  lemma (in semiring_1) of_nat_code:
   3.109    "of_nat n = (if n = 0 then 0
   3.110 @@ -121,7 +121,7 @@
   3.111  
   3.112  lemma [code abstract]:
   3.113    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
   3.114 -  by (simp add: integer_of_nat_def of_int_of_nat max_def)
   3.115 +  by transfer auto
   3.116  
   3.117  code_modulename SML
   3.118    Code_Target_Nat Arith