src/HOL/Nat_Transfer.thy

 subsection {* Set up transfer from nat to int *}
 
 text {* set up transfer direction *}
 
 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
-  by (simp add: transfer_morphism_def)
-
-declare transfer_morphism_nat_int [transfer
-  add mode: manual
+  by (fact transfer_morphismI)
+
+declare transfer_morphism_nat_int [transfer add
+  mode: manual
   return: nat_0_le
-  labels: natint
+  labels: nat_int
 ]
 
 text {* basic functions and relations *}
 
-lemma transfer_nat_int_numerals:
+lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
     "(0::nat) = nat 0"
     "(1::nat) = nat 1"
     "(2::nat) = nat 2"
     "(3::nat) = nat 3"
   by auto

   "tsub x y = (if x >= y then x - y else 0)"
 
 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   by (simp add: tsub_def)
 
-
-lemma transfer_nat_int_functions:
+lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
     "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
   by (auto simp add: eq_nat_nat_iff nat_mult_distrib
       nat_power_eq tsub_def)
 
-lemma transfer_nat_int_function_closures:
+lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
     "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
     "(0::int) >= 0"

     "(2::int) >= 0"
     "(3::int) >= 0"
     "int z >= 0"
   by (auto simp add: zero_le_mult_iff tsub_def)
 
-lemma transfer_nat_int_relations:
+lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) = nat y) = (x = y)"
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) < nat y) = (x < y)"
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) <= nat y) = (x <= y)"
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) dvd nat y) = (x dvd y)"
   by (auto simp add: zdvd_int)
-
-declare transfer_morphism_nat_int [transfer add return:
-  transfer_nat_int_numerals
-  transfer_nat_int_functions
-  transfer_nat_int_function_closures
-  transfer_nat_int_relations
-]
 
 
 text {* first-order quantifiers *}
 
 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"

 next
   assume "\<exists>x\<ge>0. P (nat x)"
   then show "\<exists>x. P x" by auto
 qed
 
-lemma transfer_nat_int_quantifiers:
+lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   by (rule all_nat, rule ex_nat)
 
 (* should we restrict these? *)

 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
     (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
   by auto
 
 declare transfer_morphism_nat_int [transfer add
-  return: transfer_nat_int_quantifiers
   cong: all_cong ex_cong]
 
 
 text {* if *}
 
-lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
-    nat (if P then x else y)"
-  by auto
-
-declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
+lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
+  "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
+  by auto
 
 
 text {* operations with sets *}
 
 definition

 
 subsection {* Set up transfer from int to nat *}
 
 text {* set up transfer direction *}
 
-lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
-  by (simp add: transfer_morphism_def)
+lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
+  by (fact transfer_morphismI)
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual
-(*  labels: int-nat *)
   return: nat_int
+  labels: int_nat
 ]
 
 
 text {* basic functions and relations *}
-
-lemma UNIV_apply:
-  "UNIV x = True"
-  by (simp add: top_fun_eq top_bool_eq)
 
 definition
   is_nat :: "int \<Rightarrow> bool"
 where
   "is_nat x = (x >= 0)"

 declare transfer_morphism_int_nat [transfer add return:
   transfer_int_nat_numerals
   transfer_int_nat_functions
   transfer_int_nat_function_closures
   transfer_int_nat_relations
-  UNIV_apply
 ]
 
 
 text {* first-order quantifiers *}