# HG changeset patch
# User haftmann
# Date 1268916993 -3600
# Node ID ee34f03a7d2667a89c4ddc298adfb322bc3528b0
# Parent  b57c3afd14841edfebb5fadac16bc57e8bdae896
meaningful transfer certificate

diff -r b57c3afd1484 -r ee34f03a7d26 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:56:33 2010 +0100
+++ b/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:56:33 2010 +0100
@@ -10,12 +10,13 @@
 
 subsection {* Generic transfer machinery *}
 
-definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
-  where "transfer_morphism f A \<longleftrightarrow> True"
+definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
+  where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
 
 lemma transfer_morphismI:
-  "transfer_morphism f A"
-  by (simp add: transfer_morphism_def)
+  assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
+  shows "transfer_morphism f A"
+  using assms by (auto simp add: transfer_morphism_def)
 
 use "Tools/transfer.ML"
 
@@ -27,7 +28,7 @@
 text {* set up transfer direction *}
 
 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
-  by (fact transfer_morphismI)
+  by (rule transfer_morphismI) simp
 
 declare transfer_morphism_nat_int [transfer add
   mode: manual
@@ -266,7 +267,7 @@
 text {* set up transfer direction *}
 
 lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
-  by (fact transfer_morphismI)
+by (rule transfer_morphismI) simp
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual
diff -r b57c3afd1484 -r ee34f03a7d26 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Thu Mar 18 13:56:33 2010 +0100
+++ b/src/HOL/Tools/transfer.ML	Thu Mar 18 13:56:33 2010 +0100
@@ -23,11 +23,13 @@
 
 val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of;
 
+val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI});
+
 fun check_morphism_key ctxt key =
   let
-    val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key)
-      handle Pattern.MATCH => error
-        ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI}));
+    val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key)
+      handle Pattern.MATCH => error ("Transfer: expected theorem of the form "
+        ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key)));
   in direction_of key end;
 
 type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,