# HG changeset patch
# User haftmann
# Date 1268037538 -3600
# Node ID d20cf282342e8a020192fe2682fe753df997c0af
# Parent  965c24dd685646107ffcde35c5d1247364882ee7
transfer: avoid camel case

diff -r 965c24dd6856 -r d20cf282342e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Divides.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -2326,7 +2326,7 @@
   apply auto
 done
 
-declare TransferMorphism_nat_int [transfer add return:
+declare transfer_morphism_nat_int [transfer add return:
   transfer_nat_int_functions
   transfer_nat_int_function_closures
 ]
@@ -2341,7 +2341,7 @@
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
 
-declare TransferMorphism_int_nat [transfer add return:
+declare transfer_morphism_int_nat [transfer add return:
   transfer_int_nat_functions
   transfer_int_nat_function_closures
 ]
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Fact.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -58,7 +58,7 @@
   "x >= (0::int) \<Longrightarrow> fact x >= 0"
   by (auto simp add: fact_int_def)
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
     transfer_nat_int_factorial transfer_nat_int_factorial_closure]
 
 lemma transfer_int_nat_factorial:
@@ -69,7 +69,7 @@
   "is_nat x \<Longrightarrow> fact x >= 0"
   by (auto simp add: fact_int_def)
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
     transfer_int_nat_factorial transfer_int_nat_factorial_closure]
 
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/GCD.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -99,7 +99,7 @@
   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   by (auto simp add: gcd_int_def lcm_int_def)
 
-declare TransferMorphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
 
 lemma transfer_int_nat_gcd:
@@ -112,7 +112,7 @@
   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   by (auto simp add: gcd_int_def lcm_int_def)
 
-declare TransferMorphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
 
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Nat_Transfer.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -10,8 +10,12 @@
 
 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"
 
@@ -22,10 +26,10 @@
 
 text {* set up transfer direction *}
 
-lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
-  by (simp add: TransferMorphism_def)
+lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
+  by (simp add: transfer_morphism_def)
 
-declare TransferMorphism_nat_int [transfer
+declare transfer_morphism_nat_int [transfer
   add mode: manual
   return: nat_0_le
   labels: natint
@@ -80,7 +84,7 @@
       (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
@@ -118,7 +122,7 @@
     (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]
 
@@ -129,7 +133,7 @@
     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 *}
@@ -190,7 +194,7 @@
     {(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
@@ -262,7 +266,7 @@
   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]
@@ -272,10 +276,10 @@
 
 text {* set up transfer direction *}
 
-lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
-  by (simp add: TransferMorphism_def)
+lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
+  by (simp add: transfer_morphism_def)
 
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
   mode: manual
 (*  labels: int-nat *)
   return: nat_int
@@ -326,7 +330,7 @@
     "(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
@@ -346,7 +350,7 @@
   apply auto
 done
 
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_quantifiers]
 
 
@@ -356,7 +360,7 @@
     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]
 
 
 
@@ -401,7 +405,7 @@
     {(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
@@ -433,7 +437,7 @@
   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]
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/Binomial.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -73,7 +73,7 @@
   "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
   by (auto simp add: binomial_int_def)
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
     transfer_nat_int_binomial transfer_nat_int_binomial_closure]
 
 lemma transfer_int_nat_binomial:
@@ -84,7 +84,7 @@
   "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
   by (auto simp add: binomial_int_def)
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
     transfer_int_nat_binomial transfer_int_nat_binomial_closure]
 
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -131,7 +131,7 @@
   apply assumption
 done
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
     transfer_nat_int_cong]
 
 lemma transfer_int_nat_cong:
@@ -140,7 +140,7 @@
   apply (auto simp add: zmod_int [symmetric])
 done
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
     transfer_int_nat_cong]
 
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/Fib.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -69,7 +69,7 @@
   "n >= (0::int) \<Longrightarrow> fib n >= 0"
   by (auto simp add: fib_int_def)
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
     transfer_nat_int_fib transfer_nat_int_fib_closure]
 
 lemma transfer_int_nat_fib:
@@ -80,7 +80,7 @@
   "is_nat n \<Longrightarrow> fib n >= 0"
   unfolding fib_int_def by auto
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
     transfer_int_nat_fib transfer_int_nat_fib_closure]
 
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/Primes.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -73,14 +73,14 @@
   unfolding gcd_int_def lcm_int_def prime_int_def
   by auto
 
-declare TransferMorphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
     transfer_nat_int_prime]
 
 lemma transfer_int_nat_prime:
   "prime (int x) = prime x"
   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
 
-declare TransferMorphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_prime]
 
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -295,7 +295,7 @@
   multiplicity (nat p) (nat n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
   transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
   transfer_nat_int_multiplicity]
 
@@ -312,7 +312,7 @@
     "multiplicity (int p) (int n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
   transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   transfer_int_nat_multiplicity]
 
@@ -636,7 +636,7 @@
   apply (rule setprod_nonneg, auto)
 done
 
-declare TransferMorphism_nat_int[transfer 
+declare transfer_morphism_nat_int[transfer 
   add return: transfer_nat_int_sum_prod_closure3
   del: transfer_nat_int_sum_prod2 (1)]
 
@@ -657,7 +657,7 @@
   apply auto
 done
 
-declare TransferMorphism_nat_int[transfer 
+declare transfer_morphism_nat_int[transfer 
   add return: transfer_nat_int_sum_prod2 (1)]
 
 lemma multiplicity_prod_prime_powers_nat:
diff -r 965c24dd6856 -r d20cf282342e src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Parity.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -32,7 +32,7 @@
   "even (int x) \<longleftrightarrow> even x"
   by (simp add: even_nat_def)
 
-declare TransferMorphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
   transfer_int_nat_relations
 ]
 
diff -r 965c24dd6856 -r d20cf282342e src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/SetInterval.thy	Mon Mar 08 09:38:58 2010 +0100
@@ -1228,7 +1228,7 @@
     "x >= 0 \<Longrightarrow> nat_set {x..y}"
   by (simp add: nat_set_def)
 
-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
 ]
@@ -1244,7 +1244,7 @@
     "is_nat x \<Longrightarrow> nat_set {x..y}"
   by (simp only: transfer_nat_int_set_function_closures is_nat_def)
 
-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
 ]