--- 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
]
--- 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]
--- 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]
--- 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]
--- 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]
--- 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]
--- 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]
--- 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]
--- 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:
--- 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
]
--- 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
]