src/HOL/Nat_Transfer.thy
changeset 42870 36abaf4cce1f
parent 39302 d7728f65b353
child 47255 30a1692557b0
     1.1 --- a/src/HOL/Nat_Transfer.thy	Fri May 20 08:16:56 2011 +0200
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Fri May 20 09:31:36 2011 +0200
     1.3 @@ -11,12 +11,10 @@
     1.4  subsection {* Generic transfer machinery *}
     1.5  
     1.6  definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
     1.7 -  where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
     1.8 +  where "transfer_morphism f A \<longleftrightarrow> True"
     1.9  
    1.10 -lemma transfer_morphismI:
    1.11 -  assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
    1.12 -  shows "transfer_morphism f A"
    1.13 -  using assms by (auto simp add: transfer_morphism_def)
    1.14 +lemma transfer_morphismI[intro]: "transfer_morphism f A"
    1.15 +  by (simp add: transfer_morphism_def)
    1.16  
    1.17  use "Tools/transfer.ML"
    1.18  
    1.19 @@ -27,8 +25,7 @@
    1.20  
    1.21  text {* set up transfer direction *}
    1.22  
    1.23 -lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
    1.24 -  by (rule transfer_morphismI) simp
    1.25 +lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
    1.26  
    1.27  declare transfer_morphism_nat_int [transfer add
    1.28    mode: manual
    1.29 @@ -266,8 +263,7 @@
    1.30  
    1.31  text {* set up transfer direction *}
    1.32  
    1.33 -lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
    1.34 -by (rule transfer_morphismI) simp
    1.35 +lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
    1.36  
    1.37  declare transfer_morphism_int_nat [transfer add
    1.38    mode: manual