src/HOL/Nat_Transfer.thy
changeset 35644 d20cf282342e
parent 35551 85aada96578b
child 35683 70ace653fe77
     1.1 --- a/src/HOL/Nat_Transfer.thy	Sun Mar 07 17:33:01 2010 -0800
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Mon Mar 08 09:38:58 2010 +0100
     1.3 @@ -10,8 +10,12 @@
     1.4  
     1.5  subsection {* Generic transfer machinery *}
     1.6  
     1.7 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
     1.8 -  where "TransferMorphism a B \<longleftrightarrow> True"
     1.9 +definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    1.10 +  where "transfer_morphism f A \<longleftrightarrow> True"
    1.11 +
    1.12 +lemma transfer_morphismI:
    1.13 +  "transfer_morphism f A"
    1.14 +  by (simp add: transfer_morphism_def)
    1.15  
    1.16  use "Tools/transfer.ML"
    1.17  
    1.18 @@ -22,10 +26,10 @@
    1.19  
    1.20  text {* set up transfer direction *}
    1.21  
    1.22 -lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    1.23 -  by (simp add: TransferMorphism_def)
    1.24 +lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
    1.25 +  by (simp add: transfer_morphism_def)
    1.26  
    1.27 -declare TransferMorphism_nat_int [transfer
    1.28 +declare transfer_morphism_nat_int [transfer
    1.29    add mode: manual
    1.30    return: nat_0_le
    1.31    labels: natint
    1.32 @@ -80,7 +84,7 @@
    1.33        (nat (x::int) dvd nat y) = (x dvd y)"
    1.34    by (auto simp add: zdvd_int)
    1.35  
    1.36 -declare TransferMorphism_nat_int [transfer add return:
    1.37 +declare transfer_morphism_nat_int [transfer add return:
    1.38    transfer_nat_int_numerals
    1.39    transfer_nat_int_functions
    1.40    transfer_nat_int_function_closures
    1.41 @@ -118,7 +122,7 @@
    1.42      (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    1.43    by auto
    1.44  
    1.45 -declare TransferMorphism_nat_int [transfer add
    1.46 +declare transfer_morphism_nat_int [transfer add
    1.47    return: transfer_nat_int_quantifiers
    1.48    cong: all_cong ex_cong]
    1.49  
    1.50 @@ -129,7 +133,7 @@
    1.51      nat (if P then x else y)"
    1.52    by auto
    1.53  
    1.54 -declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
    1.55 +declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
    1.56  
    1.57  
    1.58  text {* operations with sets *}
    1.59 @@ -190,7 +194,7 @@
    1.60      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
    1.61    by auto
    1.62  
    1.63 -declare TransferMorphism_nat_int [transfer add
    1.64 +declare transfer_morphism_nat_int [transfer add
    1.65    return: transfer_nat_int_set_functions
    1.66      transfer_nat_int_set_function_closures
    1.67      transfer_nat_int_set_relations
    1.68 @@ -262,7 +266,7 @@
    1.69    apply (subst setprod_cong, assumption, auto)
    1.70  done
    1.71  
    1.72 -declare TransferMorphism_nat_int [transfer add
    1.73 +declare transfer_morphism_nat_int [transfer add
    1.74    return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
    1.75      transfer_nat_int_sum_prod_closure
    1.76    cong: transfer_nat_int_sum_prod_cong]
    1.77 @@ -272,10 +276,10 @@
    1.78  
    1.79  text {* set up transfer direction *}
    1.80  
    1.81 -lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
    1.82 -  by (simp add: TransferMorphism_def)
    1.83 +lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
    1.84 +  by (simp add: transfer_morphism_def)
    1.85  
    1.86 -declare TransferMorphism_int_nat [transfer add
    1.87 +declare transfer_morphism_int_nat [transfer add
    1.88    mode: manual
    1.89  (*  labels: int-nat *)
    1.90    return: nat_int
    1.91 @@ -326,7 +330,7 @@
    1.92      "(int x dvd int y) = (x dvd y)"
    1.93    by (auto simp add: zdvd_int)
    1.94  
    1.95 -declare TransferMorphism_int_nat [transfer add return:
    1.96 +declare transfer_morphism_int_nat [transfer add return:
    1.97    transfer_int_nat_numerals
    1.98    transfer_int_nat_functions
    1.99    transfer_int_nat_function_closures
   1.100 @@ -346,7 +350,7 @@
   1.101    apply auto
   1.102  done
   1.103  
   1.104 -declare TransferMorphism_int_nat [transfer add
   1.105 +declare transfer_morphism_int_nat [transfer add
   1.106    return: transfer_int_nat_quantifiers]
   1.107  
   1.108  
   1.109 @@ -356,7 +360,7 @@
   1.110      int (if P then x else y)"
   1.111    by auto
   1.112  
   1.113 -declare TransferMorphism_int_nat [transfer add return: int_if_cong]
   1.114 +declare transfer_morphism_int_nat [transfer add return: int_if_cong]
   1.115  
   1.116  
   1.117  
   1.118 @@ -401,7 +405,7 @@
   1.119      {(x::nat). P x} = {x. P' x}"
   1.120    by auto
   1.121  
   1.122 -declare TransferMorphism_int_nat [transfer add
   1.123 +declare transfer_morphism_int_nat [transfer add
   1.124    return: transfer_int_nat_set_functions
   1.125      transfer_int_nat_set_function_closures
   1.126      transfer_int_nat_set_relations
   1.127 @@ -433,7 +437,7 @@
   1.128    apply (subst int_setprod, auto simp add: cong: setprod_cong)
   1.129  done
   1.130  
   1.131 -declare TransferMorphism_int_nat [transfer add
   1.132 +declare transfer_morphism_int_nat [transfer add
   1.133    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   1.134    cong: setsum_cong setprod_cong]
   1.135