transfer: avoid camel case
authorhaftmann
Mon Mar 08 09:38:58 2010 +0100 (2010-03-08)
changeset 35644d20cf282342e
parent 35643 965c24dd6856
child 35645 74e4542d0a4a
transfer: avoid camel case
src/HOL/Divides.thy
src/HOL/Fact.thy
src/HOL/GCD.thy
src/HOL/Nat_Transfer.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Parity.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Mar 07 17:33:01 2010 -0800
     1.2 +++ b/src/HOL/Divides.thy	Mon Mar 08 09:38:58 2010 +0100
     1.3 @@ -2326,7 +2326,7 @@
     1.4    apply auto
     1.5  done
     1.6  
     1.7 -declare TransferMorphism_nat_int [transfer add return:
     1.8 +declare transfer_morphism_nat_int [transfer add return:
     1.9    transfer_nat_int_functions
    1.10    transfer_nat_int_function_closures
    1.11  ]
    1.12 @@ -2341,7 +2341,7 @@
    1.13      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
    1.14    by (simp_all only: is_nat_def transfer_nat_int_function_closures)
    1.15  
    1.16 -declare TransferMorphism_int_nat [transfer add return:
    1.17 +declare transfer_morphism_int_nat [transfer add return:
    1.18    transfer_int_nat_functions
    1.19    transfer_int_nat_function_closures
    1.20  ]
     2.1 --- a/src/HOL/Fact.thy	Sun Mar 07 17:33:01 2010 -0800
     2.2 +++ b/src/HOL/Fact.thy	Mon Mar 08 09:38:58 2010 +0100
     2.3 @@ -58,7 +58,7 @@
     2.4    "x >= (0::int) \<Longrightarrow> fact x >= 0"
     2.5    by (auto simp add: fact_int_def)
     2.6  
     2.7 -declare TransferMorphism_nat_int[transfer add return: 
     2.8 +declare transfer_morphism_nat_int[transfer add return: 
     2.9      transfer_nat_int_factorial transfer_nat_int_factorial_closure]
    2.10  
    2.11  lemma transfer_int_nat_factorial:
    2.12 @@ -69,7 +69,7 @@
    2.13    "is_nat x \<Longrightarrow> fact x >= 0"
    2.14    by (auto simp add: fact_int_def)
    2.15  
    2.16 -declare TransferMorphism_int_nat[transfer add return: 
    2.17 +declare transfer_morphism_int_nat[transfer add return: 
    2.18      transfer_int_nat_factorial transfer_int_nat_factorial_closure]
    2.19  
    2.20  
     3.1 --- a/src/HOL/GCD.thy	Sun Mar 07 17:33:01 2010 -0800
     3.2 +++ b/src/HOL/GCD.thy	Mon Mar 08 09:38:58 2010 +0100
     3.3 @@ -99,7 +99,7 @@
     3.4    "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
     3.5    by (auto simp add: gcd_int_def lcm_int_def)
     3.6  
     3.7 -declare TransferMorphism_nat_int[transfer add return:
     3.8 +declare transfer_morphism_nat_int[transfer add return:
     3.9      transfer_nat_int_gcd transfer_nat_int_gcd_closures]
    3.10  
    3.11  lemma transfer_int_nat_gcd:
    3.12 @@ -112,7 +112,7 @@
    3.13    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
    3.14    by (auto simp add: gcd_int_def lcm_int_def)
    3.15  
    3.16 -declare TransferMorphism_int_nat[transfer add return:
    3.17 +declare transfer_morphism_int_nat[transfer add return:
    3.18      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
    3.19  
    3.20  
     4.1 --- a/src/HOL/Nat_Transfer.thy	Sun Mar 07 17:33:01 2010 -0800
     4.2 +++ b/src/HOL/Nat_Transfer.thy	Mon Mar 08 09:38:58 2010 +0100
     4.3 @@ -10,8 +10,12 @@
     4.4  
     4.5  subsection {* Generic transfer machinery *}
     4.6  
     4.7 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
     4.8 -  where "TransferMorphism a B \<longleftrightarrow> True"
     4.9 +definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    4.10 +  where "transfer_morphism f A \<longleftrightarrow> True"
    4.11 +
    4.12 +lemma transfer_morphismI:
    4.13 +  "transfer_morphism f A"
    4.14 +  by (simp add: transfer_morphism_def)
    4.15  
    4.16  use "Tools/transfer.ML"
    4.17  
    4.18 @@ -22,10 +26,10 @@
    4.19  
    4.20  text {* set up transfer direction *}
    4.21  
    4.22 -lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    4.23 -  by (simp add: TransferMorphism_def)
    4.24 +lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
    4.25 +  by (simp add: transfer_morphism_def)
    4.26  
    4.27 -declare TransferMorphism_nat_int [transfer
    4.28 +declare transfer_morphism_nat_int [transfer
    4.29    add mode: manual
    4.30    return: nat_0_le
    4.31    labels: natint
    4.32 @@ -80,7 +84,7 @@
    4.33        (nat (x::int) dvd nat y) = (x dvd y)"
    4.34    by (auto simp add: zdvd_int)
    4.35  
    4.36 -declare TransferMorphism_nat_int [transfer add return:
    4.37 +declare transfer_morphism_nat_int [transfer add return:
    4.38    transfer_nat_int_numerals
    4.39    transfer_nat_int_functions
    4.40    transfer_nat_int_function_closures
    4.41 @@ -118,7 +122,7 @@
    4.42      (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    4.43    by auto
    4.44  
    4.45 -declare TransferMorphism_nat_int [transfer add
    4.46 +declare transfer_morphism_nat_int [transfer add
    4.47    return: transfer_nat_int_quantifiers
    4.48    cong: all_cong ex_cong]
    4.49  
    4.50 @@ -129,7 +133,7 @@
    4.51      nat (if P then x else y)"
    4.52    by auto
    4.53  
    4.54 -declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
    4.55 +declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
    4.56  
    4.57  
    4.58  text {* operations with sets *}
    4.59 @@ -190,7 +194,7 @@
    4.60      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
    4.61    by auto
    4.62  
    4.63 -declare TransferMorphism_nat_int [transfer add
    4.64 +declare transfer_morphism_nat_int [transfer add
    4.65    return: transfer_nat_int_set_functions
    4.66      transfer_nat_int_set_function_closures
    4.67      transfer_nat_int_set_relations
    4.68 @@ -262,7 +266,7 @@
    4.69    apply (subst setprod_cong, assumption, auto)
    4.70  done
    4.71  
    4.72 -declare TransferMorphism_nat_int [transfer add
    4.73 +declare transfer_morphism_nat_int [transfer add
    4.74    return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
    4.75      transfer_nat_int_sum_prod_closure
    4.76    cong: transfer_nat_int_sum_prod_cong]
    4.77 @@ -272,10 +276,10 @@
    4.78  
    4.79  text {* set up transfer direction *}
    4.80  
    4.81 -lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
    4.82 -  by (simp add: TransferMorphism_def)
    4.83 +lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
    4.84 +  by (simp add: transfer_morphism_def)
    4.85  
    4.86 -declare TransferMorphism_int_nat [transfer add
    4.87 +declare transfer_morphism_int_nat [transfer add
    4.88    mode: manual
    4.89  (*  labels: int-nat *)
    4.90    return: nat_int
    4.91 @@ -326,7 +330,7 @@
    4.92      "(int x dvd int y) = (x dvd y)"
    4.93    by (auto simp add: zdvd_int)
    4.94  
    4.95 -declare TransferMorphism_int_nat [transfer add return:
    4.96 +declare transfer_morphism_int_nat [transfer add return:
    4.97    transfer_int_nat_numerals
    4.98    transfer_int_nat_functions
    4.99    transfer_int_nat_function_closures
   4.100 @@ -346,7 +350,7 @@
   4.101    apply auto
   4.102  done
   4.103  
   4.104 -declare TransferMorphism_int_nat [transfer add
   4.105 +declare transfer_morphism_int_nat [transfer add
   4.106    return: transfer_int_nat_quantifiers]
   4.107  
   4.108  
   4.109 @@ -356,7 +360,7 @@
   4.110      int (if P then x else y)"
   4.111    by auto
   4.112  
   4.113 -declare TransferMorphism_int_nat [transfer add return: int_if_cong]
   4.114 +declare transfer_morphism_int_nat [transfer add return: int_if_cong]
   4.115  
   4.116  
   4.117  
   4.118 @@ -401,7 +405,7 @@
   4.119      {(x::nat). P x} = {x. P' x}"
   4.120    by auto
   4.121  
   4.122 -declare TransferMorphism_int_nat [transfer add
   4.123 +declare transfer_morphism_int_nat [transfer add
   4.124    return: transfer_int_nat_set_functions
   4.125      transfer_int_nat_set_function_closures
   4.126      transfer_int_nat_set_relations
   4.127 @@ -433,7 +437,7 @@
   4.128    apply (subst int_setprod, auto simp add: cong: setprod_cong)
   4.129  done
   4.130  
   4.131 -declare TransferMorphism_int_nat [transfer add
   4.132 +declare transfer_morphism_int_nat [transfer add
   4.133    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   4.134    cong: setsum_cong setprod_cong]
   4.135  
     5.1 --- a/src/HOL/Number_Theory/Binomial.thy	Sun Mar 07 17:33:01 2010 -0800
     5.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Mon Mar 08 09:38:58 2010 +0100
     5.3 @@ -73,7 +73,7 @@
     5.4    "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
     5.5    by (auto simp add: binomial_int_def)
     5.6  
     5.7 -declare TransferMorphism_nat_int[transfer add return: 
     5.8 +declare transfer_morphism_nat_int[transfer add return: 
     5.9      transfer_nat_int_binomial transfer_nat_int_binomial_closure]
    5.10  
    5.11  lemma transfer_int_nat_binomial:
    5.12 @@ -84,7 +84,7 @@
    5.13    "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
    5.14    by (auto simp add: binomial_int_def)
    5.15  
    5.16 -declare TransferMorphism_int_nat[transfer add return: 
    5.17 +declare transfer_morphism_int_nat[transfer add return: 
    5.18      transfer_int_nat_binomial transfer_int_nat_binomial_closure]
    5.19  
    5.20  
     6.1 --- a/src/HOL/Number_Theory/Cong.thy	Sun Mar 07 17:33:01 2010 -0800
     6.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Mar 08 09:38:58 2010 +0100
     6.3 @@ -131,7 +131,7 @@
     6.4    apply assumption
     6.5  done
     6.6  
     6.7 -declare TransferMorphism_nat_int[transfer add return: 
     6.8 +declare transfer_morphism_nat_int[transfer add return: 
     6.9      transfer_nat_int_cong]
    6.10  
    6.11  lemma transfer_int_nat_cong:
    6.12 @@ -140,7 +140,7 @@
    6.13    apply (auto simp add: zmod_int [symmetric])
    6.14  done
    6.15  
    6.16 -declare TransferMorphism_int_nat[transfer add return: 
    6.17 +declare transfer_morphism_int_nat[transfer add return: 
    6.18      transfer_int_nat_cong]
    6.19  
    6.20  
     7.1 --- a/src/HOL/Number_Theory/Fib.thy	Sun Mar 07 17:33:01 2010 -0800
     7.2 +++ b/src/HOL/Number_Theory/Fib.thy	Mon Mar 08 09:38:58 2010 +0100
     7.3 @@ -69,7 +69,7 @@
     7.4    "n >= (0::int) \<Longrightarrow> fib n >= 0"
     7.5    by (auto simp add: fib_int_def)
     7.6  
     7.7 -declare TransferMorphism_nat_int[transfer add return: 
     7.8 +declare transfer_morphism_nat_int[transfer add return: 
     7.9      transfer_nat_int_fib transfer_nat_int_fib_closure]
    7.10  
    7.11  lemma transfer_int_nat_fib:
    7.12 @@ -80,7 +80,7 @@
    7.13    "is_nat n \<Longrightarrow> fib n >= 0"
    7.14    unfolding fib_int_def by auto
    7.15  
    7.16 -declare TransferMorphism_int_nat[transfer add return: 
    7.17 +declare transfer_morphism_int_nat[transfer add return: 
    7.18      transfer_int_nat_fib transfer_int_nat_fib_closure]
    7.19  
    7.20  
     8.1 --- a/src/HOL/Number_Theory/Primes.thy	Sun Mar 07 17:33:01 2010 -0800
     8.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Mar 08 09:38:58 2010 +0100
     8.3 @@ -73,14 +73,14 @@
     8.4    unfolding gcd_int_def lcm_int_def prime_int_def
     8.5    by auto
     8.6  
     8.7 -declare TransferMorphism_nat_int[transfer add return:
     8.8 +declare transfer_morphism_nat_int[transfer add return:
     8.9      transfer_nat_int_prime]
    8.10  
    8.11  lemma transfer_int_nat_prime:
    8.12    "prime (int x) = prime x"
    8.13    by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
    8.14  
    8.15 -declare TransferMorphism_int_nat[transfer add return:
    8.16 +declare transfer_morphism_int_nat[transfer add return:
    8.17      transfer_int_nat_prime]
    8.18  
    8.19  
     9.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Mar 07 17:33:01 2010 -0800
     9.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Mar 08 09:38:58 2010 +0100
     9.3 @@ -295,7 +295,7 @@
     9.4    multiplicity (nat p) (nat n) = multiplicity p n"
     9.5    by (auto simp add: multiplicity_int_def)
     9.6  
     9.7 -declare TransferMorphism_nat_int[transfer add return: 
     9.8 +declare transfer_morphism_nat_int[transfer add return: 
     9.9    transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
    9.10    transfer_nat_int_multiplicity]
    9.11  
    9.12 @@ -312,7 +312,7 @@
    9.13      "multiplicity (int p) (int n) = multiplicity p n"
    9.14    by (auto simp add: multiplicity_int_def)
    9.15  
    9.16 -declare TransferMorphism_int_nat[transfer add return: 
    9.17 +declare transfer_morphism_int_nat[transfer add return: 
    9.18    transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
    9.19    transfer_int_nat_multiplicity]
    9.20  
    9.21 @@ -636,7 +636,7 @@
    9.22    apply (rule setprod_nonneg, auto)
    9.23  done
    9.24  
    9.25 -declare TransferMorphism_nat_int[transfer 
    9.26 +declare transfer_morphism_nat_int[transfer 
    9.27    add return: transfer_nat_int_sum_prod_closure3
    9.28    del: transfer_nat_int_sum_prod2 (1)]
    9.29  
    9.30 @@ -657,7 +657,7 @@
    9.31    apply auto
    9.32  done
    9.33  
    9.34 -declare TransferMorphism_nat_int[transfer 
    9.35 +declare transfer_morphism_nat_int[transfer 
    9.36    add return: transfer_nat_int_sum_prod2 (1)]
    9.37  
    9.38  lemma multiplicity_prod_prime_powers_nat:
    10.1 --- a/src/HOL/Parity.thy	Sun Mar 07 17:33:01 2010 -0800
    10.2 +++ b/src/HOL/Parity.thy	Mon Mar 08 09:38:58 2010 +0100
    10.3 @@ -32,7 +32,7 @@
    10.4    "even (int x) \<longleftrightarrow> even x"
    10.5    by (simp add: even_nat_def)
    10.6  
    10.7 -declare TransferMorphism_int_nat[transfer add return:
    10.8 +declare transfer_morphism_int_nat[transfer add return:
    10.9    transfer_int_nat_relations
   10.10  ]
   10.11  
    11.1 --- a/src/HOL/SetInterval.thy	Sun Mar 07 17:33:01 2010 -0800
    11.2 +++ b/src/HOL/SetInterval.thy	Mon Mar 08 09:38:58 2010 +0100
    11.3 @@ -1228,7 +1228,7 @@
    11.4      "x >= 0 \<Longrightarrow> nat_set {x..y}"
    11.5    by (simp add: nat_set_def)
    11.6  
    11.7 -declare TransferMorphism_nat_int[transfer add
    11.8 +declare transfer_morphism_nat_int[transfer add
    11.9    return: transfer_nat_int_set_functions
   11.10      transfer_nat_int_set_function_closures
   11.11  ]
   11.12 @@ -1244,7 +1244,7 @@
   11.13      "is_nat x \<Longrightarrow> nat_set {x..y}"
   11.14    by (simp only: transfer_nat_int_set_function_closures is_nat_def)
   11.15  
   11.16 -declare TransferMorphism_int_nat[transfer add
   11.17 +declare transfer_morphism_int_nat[transfer add
   11.18    return: transfer_int_nat_set_functions
   11.19      transfer_int_nat_set_function_closures
   11.20  ]