src/HOL/Nat_Transfer.thy
 changeset 35821 ee34f03a7d26 parent 35683 70ace653fe77 child 39198 f967a16dfcdd
```     1.1 --- a/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:56:33 2010 +0100
1.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Mar 18 13:56:33 2010 +0100
1.3 @@ -10,12 +10,13 @@
1.4
1.5  subsection {* Generic transfer machinery *}
1.6
1.7 -definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
1.8 -  where "transfer_morphism f A \<longleftrightarrow> True"
1.9 +definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
1.10 +  where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
1.11
1.12  lemma transfer_morphismI:
1.13 -  "transfer_morphism f A"
1.14 -  by (simp add: transfer_morphism_def)
1.15 +  assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
1.16 +  shows "transfer_morphism f A"
1.17 +  using assms by (auto simp add: transfer_morphism_def)
1.18
1.19  use "Tools/transfer.ML"
1.20
1.21 @@ -27,7 +28,7 @@
1.22  text {* set up transfer direction *}
1.23
1.24  lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
1.25 -  by (fact transfer_morphismI)
1.26 +  by (rule transfer_morphismI) simp
1.27