src/HOL/Nat_Transfer.thy

 uses ("Tools/transfer.ML")
 begin
 
 subsection {* Generic transfer machinery *}
 
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
-  where "TransferMorphism a B \<longleftrightarrow> True"
+definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+  where "transfer_morphism f A \<longleftrightarrow> True"
+
+lemma transfer_morphismI:
+  "transfer_morphism f A"
+  by (simp add: transfer_morphism_def)
 
 use "Tools/transfer.ML"
 
 setup Transfer.setup
 
 
 subsection {* Set up transfer from nat to int *}
 
 text {* set up transfer direction *}
 
-lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
-  by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_nat_int [transfer
+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
   return: nat_0_le
   labels: natint
 ]
 

       (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 TransferMorphism_nat_int [transfer add return:
+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
 ]

 
 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 TransferMorphism_nat_int [transfer add
+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 TransferMorphism_nat_int [transfer add return: nat_if_cong]
+declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
 
 
 text {* operations with sets *}
 
 definition

 
 lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
     {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   by auto
 
-declare TransferMorphism_nat_int [transfer add
+declare transfer_morphism_nat_int [transfer add
   return: transfer_nat_int_set_functions
     transfer_nat_int_set_function_closures
     transfer_nat_int_set_relations
     transfer_nat_int_set_return_embed
   cong: transfer_nat_int_set_cong

   apply (subst setsum_cong, assumption)
   apply auto [2]
   apply (subst setprod_cong, assumption, auto)
 done
 
-declare TransferMorphism_nat_int [transfer add
+declare transfer_morphism_nat_int [transfer add
   return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
     transfer_nat_int_sum_prod_closure
   cong: transfer_nat_int_sum_prod_cong]
 
 
 subsection {* Set up transfer from int to nat *}
 
 text {* set up transfer direction *}
 
-lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
-  by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_int_nat [transfer add
+lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
+  by (simp add: transfer_morphism_def)
+
+declare transfer_morphism_int_nat [transfer add
   mode: manual
 (*  labels: int-nat *)
   return: nat_int
 ]
 

     "(int x < int y) = (x < y)"
     "(int x <= int y) = (x <= y)"
     "(int x dvd int y) = (x dvd y)"
   by (auto simp add: zdvd_int)
 
-declare TransferMorphism_int_nat [transfer add return:
+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

   apply auto [1]
   apply (subst ex_nat)
   apply auto
 done
 
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_quantifiers]
 
 
 text {* if *}
 
 lemma int_if_cong: "(if P then (int x) else (int y)) =
     int (if P then x else y)"
   by auto
 
-declare TransferMorphism_int_nat [transfer add return: int_if_cong]
+declare transfer_morphism_int_nat [transfer add return: int_if_cong]
 
 
 
 text {* operations with sets *}
 

 
 lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
     {(x::nat). P x} = {x. P' x}"
   by auto
 
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_set_functions
     transfer_int_nat_set_function_closures
     transfer_int_nat_set_relations
     transfer_int_nat_set_return_embed
   cong: transfer_int_nat_set_cong

   unfolding is_nat_def
   apply (subst int_setsum, auto)
   apply (subst int_setprod, auto simp add: cong: setprod_cong)
 done
 
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   cong: setsum_cong setprod_cong]
 
 end