removed ancient nat-int transfer
authorhaftmann
Tue Oct 31 07:11:03 2017 +0000 (19 months ago)
changeset 669540230af0f3c59
parent 66953 826a5fd4d36c
child 66955 289f390c4e57
removed ancient nat-int transfer
NEWS
src/HOL/Decision_Procs/Conversions.thy
src/HOL/Main.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nat_Transfer.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/ROOT
src/HOL/ex/Transfer_Ex.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Mon Oct 30 19:29:06 2017 +0000
     1.2 +++ b/NEWS	Tue Oct 31 07:11:03 2017 +0000
     1.3 @@ -66,6 +66,8 @@
     1.4  * Class linordered_semiring_1 covers zero_less_one also, ruling out
     1.5  pathologic instances. Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Removed nat-int transfer machinery.  Rare INCOMPATIBILITY.
     1.8 +
     1.9  
    1.10  *** System ***
    1.11  
     2.1 --- a/src/HOL/Decision_Procs/Conversions.thy	Mon Oct 30 19:29:06 2017 +0000
     2.2 +++ b/src/HOL/Decision_Procs/Conversions.thy	Tue Oct 31 07:11:03 2017 +0000
     2.3 @@ -93,7 +93,7 @@
     2.4  ML \<open>
     2.5  fun nat_conv i = (case strip_app i of
     2.6      (@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
     2.7 -  | (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
     2.8 +  | (@{const_name one_class.one}, []) => @{thm nat_one_as_int [meta, symmetric]}
     2.9    | (@{const_name numeral}, [b]) => inst [] [b] @{thm nat_numeral [meta]}
    2.10    | (@{const_name uminus}, [b]) => (case strip_app b of
    2.11        (@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
     3.1 --- a/src/HOL/Main.thy	Mon Oct 30 19:29:06 2017 +0000
     3.2 +++ b/src/HOL/Main.thy	Tue Oct 31 07:11:03 2017 +0000
     3.3 @@ -15,7 +15,6 @@
     3.4      Conditionally_Complete_Lattices
     3.5      Binomial
     3.6      GCD
     3.7 -    Nat_Transfer
     3.8  begin
     3.9  
    3.10  text \<open>
     4.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Oct 30 19:29:06 2017 +0000
     4.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 31 07:11:03 2017 +0000
     4.3 @@ -268,7 +268,6 @@
     4.4   @{const_name Meson.skolem},
     4.5   @{const_name ATP.fequal},
     4.6   @{const_name ATP.fEx},
     4.7 - @{const_name transfer_morphism},
     4.8   @{const_name enum_prod_inst.enum_all_prod},
     4.9   @{const_name enum_prod_inst.enum_ex_prod},
    4.10   @{const_name Quickcheck_Random.catch_match},
     5.1 --- a/src/HOL/Nat_Transfer.thy	Mon Oct 30 19:29:06 2017 +0000
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,464 +0,0 @@
     5.4 -(* Authors: Jeremy Avigad and Amine Chaieb *)
     5.5 -
     5.6 -section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
     5.7 -
     5.8 -theory Nat_Transfer
     5.9 -imports List GCD
    5.10 -begin
    5.11 -
    5.12 -subsection \<open>Generic transfer machinery\<close>
    5.13 -
    5.14 -definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
    5.15 -  where "transfer_morphism f A \<longleftrightarrow> True"
    5.16 -
    5.17 -lemma transfer_morphismI[intro]: "transfer_morphism f A"
    5.18 -  by (simp add: transfer_morphism_def)
    5.19 -
    5.20 -ML_file "Tools/legacy_transfer.ML"
    5.21 -
    5.22 -
    5.23 -subsection \<open>Set up transfer from nat to int\<close>
    5.24 -
    5.25 -text \<open>set up transfer direction\<close>
    5.26 -
    5.27 -lemma transfer_morphism_nat_int [no_atp]:
    5.28 -  "transfer_morphism nat (op <= (0::int))" ..
    5.29 -
    5.30 -declare transfer_morphism_nat_int [transfer add
    5.31 -  mode: manual
    5.32 -  return: nat_0_le
    5.33 -  labels: nat_int
    5.34 -]
    5.35 -
    5.36 -text \<open>basic functions and relations\<close>
    5.37 -
    5.38 -lemma transfer_nat_int_numerals [no_atp, transfer key: transfer_morphism_nat_int]:
    5.39 -    "(0::nat) = nat 0"
    5.40 -    "(1::nat) = nat 1"
    5.41 -    "(2::nat) = nat 2"
    5.42 -    "(3::nat) = nat 3"
    5.43 -  by auto
    5.44 -
    5.45 -definition
    5.46 -  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
    5.47 -where
    5.48 -  "tsub x y = (if x >= y then x - y else 0)"
    5.49 -
    5.50 -lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
    5.51 -  by (simp add: tsub_def)
    5.52 -
    5.53 -lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]:
    5.54 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
    5.55 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    5.56 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    5.57 -    "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    5.58 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    5.59 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    5.60 -  by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    5.61 -      nat_power_eq tsub_def nat_div_distrib nat_mod_distrib)
    5.62 -
    5.63 -lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]:
    5.64 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    5.65 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    5.66 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    5.67 -    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
    5.68 -    "(0::int) >= 0"
    5.69 -    "(1::int) >= 0"
    5.70 -    "(2::int) >= 0"
    5.71 -    "(3::int) >= 0"
    5.72 -    "int z >= 0"
    5.73 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    5.74 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    5.75 -            apply (auto simp add: zero_le_mult_iff tsub_def pos_imp_zdiv_nonneg_iff)
    5.76 -   apply (cases "y = 0")
    5.77 -    apply (auto simp add: pos_imp_zdiv_nonneg_iff)
    5.78 -  apply (cases "y = 0")
    5.79 -   apply auto
    5.80 -  done
    5.81 -
    5.82 -lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]:
    5.83 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    5.84 -      (nat (x::int) = nat y) = (x = y)"
    5.85 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    5.86 -      (nat (x::int) < nat y) = (x < y)"
    5.87 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    5.88 -      (nat (x::int) <= nat y) = (x <= y)"
    5.89 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    5.90 -      (nat (x::int) dvd nat y) = (x dvd y)"
    5.91 -  by (auto simp add: zdvd_int)
    5.92 -
    5.93 -
    5.94 -text \<open>first-order quantifiers\<close>
    5.95 -
    5.96 -lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
    5.97 -    "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    5.98 -    "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
    5.99 -  by (rule all_nat, rule ex_nat)
   5.100 -
   5.101 -declare transfer_morphism_nat_int [transfer add
   5.102 -  cong: all_cong ex_cong]
   5.103 -
   5.104 -
   5.105 -text \<open>if\<close>
   5.106 -
   5.107 -lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
   5.108 -  "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
   5.109 -  by auto
   5.110 -
   5.111 -
   5.112 -text \<open>operations with sets\<close>
   5.113 -
   5.114 -definition
   5.115 -  nat_set :: "int set \<Rightarrow> bool"
   5.116 -where
   5.117 -  "nat_set S = (ALL x:S. x >= 0)"
   5.118 -
   5.119 -lemma transfer_nat_int_set_functions [no_atp]:
   5.120 -    "card A = card (int ` A)"
   5.121 -    "{} = nat ` ({}::int set)"
   5.122 -    "A Un B = nat ` (int ` A Un int ` B)"
   5.123 -    "A Int B = nat ` (int ` A Int int ` B)"
   5.124 -    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
   5.125 -    "{..n} = nat ` {0..int n}"
   5.126 -    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   5.127 -  by (rule card_image [symmetric])
   5.128 -    (auto simp add: inj_on_def image_def intro: bexI [of _ "int x" for x] exI [of _ "int x" for x])
   5.129 -
   5.130 -lemma transfer_nat_int_set_function_closures [no_atp]:
   5.131 -    "nat_set {}"
   5.132 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   5.133 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   5.134 -    "nat_set {x. x >= 0 & P x}"
   5.135 -    "nat_set (int ` C)"
   5.136 -    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
   5.137 -    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   5.138 -  unfolding nat_set_def apply auto
   5.139 -done
   5.140 -
   5.141 -lemma transfer_nat_int_set_relations [no_atp]:
   5.142 -    "(finite A) = (finite (int ` A))"
   5.143 -    "(x : A) = (int x : int ` A)"
   5.144 -    "(A = B) = (int ` A = int ` B)"
   5.145 -    "(A < B) = (int ` A < int ` B)"
   5.146 -    "(A <= B) = (int ` A <= int ` B)"
   5.147 -  apply (rule iffI)
   5.148 -  apply (erule finite_imageI)
   5.149 -  apply (erule finite_imageD)
   5.150 -  apply (auto simp add: image_def set_eq_iff inj_on_def)
   5.151 -  apply (drule_tac x = "int x" in spec, auto)
   5.152 -  apply (drule_tac x = "int x" in spec, auto)
   5.153 -  apply (drule_tac x = "int x" in spec, auto)
   5.154 -done
   5.155 -
   5.156 -lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \<Longrightarrow>
   5.157 -    (int ` nat ` A = A)"
   5.158 -  by (auto simp add: nat_set_def image_def)
   5.159 -
   5.160 -lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
   5.161 -    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   5.162 -  by auto
   5.163 -
   5.164 -declare transfer_morphism_nat_int [transfer add
   5.165 -  return: transfer_nat_int_set_functions
   5.166 -    transfer_nat_int_set_function_closures
   5.167 -    transfer_nat_int_set_relations
   5.168 -    transfer_nat_int_set_return_embed
   5.169 -  cong: transfer_nat_int_set_cong
   5.170 -]
   5.171 -
   5.172 -
   5.173 -text \<open>sum and prod\<close>
   5.174 -
   5.175 -(* this handles the case where the *domain* of f is nat *)
   5.176 -lemma transfer_nat_int_sum_prod [no_atp]:
   5.177 -    "sum f A = sum (%x. f (nat x)) (int ` A)"
   5.178 -    "prod f A = prod (%x. f (nat x)) (int ` A)"
   5.179 -  apply (subst sum.reindex)
   5.180 -  apply (unfold inj_on_def, auto)
   5.181 -  apply (subst prod.reindex)
   5.182 -  apply (unfold inj_on_def o_def, auto)
   5.183 -done
   5.184 -
   5.185 -(* this handles the case where the *range* of f is nat *)
   5.186 -lemma transfer_nat_int_sum_prod2 [no_atp]:
   5.187 -    "sum f A = nat(sum (%x. int (f x)) A)"
   5.188 -    "prod f A = nat(prod (%x. int (f x)) A)"
   5.189 -  apply (simp only: int_sum [symmetric] nat_int)
   5.190 -  apply (simp only: int_prod [symmetric] nat_int)
   5.191 -  done
   5.192 -
   5.193 -lemma transfer_nat_int_sum_prod_closure [no_atp]:
   5.194 -    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
   5.195 -    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   5.196 -  unfolding nat_set_def
   5.197 -  apply (rule sum_nonneg)
   5.198 -  apply auto
   5.199 -  apply (rule prod_nonneg)
   5.200 -  apply auto
   5.201 -done
   5.202 -
   5.203 -(* this version doesn't work, even with nat_set A \<Longrightarrow>
   5.204 -      x : A \<Longrightarrow> x >= 0 turned on. Why not?
   5.205 -
   5.206 -  also: what does =simp=> do?
   5.207 -
   5.208 -lemma transfer_nat_int_sum_prod_closure:
   5.209 -    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
   5.210 -    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   5.211 -  unfolding nat_set_def simp_implies_def
   5.212 -  apply (rule sum_nonneg)
   5.213 -  apply auto
   5.214 -  apply (rule prod_nonneg)
   5.215 -  apply auto
   5.216 -done
   5.217 -*)
   5.218 -
   5.219 -(* Making A = B in this lemma doesn't work. Why not?
   5.220 -   Also, why aren't sum.cong and prod.cong enough,
   5.221 -   with the previously mentioned rule turned on? *)
   5.222 -
   5.223 -lemma transfer_nat_int_sum_prod_cong [no_atp]:
   5.224 -    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   5.225 -      sum f A = sum g B"
   5.226 -    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   5.227 -      prod f A = prod g B"
   5.228 -  unfolding nat_set_def
   5.229 -  apply (subst sum.cong, assumption)
   5.230 -  apply auto [2]
   5.231 -  apply (subst prod.cong, assumption, auto)
   5.232 -done
   5.233 -
   5.234 -declare transfer_morphism_nat_int [transfer add
   5.235 -  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
   5.236 -    transfer_nat_int_sum_prod_closure
   5.237 -  cong: transfer_nat_int_sum_prod_cong]
   5.238 -
   5.239 -
   5.240 -subsection \<open>Set up transfer from int to nat\<close>
   5.241 -
   5.242 -text \<open>set up transfer direction\<close>
   5.243 -
   5.244 -lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
   5.245 -
   5.246 -declare transfer_morphism_int_nat [transfer add
   5.247 -  mode: manual
   5.248 -  return: nat_int
   5.249 -  labels: int_nat
   5.250 -]
   5.251 -
   5.252 -
   5.253 -text \<open>basic functions and relations\<close>
   5.254 -
   5.255 -definition
   5.256 -  is_nat :: "int \<Rightarrow> bool"
   5.257 -where
   5.258 -  "is_nat x = (x >= 0)"
   5.259 -
   5.260 -lemma transfer_int_nat_numerals [no_atp]:
   5.261 -    "0 = int 0"
   5.262 -    "1 = int 1"
   5.263 -    "2 = int 2"
   5.264 -    "3 = int 3"
   5.265 -  by auto
   5.266 -
   5.267 -lemma transfer_int_nat_functions [no_atp]:
   5.268 -    "(int x) + (int y) = int (x + y)"
   5.269 -    "(int x) * (int y) = int (x * y)"
   5.270 -    "tsub (int x) (int y) = int (x - y)"
   5.271 -    "(int x)^n = int (x^n)"
   5.272 -    "(int x) div (int y) = int (x div y)"
   5.273 -    "(int x) mod (int y) = int (x mod y)"
   5.274 -  by (auto simp add: zdiv_int zmod_int tsub_def)
   5.275 -
   5.276 -lemma transfer_int_nat_function_closures [no_atp]:
   5.277 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   5.278 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   5.279 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   5.280 -    "is_nat x \<Longrightarrow> is_nat (x^n)"
   5.281 -    "is_nat 0"
   5.282 -    "is_nat 1"
   5.283 -    "is_nat 2"
   5.284 -    "is_nat 3"
   5.285 -    "is_nat (int z)"
   5.286 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   5.287 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   5.288 -  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   5.289 -
   5.290 -lemma transfer_int_nat_relations [no_atp]:
   5.291 -    "(int x = int y) = (x = y)"
   5.292 -    "(int x < int y) = (x < y)"
   5.293 -    "(int x <= int y) = (x <= y)"
   5.294 -    "(int x dvd int y) = (x dvd y)"
   5.295 -  by (auto simp add: zdvd_int)
   5.296 -
   5.297 -declare transfer_morphism_int_nat [transfer add return:
   5.298 -  transfer_int_nat_numerals
   5.299 -  transfer_int_nat_functions
   5.300 -  transfer_int_nat_function_closures
   5.301 -  transfer_int_nat_relations
   5.302 -]
   5.303 -
   5.304 -
   5.305 -text \<open>first-order quantifiers\<close>
   5.306 -
   5.307 -lemma transfer_int_nat_quantifiers [no_atp]:
   5.308 -    "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   5.309 -    "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   5.310 -  apply (subst all_nat)
   5.311 -  apply auto [1]
   5.312 -  apply (subst ex_nat)
   5.313 -  apply auto
   5.314 -done
   5.315 -
   5.316 -declare transfer_morphism_int_nat [transfer add
   5.317 -  return: transfer_int_nat_quantifiers]
   5.318 -
   5.319 -
   5.320 -text \<open>if\<close>
   5.321 -
   5.322 -lemma int_if_cong: "(if P then (int x) else (int y)) =
   5.323 -    int (if P then x else y)"
   5.324 -  by auto
   5.325 -
   5.326 -declare transfer_morphism_int_nat [transfer add return: int_if_cong]
   5.327 -
   5.328 -
   5.329 -
   5.330 -text \<open>operations with sets\<close>
   5.331 -
   5.332 -lemma transfer_int_nat_set_functions [no_atp]:
   5.333 -    "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   5.334 -    "{} = int ` ({}::nat set)"
   5.335 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   5.336 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
   5.337 -    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
   5.338 -    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   5.339 -       (* need all variants of these! *)
   5.340 -  by (simp_all only: is_nat_def transfer_nat_int_set_functions
   5.341 -          transfer_nat_int_set_function_closures
   5.342 -          transfer_nat_int_set_return_embed nat_0_le
   5.343 -          cong: transfer_nat_int_set_cong)
   5.344 -
   5.345 -lemma transfer_int_nat_set_function_closures [no_atp]:
   5.346 -    "nat_set {}"
   5.347 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   5.348 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   5.349 -    "nat_set {x. x >= 0 & P x}"
   5.350 -    "nat_set (int ` C)"
   5.351 -    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   5.352 -    "is_nat x \<Longrightarrow> nat_set {x..y}"
   5.353 -  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
   5.354 -
   5.355 -lemma transfer_int_nat_set_relations [no_atp]:
   5.356 -    "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
   5.357 -    "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
   5.358 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
   5.359 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
   5.360 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
   5.361 -  by (simp_all only: is_nat_def transfer_nat_int_set_relations
   5.362 -    transfer_nat_int_set_return_embed nat_0_le)
   5.363 -
   5.364 -lemma transfer_int_nat_set_return_embed [no_atp]: "nat ` int ` A = A"
   5.365 -  by (simp only: transfer_nat_int_set_relations
   5.366 -    transfer_nat_int_set_function_closures
   5.367 -    transfer_nat_int_set_return_embed nat_0_le)
   5.368 -
   5.369 -lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
   5.370 -    {(x::nat). P x} = {x. P' x}"
   5.371 -  by auto
   5.372 -
   5.373 -declare transfer_morphism_int_nat [transfer add
   5.374 -  return: transfer_int_nat_set_functions
   5.375 -    transfer_int_nat_set_function_closures
   5.376 -    transfer_int_nat_set_relations
   5.377 -    transfer_int_nat_set_return_embed
   5.378 -  cong: transfer_int_nat_set_cong
   5.379 -]
   5.380 -
   5.381 -
   5.382 -text \<open>sum and prod\<close>
   5.383 -
   5.384 -(* this handles the case where the *domain* of f is int *)
   5.385 -lemma transfer_int_nat_sum_prod [no_atp]:
   5.386 -    "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
   5.387 -    "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
   5.388 -  apply (subst sum.reindex)
   5.389 -  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
   5.390 -  apply (subst prod.reindex)
   5.391 -  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
   5.392 -            cong: prod.cong)
   5.393 -done
   5.394 -
   5.395 -(* this handles the case where the *range* of f is int *)
   5.396 -lemma transfer_int_nat_sum_prod2 [no_atp]:
   5.397 -    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
   5.398 -    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
   5.399 -      prod f A = int(prod (%x. nat (f x)) A)"
   5.400 -  unfolding is_nat_def
   5.401 -  by (subst int_sum) auto
   5.402 -
   5.403 -declare transfer_morphism_int_nat [transfer add
   5.404 -  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   5.405 -  cong: sum.cong prod.cong]
   5.406 -
   5.407 -declare transfer_morphism_int_nat [transfer add return: even_int_iff]
   5.408 -
   5.409 -lemma transfer_nat_int_gcd [no_atp]:
   5.410 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   5.411 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   5.412 -  for x y :: int
   5.413 -  unfolding gcd_int_def lcm_int_def by auto
   5.414 -
   5.415 -lemma transfer_nat_int_gcd_closures [no_atp]:
   5.416 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
   5.417 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
   5.418 -  for x y :: int
   5.419 -  by (auto simp add: gcd_int_def lcm_int_def)
   5.420 -
   5.421 -declare transfer_morphism_nat_int
   5.422 -  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   5.423 -
   5.424 -lemma transfer_int_nat_gcd [no_atp]:
   5.425 -  "gcd (int x) (int y) = int (gcd x y)"
   5.426 -  "lcm (int x) (int y) = int (lcm x y)"
   5.427 -  by (auto simp: gcd_int_def lcm_int_def)
   5.428 -
   5.429 -lemma transfer_int_nat_gcd_closures [no_atp]:
   5.430 -  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   5.431 -  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   5.432 -  by (auto simp: gcd_int_def lcm_int_def)
   5.433 -
   5.434 -declare transfer_morphism_int_nat
   5.435 -  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   5.436 -
   5.437 -definition embed_list :: "nat list \<Rightarrow> int list" where
   5.438 -"embed_list l = map int l"
   5.439 -
   5.440 -definition nat_list :: "int list \<Rightarrow> bool" where
   5.441 -"nat_list l = nat_set (set l)"
   5.442 -
   5.443 -definition return_list :: "int list \<Rightarrow> nat list" where
   5.444 -"return_list l = map nat l"
   5.445 -
   5.446 -lemma transfer_nat_int_list_return_embed [no_atp]:
   5.447 -  "nat_list l \<longrightarrow> embed_list (return_list l) = l"
   5.448 -  unfolding embed_list_def return_list_def nat_list_def nat_set_def
   5.449 -  apply (induct l)
   5.450 -  apply auto
   5.451 -done
   5.452 -
   5.453 -lemma transfer_nat_int_list_functions [no_atp]:
   5.454 -  "l @ m = return_list (embed_list l @ embed_list m)"
   5.455 -  "[] = return_list []"
   5.456 -  unfolding return_list_def embed_list_def
   5.457 -  apply auto
   5.458 -  apply (induct l, auto)
   5.459 -  apply (induct m, auto)
   5.460 -done
   5.461 -
   5.462 -(*
   5.463 -lemma transfer_nat_int_fold1: "fold f l x =
   5.464 -    fold (%x. f (nat x)) (embed_list l) x";
   5.465 -*)
   5.466 -
   5.467 -end
     6.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Oct 30 19:29:06 2017 +0000
     6.2 +++ b/src/HOL/Number_Theory/Cong.thy	Tue Oct 31 07:11:03 2017 +0000
     6.3 @@ -161,54 +161,56 @@
     6.4  
     6.5  subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
     6.6  
     6.7 -lemma transfer_nat_int_cong:
     6.8 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
     6.9 -  for x y m :: int
    6.10 -  by (auto simp add: cong_def nat_mod_distrib [symmetric])
    6.11 -     (metis eq_nat_nat_iff le_less mod_by_0 pos_mod_conj)
    6.12 -
    6.13 -declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
    6.14 -
    6.15  lemma cong_int_iff:
    6.16    "[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)"
    6.17    by (simp add: cong_def of_nat_mod [symmetric])
    6.18  
    6.19 -lemma transfer_int_nat_cong:
    6.20 -  "[int x = int y] (mod (int m)) = [x = y] (mod m)"
    6.21 -  by (fact cong_int_iff)
    6.22 -
    6.23 -declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong]
    6.24 -
    6.25  lemma cong_Suc_0 [simp, presburger]:
    6.26    "[m = n] (mod Suc 0)"
    6.27    using cong_1 [of m n] by simp
    6.28  
    6.29 -lemma cong_diff_aux_int:
    6.30 -  "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
    6.31 -    a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
    6.32 -  for a b c d :: int
    6.33 -  by (metis cong_diff tsub_eq)
    6.34 -
    6.35  lemma cong_diff_nat:
    6.36    "[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
    6.37 -    and "a \<ge> c" "b \<ge> d" for a b c d m :: nat 
    6.38 -  using that by (rule cong_diff_aux_int [transferred])
    6.39 -
    6.40 -lemma cong_diff_iff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [tsub a b = 0] (mod m) = [a = b] (mod m)"
    6.41 -  for a b :: int
    6.42 -  by (subst tsub_eq, assumption, rule cong_diff_iff_cong_0)
    6.43 +    and "a \<ge> c" "b \<ge> d" for a b c d m :: nat
    6.44 +proof -
    6.45 +  have "[c + (a - c) = d + (b - d)] (mod m)"
    6.46 +    using that by simp
    6.47 +  with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)"
    6.48 +    using mod_add_cong by (auto simp add: cong_def) fastforce
    6.49 +  then show ?thesis
    6.50 +    by (simp add: cong_def nat_mod_eq_iff)
    6.51 +qed
    6.52  
    6.53  lemma cong_diff_iff_cong_0_nat:
    6.54 -  fixes a b :: nat
    6.55 -  assumes "a \<ge> b"
    6.56 -  shows "[a - b = 0] (mod m) = [a = b] (mod m)"
    6.57 -  using assms by (rule cong_diff_iff_cong_0_aux_int [transferred])
    6.58 +  "[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat
    6.59 +  using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma)
    6.60  
    6.61 -lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
    6.62 +lemma cong_diff_iff_cong_0_nat':
    6.63 +  "[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)"
    6.64 +proof (cases "b \<le> a")
    6.65 +  case True
    6.66 +  then show ?thesis
    6.67 +    by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m])
    6.68 +next
    6.69 +  case False
    6.70 +  then have "a \<le> b"
    6.71 +    by simp
    6.72 +  then show ?thesis
    6.73 +    by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m])
    6.74 +      (auto simp add: cong_def)
    6.75 +qed
    6.76 +
    6.77 +lemma cong_altdef_nat:
    6.78 +  "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
    6.79    for a b :: nat
    6.80    by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
    6.81  
    6.82 -lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
    6.83 +lemma cong_altdef_nat':
    6.84 +  "[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
    6.85 +  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat')
    6.86 +
    6.87 +lemma cong_altdef_int:
    6.88 +  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
    6.89    for a b :: int
    6.90    by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
    6.91  
    6.92 @@ -224,31 +226,47 @@
    6.93    apply (auto simp add: field_simps)
    6.94    done
    6.95  
    6.96 -lemma cong_mult_rcancel_int: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
    6.97 -  for a k m :: int
    6.98 -  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
    6.99 -
   6.100 -lemma cong_mult_rcancel_nat: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   6.101 -  for a k m :: nat
   6.102 -  by (metis cong_mult_rcancel_int [transferred])
   6.103 +lemma cong_mult_rcancel_int:
   6.104 +  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   6.105 +  if "coprime k m" for a k m :: int
   6.106 +  by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
   6.107  
   6.108 -lemma cong_mult_lcancel_nat: "coprime k m \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
   6.109 -  for a k m :: nat
   6.110 -  by (simp add: mult.commute cong_mult_rcancel_nat)
   6.111 +lemma cong_mult_rcancel_nat:
   6.112 +  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   6.113 +  if "coprime k m" for a k m :: nat
   6.114 +proof -
   6.115 +  have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>"
   6.116 +    by (simp add: cong_altdef_nat')
   6.117 +  also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>"
   6.118 +    by (simp add: algebra_simps)
   6.119 +  also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
   6.120 +    by (simp add: abs_mult nat_times_as_int)
   6.121 +  also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
   6.122 +    by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
   6.123 +  also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
   6.124 +    by (simp add: cong_altdef_nat')
   6.125 +  finally show ?thesis .
   6.126 +qed
   6.127  
   6.128 -lemma cong_mult_lcancel_int: "coprime k m \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
   6.129 -  for a k m :: int
   6.130 -  by (simp add: mult.commute cong_mult_rcancel_int)
   6.131 +lemma cong_mult_lcancel_int:
   6.132 +  "[k * a = k * b] (mod m) = [a = b] (mod m)"
   6.133 +  if "coprime k m" for a k m :: int
   6.134 +  using that by (simp add: cong_mult_rcancel_int ac_simps)
   6.135 +
   6.136 +lemma cong_mult_lcancel_nat:
   6.137 +  "[k * a = k * b] (mod m) = [a = b] (mod m)"
   6.138 +  if "coprime k m" for a k m :: nat
   6.139 +  using that by (simp add: cong_mult_rcancel_nat ac_simps)
   6.140  
   6.141  lemma coprime_cong_mult_int:
   6.142    "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   6.143    for a b :: int
   6.144 -  by (metis divides_mult cong_altdef_int)
   6.145 +  by (simp add: cong_altdef_int divides_mult)
   6.146  
   6.147  lemma coprime_cong_mult_nat:
   6.148    "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   6.149    for a b :: nat
   6.150 -  by (metis coprime_cong_mult_int [transferred])
   6.151 +  by (simp add: cong_altdef_nat' divides_mult)
   6.152  
   6.153  lemma cong_less_imp_eq_nat: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   6.154    for a b :: nat
   6.155 @@ -292,14 +310,14 @@
   6.156      by (metis cong_def mult.commute nat_mod_eq_iff) 
   6.157  qed
   6.158  
   6.159 +lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   6.160 +  for a b :: nat
   6.161 +  by (auto simp add: cong_def) (metis gcd_red_nat)
   6.162 +
   6.163  lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   6.164    for a b :: int
   6.165    by (auto simp add: cong_def) (metis gcd_red_int)
   6.166  
   6.167 -lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   6.168 -  for a b :: nat
   6.169 -  by (metis cong_gcd_eq_int [transferred])
   6.170 -
   6.171  lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   6.172    for a b :: nat
   6.173    by (auto simp add: cong_gcd_eq_nat)
     7.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 30 19:29:06 2017 +0000
     7.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Oct 31 07:11:03 2017 +0000
     7.3 @@ -291,8 +291,8 @@
     7.4  next
     7.5    case False
     7.6    with assms show ?thesis
     7.7 -    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
     7.8 -    by (auto simp add: residues_def gcd_int_def) force
     7.9 +    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
    7.10 +    by (auto simp add: residues_def gcd_int_def) fastforce
    7.11  qed
    7.12  
    7.13  lemma fermat_theorem:
     8.1 --- a/src/HOL/ROOT	Mon Oct 30 19:29:06 2017 +0000
     8.2 +++ b/src/HOL/ROOT	Tue Oct 31 07:11:03 2017 +0000
     8.3 @@ -590,7 +590,6 @@
     8.4      Termination
     8.5      ThreeDivides
     8.6      Transfer_Debug
     8.7 -    Transfer_Ex
     8.8      Transfer_Int_Nat
     8.9      Transitive_Closure_Table_Ex
    8.10      Tree23
     9.1 --- a/src/HOL/ex/Transfer_Ex.thy	Mon Oct 30 19:29:06 2017 +0000
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,65 +0,0 @@
     9.4 -
     9.5 -section \<open>Various examples for transfer procedure\<close>
     9.6 -
     9.7 -theory Transfer_Ex
     9.8 -imports Main Transfer_Int_Nat
     9.9 -begin
    9.10 -
    9.11 -lemma ex1: "(x::nat) + y = y + x"
    9.12 -  by auto
    9.13 -
    9.14 -lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> x + y = y + x"
    9.15 -  by (fact ex1 [transferred])
    9.16 -
    9.17 -(* Using new transfer package *)
    9.18 -lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> x + y = y + x"
    9.19 -  by (fact ex1 [untransferred])
    9.20 -
    9.21 -lemma ex2: "(a::nat) div b * b + a mod b = a"
    9.22 -  by (rule div_mult_mod_eq)
    9.23 -
    9.24 -lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
    9.25 -  by (fact ex2 [transferred])
    9.26 -
    9.27 -(* Using new transfer package *)
    9.28 -lemma "0 \<le> (a::int) \<Longrightarrow> 0 \<le> (b::int) \<Longrightarrow> a div b * b + a mod b = a"
    9.29 -  by (fact ex2 [untransferred])
    9.30 -
    9.31 -lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
    9.32 -  by auto
    9.33 -
    9.34 -lemma "\<forall>x\<ge>0::int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
    9.35 -  by (fact ex3 [transferred nat_int])
    9.36 -
    9.37 -(* Using new transfer package *)
    9.38 -lemma "\<forall>x::int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
    9.39 -  by (fact ex3 [untransferred])
    9.40 -
    9.41 -lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
    9.42 -  by auto
    9.43 -
    9.44 -lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
    9.45 -  by (fact ex4 [transferred])
    9.46 -
    9.47 -(* Using new transfer package *)
    9.48 -lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
    9.49 -  by (fact ex4 [untransferred])
    9.50 -
    9.51 -lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
    9.52 -  by (induct n rule: nat_induct, auto)
    9.53 -
    9.54 -lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    9.55 -  by (fact ex5 [transferred])
    9.56 -
    9.57 -(* Using new transfer package *)
    9.58 -lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    9.59 -  by (fact ex5 [untransferred])
    9.60 -
    9.61 -lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    9.62 -  by (fact ex5 [transferred, transferred])
    9.63 -
    9.64 -(* Using new transfer package *)
    9.65 -lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
    9.66 -  by (fact ex5 [untransferred, Transfer.transferred])
    9.67 -
    9.68 -end
    10.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Mon Oct 30 19:29:06 2017 +0000
    10.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Tue Oct 31 07:11:03 2017 +0000
    10.3 @@ -39,13 +39,16 @@
    10.4    unfolding rel_fun_def ZN_def by simp
    10.5  
    10.6  lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
    10.7 -  unfolding rel_fun_def ZN_def by (simp add: of_nat_mult)
    10.8 +  unfolding rel_fun_def ZN_def by simp
    10.9 +
   10.10 +definition tsub :: "int \<Rightarrow> int \<Rightarrow> int"
   10.11 +  where "tsub k l = max 0 (k - l)"
   10.12  
   10.13  lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
   10.14 -  unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff)
   10.15 +  unfolding rel_fun_def ZN_def by (auto simp add: of_nat_diff tsub_def)
   10.16  
   10.17  lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
   10.18 -  unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
   10.19 +  unfolding rel_fun_def ZN_def by simp
   10.20  
   10.21  lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
   10.22    unfolding rel_fun_def ZN_def by simp
   10.23 @@ -92,7 +95,7 @@
   10.24    unfolding rel_fun_def ZN_def by (simp add: zmod_int)
   10.25  
   10.26  lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
   10.27 -  unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd)
   10.28 +  unfolding rel_fun_def ZN_def by (simp add: gcd_int_def)
   10.29  
   10.30  lemma ZN_atMost [transfer_rule]:
   10.31    "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"