# HG changeset patch
# User haftmann
# Date 1360841096 -3600
# Node ID 3e913a575dc677215aafc07aa63b44d0e7b68e09
# Parent  222fb6cb2c3eaa088a4c08311271efb2aa22e246
type lifting setup for code numeral types

diff -r 222fb6cb2c3e -r 3e913a575dc6 src/HOL/Library/Code_Numeral_Types.thy
--- a/src/HOL/Library/Code_Numeral_Types.thy	Thu Feb 14 12:24:56 2013 +0100
+++ b/src/HOL/Library/Code_Numeral_Types.thy	Thu Feb 14 12:24:56 2013 +0100
@@ -13,9 +13,11 @@
 typedef integer = "UNIV \<Colon> int set"
   morphisms int_of_integer integer_of_int ..
 
+setup_lifting (no_code) type_definition_integer
+
 lemma integer_eq_iff:
   "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
-  using int_of_integer_inject [of k l] ..
+  by transfer rule
 
 lemma integer_eqI:
   "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
@@ -23,172 +25,199 @@
 
 lemma int_of_integer_integer_of_int [simp]:
   "int_of_integer (integer_of_int k) = k"
-  using integer_of_int_inverse [of k] by simp
+  by transfer rule
 
 lemma integer_of_int_int_of_integer [simp]:
   "integer_of_int (int_of_integer k) = k"
-  using int_of_integer_inverse [of k] by simp
+  by transfer rule
 
 instantiation integer :: ring_1
 begin
 
-definition
-  "0 = integer_of_int 0"
+lift_definition zero_integer :: integer
+  is "0 :: int"
+  .
 
-lemma int_of_integer_zero [simp]:
-  "int_of_integer 0 = 0"
-  by (simp add: zero_integer_def)
-
-definition
-  "1 = integer_of_int 1"
+declare zero_integer.rep_eq [simp]
 
-lemma int_of_integer_one [simp]:
-  "int_of_integer 1 = 1"
-  by (simp add: one_integer_def)
+lift_definition one_integer :: integer
+  is "1 :: int"
+  .
+
+declare one_integer.rep_eq [simp]
 
-definition
-  "k + l = integer_of_int (int_of_integer k + int_of_integer l)"
+lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "plus :: int \<Rightarrow> int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_plus [simp]:
-  "int_of_integer (k + l) = int_of_integer k + int_of_integer l"
-  by (simp add: plus_integer_def)
+declare plus_integer.rep_eq [simp]
 
-definition
-  "- k = integer_of_int (- int_of_integer k)"
+lift_definition uminus_integer :: "integer \<Rightarrow> integer"
+  is "uminus :: int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_uminus [simp]:
-  "int_of_integer (- k) = - int_of_integer k"
-  by (simp add: uminus_integer_def)
-
-definition
-  "k - l = integer_of_int (int_of_integer k - int_of_integer l)"
+declare uminus_integer.rep_eq [simp]
 
-lemma int_of_integer_minus [simp]:
-  "int_of_integer (k - l) = int_of_integer k - int_of_integer l"
-  by (simp add: minus_integer_def)
+lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "minus :: int \<Rightarrow> int \<Rightarrow> int"
+  .
+
+declare minus_integer.rep_eq [simp]
 
-definition
-  "k * l = integer_of_int (int_of_integer k * int_of_integer l)"
+lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "times :: int \<Rightarrow> int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_times [simp]:
-  "int_of_integer (k * l) = int_of_integer k * int_of_integer l"
-  by (simp add: times_integer_def)
+declare times_integer.rep_eq [simp]
 
 instance proof
-qed (auto simp add: integer_eq_iff algebra_simps)
+qed (transfer, simp add: algebra_simps)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+  by (unfold of_nat_def [abs_def])  transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+proof -
+  have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+    by (unfold of_int_of_nat [abs_def]) transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
+proof -
+  have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+    by transfer_prover
+  then show ?thesis by simp
+qed
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
+  by (unfold neg_numeral_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold Num.sub_def [abs_def]) transfer_prover
+
 lemma int_of_integer_of_nat [simp]:
   "int_of_integer (of_nat n) = of_nat n"
-  by (induct n) simp_all
+  by transfer rule
 
-definition integer_of_nat :: "nat \<Rightarrow> integer"
-where
-  "integer_of_nat = of_nat"
+lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
+  is "of_nat :: nat \<Rightarrow> int"
+  .
 
 lemma int_of_integer_integer_of_nat [simp]:
   "int_of_integer (integer_of_nat n) = of_nat n"
-  by (simp add: integer_of_nat_def)
-  
-definition nat_of_integer :: "integer \<Rightarrow> nat"
-where
-  "nat_of_integer k = Int.nat (int_of_integer k)"
+  by transfer rule
+
+lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
+  is Int.nat
+  .
 
 lemma nat_of_integer_of_nat [simp]:
   "nat_of_integer (of_nat n) = n"
-  by (simp add: nat_of_integer_def)
+  by transfer simp
 
 lemma int_of_integer_of_int [simp]:
   "int_of_integer (of_int k) = k"
-  by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
+  by transfer simp
 
 lemma nat_of_integer_integer_of_nat [simp]:
   "nat_of_integer (integer_of_nat n) = n"
-  by (simp add: integer_of_nat_def)
+  by transfer simp
 
 lemma integer_of_int_eq_of_int [simp, code_abbrev]:
   "integer_of_int = of_int"
-  by rule (simp add: integer_eq_iff)
+  by transfer (simp add: fun_eq_iff)
 
 lemma of_int_integer_of [simp]:
   "of_int (int_of_integer k) = (k :: integer)"
-  by (simp add: integer_eq_iff)
+  by transfer rule
 
 lemma int_of_integer_numeral [simp]:
   "int_of_integer (numeral k) = numeral k"
-  using int_of_integer_of_int [of "numeral k"] by simp
+  by transfer rule
 
 lemma int_of_integer_neg_numeral [simp]:
   "int_of_integer (neg_numeral k) = neg_numeral k"
-  by (simp only: neg_numeral_def int_of_integer_uminus) simp
+  by transfer rule
 
 lemma int_of_integer_sub [simp]:
   "int_of_integer (Num.sub k l) = Num.sub k l"
-  by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral)
+  by transfer rule
 
 instantiation integer :: "{ring_div, equal, linordered_idom}"
 begin
 
-definition
-  "k div l = of_int (int_of_integer k div int_of_integer l)"
+lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
+  .
 
-lemma int_of_integer_div [simp]:
-  "int_of_integer (k div l) = int_of_integer k div int_of_integer l"
-  by (simp add: div_integer_def)
+declare div_integer.rep_eq [simp]
 
-definition
-  "k mod l = of_int (int_of_integer k mod int_of_integer l)"
+lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
+  .
+
+declare mod_integer.rep_eq [simp]
 
-lemma int_of_integer_mod [simp]:
-  "int_of_integer (k mod l) = int_of_integer k mod int_of_integer l"
-  by (simp add: mod_integer_def)
+lift_definition abs_integer :: "integer \<Rightarrow> integer"
+  is "abs :: int \<Rightarrow> int"
+  .
 
-definition
-  "\<bar>k\<bar> = of_int \<bar>int_of_integer k\<bar>"
+declare abs_integer.rep_eq [simp]
 
-lemma int_of_integer_abs [simp]:
-  "int_of_integer \<bar>k\<bar> = \<bar>int_of_integer k\<bar>"
-  by (simp add: abs_integer_def)
+lift_definition sgn_integer :: "integer \<Rightarrow> integer"
+  is "sgn :: int \<Rightarrow> int"
+  .
 
-definition
-  "sgn k = of_int (sgn (int_of_integer k))"
+declare sgn_integer.rep_eq [simp]
 
-lemma int_of_integer_sgn [simp]:
-  "int_of_integer (sgn k) = sgn (int_of_integer k)"
-  by (simp add: sgn_integer_def)
+lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
 
-definition
-  "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
+lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "less :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
 
-definition
-  "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
-
-definition
-  "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of_integer k) (int_of_integer l)"
+lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
 
 instance proof
-qed (auto simp add: integer_eq_iff algebra_simps
-  less_eq_integer_def less_integer_def equal_integer_def equal
-  intro: mult_strict_right_mono)
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold max_def [abs_def]) transfer_prover
+
 lemma int_of_integer_min [simp]:
   "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
-  by (simp add: min_def less_eq_integer_def)
+  by transfer rule
 
 lemma int_of_integer_max [simp]:
   "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
-  by (simp add: max_def less_eq_integer_def)
+  by transfer rule
 
 lemma nat_of_integer_non_positive [simp]:
   "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
-  by (simp add: nat_of_integer_def less_eq_integer_def)
+  by transfer simp
 
 lemma of_nat_of_integer [simp]:
   "of_nat (nat_of_integer k) = max 0 k"
-  by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def)
+  by transfer auto
 
 
 subsection {* Code theorems for target language integers *}
@@ -199,29 +228,36 @@
 where
   [simp, code_abbrev]: "Pos = numeral"
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer numeral Pos"
+  by simp transfer_prover
+
 definition Neg :: "num \<Rightarrow> integer"
 where
   [simp, code_abbrev]: "Neg = neg_numeral"
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_integer neg_numeral Neg"
+  by simp transfer_prover
+
 code_datatype "0::integer" Pos Neg
 
 
 text {* Auxiliary operations *}
 
-definition dup :: "integer \<Rightarrow> integer"
-where
-  [simp]: "dup k = k + k"
+lift_definition dup :: "integer \<Rightarrow> integer"
+  is "\<lambda>k::int. k + k"
+  .
 
 lemma dup_code [code]:
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
-  unfolding Pos_def Neg_def neg_numeral_def
-  by (simp_all add: numeral_Bit0)
+  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
 
-definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
-where
-  [simp]: "sub m n = numeral m - numeral n"
+lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
+  is "\<lambda>m n. numeral m - numeral n :: int"
+  .
 
 lemma sub_code [code]:
   "sub Num.One Num.One = 0"
@@ -233,9 +269,7 @@
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
-  unfolding sub_def dup_def numeral.simps Pos_def Neg_def
-    neg_numeral_def numeral_BitM
-  by (simp_all only: algebra_simps add.comm_neutral)
+  by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
 
 
 text {* Implementations *}
@@ -251,7 +285,7 @@
   "Pos m + Neg n = sub m n"
   "Neg m + Pos n = sub n m"
   "Neg m + Neg n = Neg (m + n)"
-  by simp_all
+  by (transfer, simp)+
 
 lemma uminus_integer_code [code]:
   "uminus 0 = (0::integer)"
@@ -266,7 +300,7 @@
   "Pos m - Neg n = Pos (m + n)"
   "Neg m - Pos n = Neg (m + n)"
   "Neg m - Neg n = sub n m"
-  by simp_all
+  by (transfer, simp)+
 
 lemma abs_integer_code [code]:
   "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
@@ -322,15 +356,18 @@
     (let j = sub k l in
        if j < 0 then (0, Pos k)
        else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
-  by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta
-    sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+  apply (simp add: prod_eq_iff Let_def prod_case_beta)
+  apply transfer
+  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+  done
 
-lemma divmod_integer_code [code]: "divmod_integer k l =
-  (if k = 0 then (0, 0) else if l = 0 then (0, k) else
-  (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
-    then divmod_abs k l
-    else (let (r, s) = divmod_abs k l in
-      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+lemma divmod_integer_code [code]:
+  "divmod_integer k l =
+    (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+    (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
+      then divmod_abs k l
+      else (let (r, s) = divmod_abs k l in
+        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
 proof -
   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"
     by (auto simp add: sgn_if)
@@ -358,7 +395,7 @@
   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
-  by (simp_all add: equal integer_eq_iff)
+  by (simp_all add: equal)
 
 lemma equal_integer_refl [code nbe]:
   "HOL.equal (k::integer) k \<longleftrightarrow> True"
@@ -374,7 +411,7 @@
   "Neg k \<le> 0 \<longleftrightarrow> True"
   "Neg k \<le> Pos l \<longleftrightarrow> True"
   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
-  by (simp_all add: less_eq_integer_def)
+  by simp_all
 
 lemma less_integer_code [code]:
   "0 < (0::integer) \<longleftrightarrow> False"
@@ -386,21 +423,21 @@
   "Neg k < 0 \<longleftrightarrow> True"
   "Neg k < Pos l \<longleftrightarrow> True"
   "Neg k < Neg l \<longleftrightarrow> l < k"
-  by (simp_all add: less_integer_def)
+  by simp_all
 
-definition integer_of_num :: "num \<Rightarrow> integer"
-where
-  "integer_of_num = numeral"
+lift_definition integer_of_num :: "num \<Rightarrow> integer"
+  is "numeral :: num \<Rightarrow> int"
+  .
 
 lemma integer_of_num [code]:
   "integer_of_num num.One = 1"
   "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
   "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
-  by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps)
+  by (transfer, simp only: numeral.simps Let_def)+
 
-definition num_of_integer :: "integer \<Rightarrow> num"
-where
-  "num_of_integer = num_of_nat \<circ> nat_of_integer"
+lift_definition num_of_integer :: "integer \<Rightarrow> num"
+  is "num_of_nat \<circ> nat"
+  .
 
 lemma num_of_integer_code [code]:
   "num_of_integer k = (if k \<le> 1 then Num.One
@@ -587,9 +624,11 @@
 typedef natural = "UNIV \<Colon> nat set"
   morphisms nat_of_natural natural_of_nat ..
 
+setup_lifting (no_code) type_definition_natural
+
 lemma natural_eq_iff [termination_simp]:
   "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
-  using nat_of_natural_inject [of m n] ..
+  by transfer rule
 
 lemma natural_eqI:
   "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
@@ -597,168 +636,179 @@
 
 lemma nat_of_natural_of_nat_inverse [simp]:
   "nat_of_natural (natural_of_nat n) = n"
-  using natural_of_nat_inverse [of n] by simp
+  by transfer rule
 
 lemma natural_of_nat_of_natural_inverse [simp]:
   "natural_of_nat (nat_of_natural n) = n"
-  using nat_of_natural_inverse [of n] by simp
+  by transfer rule
 
 instantiation natural :: "{comm_monoid_diff, semiring_1}"
 begin
 
-definition
-  "0 = natural_of_nat 0"
+lift_definition zero_natural :: natural
+  is "0 :: nat"
+  .
 
-lemma nat_of_natural_zero [simp]:
-  "nat_of_natural 0 = 0"
-  by (simp add: zero_natural_def)
+declare zero_natural.rep_eq [simp]
 
-definition
-  "1 = natural_of_nat 1"
+lift_definition one_natural :: natural
+  is "1 :: nat"
+  .
 
-lemma nat_of_natural_one [simp]:
-  "nat_of_natural 1 = 1"
-  by (simp add: one_natural_def)
-
-definition
-  "m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)"
+declare one_natural.rep_eq [simp]
 
-lemma nat_of_natural_plus [simp]:
-  "nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n"
-  by (simp add: plus_natural_def)
+lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
 
-definition
-  "m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)"
+declare plus_natural.rep_eq [simp]
 
-lemma nat_of_natural_minus [simp]:
-  "nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n"
-  by (simp add: minus_natural_def)
+lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
+
+declare minus_natural.rep_eq [simp]
 
-definition
-  "m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)"
+lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
 
-lemma nat_of_natural_times [simp]:
-  "nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n"
-  by (simp add: times_natural_def)
+declare times_natural.rep_eq [simp]
 
 instance proof
-qed (auto simp add: natural_eq_iff algebra_simps)
+qed (transfer, simp add: algebra_simps)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+proof -
+  have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+    by (unfold of_nat_def [abs_def]) transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+  "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+proof -
+  have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+    by transfer_prover
+  then show ?thesis by simp
+qed
+
 lemma nat_of_natural_of_nat [simp]:
   "nat_of_natural (of_nat n) = n"
-  by (induct n) simp_all
+  by transfer rule
 
 lemma natural_of_nat_of_nat [simp, code_abbrev]:
   "natural_of_nat = of_nat"
-  by rule (simp add: natural_eq_iff)
+  by transfer rule
 
 lemma of_nat_of_natural [simp]:
   "of_nat (nat_of_natural n) = n"
-  using natural_of_nat_of_natural_inverse [of n] by simp
+  by transfer rule
 
 lemma nat_of_natural_numeral [simp]:
   "nat_of_natural (numeral k) = numeral k"
-  using nat_of_natural_of_nat [of "numeral k"] by simp
+  by transfer rule
 
 instantiation natural :: "{semiring_div, equal, linordered_semiring}"
 begin
 
-definition
-  "m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)"
+lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
+
+declare div_natural.rep_eq [simp]
 
-lemma nat_of_natural_div [simp]:
-  "nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n"
-  by (simp add: div_natural_def)
+lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
 
-definition
-  "m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)"
+declare mod_natural.rep_eq [simp]
 
-lemma nat_of_natural_mod [simp]:
-  "nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n"
-  by (simp add: mod_natural_def)
+lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
+
+declare less_eq_natural.rep_eq [termination_simp]
 
-definition
-  [termination_simp]: "m \<le> n \<longleftrightarrow> nat_of_natural m \<le> nat_of_natural n"
+lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
 
-definition
-  [termination_simp]: "m < n \<longleftrightarrow> nat_of_natural m < nat_of_natural n"
+declare less_natural.rep_eq [termination_simp]
 
-definition
-  "HOL.equal m n \<longleftrightarrow> HOL.equal (nat_of_natural m) (nat_of_natural n)"
+lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
 
 instance proof
-qed (auto simp add: natural_eq_iff algebra_simps
-  less_eq_natural_def less_natural_def equal_natural_def equal)
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
 
 end
 
+lemma [transfer_rule]:
+  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold max_def [abs_def]) transfer_prover
+
 lemma nat_of_natural_min [simp]:
   "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
-  by (simp add: min_def less_eq_natural_def)
+  by transfer rule
 
 lemma nat_of_natural_max [simp]:
   "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
-  by (simp add: max_def less_eq_natural_def)
+  by transfer rule
 
-definition natural_of_integer :: "integer \<Rightarrow> natural"
-where
-  "natural_of_integer = of_nat \<circ> nat_of_integer"
+lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
+  is "nat :: int \<Rightarrow> nat"
+  .
 
-definition integer_of_natural :: "natural \<Rightarrow> integer"
-where
-  "integer_of_natural = of_nat \<circ> nat_of_natural"
+lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
+  is "of_nat :: nat \<Rightarrow> int"
+  .
 
 lemma natural_of_integer_of_natural [simp]:
   "natural_of_integer (integer_of_natural n) = n"
-  by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff)
+  by transfer simp
 
 lemma integer_of_natural_of_integer [simp]:
   "integer_of_natural (natural_of_integer k) = max 0 k"
-  by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff)
+  by transfer auto
 
 lemma int_of_integer_of_natural [simp]:
   "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
-  by (simp add: integer_of_natural_def)
+  by transfer rule
 
 lemma integer_of_natural_of_nat [simp]:
   "integer_of_natural (of_nat n) = of_nat n"
-  by (simp add: integer_eq_iff)
+  by transfer rule
 
 lemma [measure_function]:
-  "is_measure nat_of_natural" by (rule is_measure_trivial)
+  "is_measure nat_of_natural"
+  by (rule is_measure_trivial)
 
 
 subsection {* Inductive represenation of target language naturals *}
 
-definition Suc :: "natural \<Rightarrow> natural"
-where
-  "Suc = natural_of_nat \<circ> Nat.Suc \<circ> nat_of_natural"
+lift_definition Suc :: "natural \<Rightarrow> natural"
+  is Nat.Suc
+  .
 
-lemma nat_of_natural_Suc [simp]:
-  "nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)"
-  by (simp add: Suc_def)
+declare Suc.rep_eq [simp]
 
 rep_datatype "0::natural" Suc
-proof -
-  fix P :: "natural \<Rightarrow> bool"
-  fix n :: natural
-  assume "P 0" then have init: "P (natural_of_nat 0)" by simp
-  assume "\<And>n. P n \<Longrightarrow> P (Suc n)"
-    then have "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (Suc (natural_of_nat n))" .
-    then have step: "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (natural_of_nat (Nat.Suc n))"
-      by (simp add: Suc_def)
-  from init step have "P (natural_of_nat (nat_of_natural n))"
-    by (rule nat.induct)
-  with natural_of_nat_of_natural_inverse show "P n" by simp
-qed (simp_all add: natural_eq_iff)
+  by (transfer, fact nat.induct nat.inject nat.distinct)+
 
 lemma natural_case [case_names nat, cases type: natural]:
   fixes m :: natural
   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   shows P
-  by (rule assms [of "nat_of_natural m"]) simp
+  using assms by transfer blast
 
 lemma [simp, code]:
   "natural_size = nat_of_natural"
@@ -778,7 +828,7 @@
 
 lemma natural_decr [termination_simp]:
   "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
-  by (simp add: natural_eq_iff)
+  by transfer simp
 
 lemma natural_zero_minus_one:
   "(0::natural) - 1 = 0"
@@ -786,26 +836,26 @@
 
 lemma Suc_natural_minus_one:
   "Suc n - 1 = n"
-  by (simp add: natural_eq_iff)
+  by transfer simp
 
 hide_const (open) Suc
 
 
 subsection {* Code refinement for target language naturals *}
 
-definition Nat :: "integer \<Rightarrow> natural"
-where
-  "Nat = natural_of_integer"
+lift_definition Nat :: "integer \<Rightarrow> natural"
+  is nat
+  .
 
 lemma [code_post]:
   "Nat 0 = 0"
   "Nat 1 = 1"
   "Nat (numeral k) = numeral k"
-  by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
+  by (transfer, simp)+
 
 lemma [code abstype]:
   "Nat (integer_of_natural n) = n"
-  by (unfold Nat_def) (fact natural_of_integer_of_natural)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (natural_of_nat n) = of_nat n"
@@ -817,23 +867,23 @@
 
 lemma [code_abbrev]:
   "natural_of_integer (Code_Numeral_Types.Pos k) = numeral k"
-  by (simp add: nat_of_integer_def natural_of_integer_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural 0 = 0"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural 1 = 1"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code]:
   "nat_of_natural = nat_of_integer \<circ> integer_of_natural"
-  by (simp add: integer_of_natural_def fun_eq_iff)
+  by transfer (simp add: fun_eq_iff)
 
 lemma [code, code_unfold]:
   "natural_case f g n = (if n = 0 then f else g (n - 1))"
@@ -843,39 +893,39 @@
 
 lemma [code abstract]:
   "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
-  by (simp add: integer_eq_iff)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
-  by (simp add: integer_eq_iff of_nat_mult)
+  by transfer (simp add: of_nat_mult)
 
 lemma [code abstract]:
   "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
-  by (simp add: integer_eq_iff zdiv_int)
+  by transfer (simp add: zdiv_int)
 
 lemma [code abstract]:
   "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
-  by (simp add: integer_eq_iff zmod_int)
+  by transfer (simp add: zmod_int)
 
 lemma [code]:
   "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
-  by (simp add: equal natural_eq_iff integer_eq_iff)
+  by transfer (simp add: equal)
 
 lemma [code nbe]:
   "HOL.equal n (n::natural) \<longleftrightarrow> True"
   by (simp add: equal)
 
 lemma [code]:
-  "m \<le> n \<longleftrightarrow> (integer_of_natural m) \<le> integer_of_natural n"
-  by (simp add: less_eq_natural_def less_eq_integer_def)
+  "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
+  by transfer simp
 
 lemma [code]:
-  "m < n \<longleftrightarrow> (integer_of_natural m) < integer_of_natural n"
-  by (simp add: less_natural_def less_integer_def)
+  "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
+  by transfer simp
 
 hide_const (open) Nat
 
diff -r 222fb6cb2c3e -r 3e913a575dc6 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 12:24:56 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Feb 14 12:24:56 2013 +0100
@@ -15,47 +15,47 @@
 
 lemma [code]:
   "integer_of_int (int_of_integer k) = k"
-  by (simp add: integer_eq_iff)
+  by transfer rule
 
 lemma [code]:
   "Int.Pos = int_of_integer \<circ> integer_of_num"
-  by (simp add: integer_of_num_def fun_eq_iff)
+  by transfer (simp add: fun_eq_iff) 
 
 lemma [code]:
   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
-  by (simp add: integer_of_num_def fun_eq_iff)
+  by transfer (simp add: fun_eq_iff) 
 
 lemma [code_abbrev]:
   "int_of_integer (numeral k) = Int.Pos k"
-  by simp
+  by transfer simp
 
 lemma [code_abbrev]:
   "int_of_integer (neg_numeral k) = Int.Neg k"
-  by simp
+  by transfer simp
   
 lemma [code, symmetric, code_post]:
   "0 = int_of_integer 0"
-  by simp
+  by transfer simp
 
 lemma [code, symmetric, code_post]:
   "1 = int_of_integer 1"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "k + l = int_of_integer (of_int k + of_int l)"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "- k = int_of_integer (- of_int k)"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "k - l = int_of_integer (of_int k - of_int l)"
-  by simp
+  by transfer simp
 
 lemma [code]:
   "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
-  by simp
+  by transfer simp
 
 lemma [code, code del]:
   "Int.sub = Int.sub" ..
@@ -79,15 +79,15 @@
 
 lemma [code]:
   "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
-  by (simp add: equal integer_eq_iff)
+  by transfer (simp add: equal)
 
 lemma [code]:
   "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
-  by (simp add: less_eq_int_def)
+  by transfer rule
 
 lemma [code]:
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
-  by (simp add: less_int_def)
+  by transfer rule
 
 lemma (in ring_1) of_int_code:
   "of_int k = (if k = 0 then 0
@@ -107,7 +107,7 @@
 
 lemma [code]:
   "nat = nat_of_integer \<circ> of_int"
-  by (simp add: fun_eq_iff nat_of_integer_def)
+  by transfer (simp add: fun_eq_iff)
 
 code_modulename SML
   Code_Target_Int Arith
diff -r 222fb6cb2c3e -r 3e913a575dc6 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Thu Feb 14 12:24:56 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Feb 14 12:24:56 2013 +0100
@@ -10,47 +10,47 @@
 
 subsection {* Implementation for @{typ nat} *}
 
-definition Nat :: "integer \<Rightarrow> nat"
-where
-  "Nat = nat_of_integer"
+lift_definition Nat :: "integer \<Rightarrow> nat"
+  is nat
+  .
 
 lemma [code_post]:
   "Nat 0 = 0"
   "Nat 1 = 1"
   "Nat (numeral k) = numeral k"
-  by (simp_all add: Nat_def nat_of_integer_def)
+  by (transfer, simp)+
 
 lemma [code_abbrev]:
   "integer_of_nat = of_nat"
-  by (fact integer_of_nat_def)
+  by transfer rule
 
 lemma [code_unfold]:
   "Int.nat (int_of_integer k) = nat_of_integer k"
-  by (simp add: nat_of_integer_def)
+  by transfer rule
 
 lemma [code abstype]:
   "Code_Target_Nat.Nat (integer_of_nat n) = n"
-  by (simp add: Nat_def integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_integer k) = max 0 k"
-  by (simp add: integer_of_nat_def)
+  by transfer auto
 
 lemma [code_abbrev]:
   "nat_of_integer (numeral k) = nat_of_num k"
-  by (simp add: nat_of_integer_def nat_of_num_numeral)
+  by transfer (simp add: nat_of_num_numeral)
 
 lemma [code abstract]:
   "integer_of_nat (nat_of_num n) = integer_of_num n"
-  by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
+  by transfer (simp add: nat_of_num_numeral)
 
 lemma [code abstract]:
   "integer_of_nat 0 = 0"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat 1 = 1"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
 
 lemma [code]:
   "Suc n = n + 1"
@@ -58,23 +58,23 @@
 
 lemma [code abstract]:
   "integer_of_nat (m + n) = of_nat m + of_nat n"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
-  by (simp add: integer_eq_iff integer_of_nat_def)
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_nat (m * n) = of_nat m * of_nat n"
-  by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
+  by transfer (simp add: of_nat_mult)
 
 lemma [code abstract]:
   "integer_of_nat (m div n) = of_nat m div of_nat n"
-  by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
+  by transfer (simp add: zdiv_int)
 
 lemma [code abstract]:
   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
-  by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
+  by transfer (simp add: zmod_int)
 
 lemma [code]:
   "Divides.divmod_nat m n = (m div n, m mod n)"
@@ -82,7 +82,7 @@
 
 lemma [code]:
   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
-  by (simp add: equal integer_eq_iff)
+  by transfer (simp add: equal)
 
 lemma [code]:
   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
@@ -94,7 +94,7 @@
 
 lemma num_of_nat_code [code]:
   "num_of_nat = num_of_integer \<circ> of_nat"
-  by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
+  by transfer (simp add: fun_eq_iff)
 
 lemma (in semiring_1) of_nat_code:
   "of_nat n = (if n = 0 then 0
@@ -121,7 +121,7 @@
 
 lemma [code abstract]:
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
-  by (simp add: integer_of_nat_def of_int_of_nat max_def)
+  by transfer auto
 
 code_modulename SML
   Code_Target_Nat Arith