# HG changeset patch
# User haftmann
# Date 1268165988 -3600
# Node ID 70ace653fe77a0bf62f185056314485a27cb471a
# Parent  b6720fe8afa795004e3b282b0e42dd7e40c7c4c6
misc tuning

diff -r b6720fe8afa7 -r 70ace653fe77 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Tue Mar 09 18:33:01 2010 +0100
+++ b/src/HOL/Nat_Transfer.thy	Tue Mar 09 21:19:48 2010 +0100
@@ -27,17 +27,17 @@
 text {* set up transfer direction *}
 
 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
-  by (simp add: transfer_morphism_def)
+  by (fact transfer_morphismI)
 
-declare transfer_morphism_nat_int [transfer
-  add mode: manual
+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"
@@ -52,8 +52,7 @@
 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)"
@@ -61,7 +60,7 @@
   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"
@@ -73,7 +72,7 @@
     "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>
@@ -84,13 +83,6 @@
       (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 *}
 
@@ -108,7 +100,7 @@
   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)
@@ -123,18 +115,15 @@
   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)"
+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
 
-declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
-
 
 text {* operations with sets *}
 
@@ -276,22 +265,18 @@
 
 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
@@ -335,7 +320,6 @@
   transfer_int_nat_functions
   transfer_int_nat_function_closures
   transfer_int_nat_relations
-  UNIV_apply
 ]