--- a/NEWS Mon Oct 30 19:29:06 2017 +0000
+++ b/NEWS Tue Oct 31 07:11:03 2017 +0000
@@ -66,6 +66,8 @@
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.
+* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Decision_Procs/Conversions.thy Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Decision_Procs/Conversions.thy Tue Oct 31 07:11:03 2017 +0000
@@ -93,7 +93,7 @@
ML \<open>
fun nat_conv i = (case strip_app i of
(@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
- | (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
+ | (@{const_name one_class.one}, []) => @{thm nat_one_as_int [meta, symmetric]}
| (@{const_name numeral}, [b]) => inst [] [b] @{thm nat_numeral [meta]}
| (@{const_name uminus}, [b]) => (case strip_app b of
(@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
--- a/src/HOL/Main.thy Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Main.thy Tue Oct 31 07:11:03 2017 +0000
@@ -15,7 +15,6 @@
Conditionally_Complete_Lattices
Binomial
GCD
- Nat_Transfer
begin
text \<open>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Oct 31 07:11:03 2017 +0000
@@ -268,7 +268,6 @@
@{const_name Meson.skolem},
@{const_name ATP.fequal},
@{const_name ATP.fEx},
- @{const_name transfer_morphism},
@{const_name enum_prod_inst.enum_all_prod},
@{const_name enum_prod_inst.enum_ex_prod},
@{const_name Quickcheck_Random.catch_match},
--- a/src/HOL/Nat_Transfer.thy Mon Oct 30 19:29:06 2017 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,464 +0,0 @@
-(* Authors: Jeremy Avigad and Amine Chaieb *)
-
-section \<open>Generic transfer machinery; specific transfer from nats to ints and back.\<close>
-
-theory Nat_Transfer
-imports List GCD
-begin
-
-subsection \<open>Generic transfer machinery\<close>
-
-definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
- where "transfer_morphism f A \<longleftrightarrow> True"
-
-lemma transfer_morphismI[intro]: "transfer_morphism f A"
- by (simp add: transfer_morphism_def)
-
-ML_file "Tools/legacy_transfer.ML"
-
-
-subsection \<open>Set up transfer from nat to int\<close>
-
-text \<open>set up transfer direction\<close>
-
-lemma transfer_morphism_nat_int [no_atp]:
- "transfer_morphism nat (op <= (0::int))" ..
-
-declare transfer_morphism_nat_int [transfer add
- mode: manual
- return: nat_0_le
- labels: nat_int
-]
-
-text \<open>basic functions and relations\<close>
-
-lemma transfer_nat_int_numerals [no_atp, transfer key: transfer_morphism_nat_int]:
- "(0::nat) = nat 0"
- "(1::nat) = nat 1"
- "(2::nat) = nat 2"
- "(3::nat) = nat 3"
- by auto
-
-definition
- tsub :: "int \<Rightarrow> int \<Rightarrow> int"
-where
- "tsub x y = (if x >= y then x - y else 0)"
-
-lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
- by (simp add: tsub_def)
-
-lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
- "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
- by (auto simp add: eq_nat_nat_iff nat_mult_distrib
- nat_power_eq tsub_def nat_div_distrib nat_mod_distrib)
-
-lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
- "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
- "(0::int) >= 0"
- "(1::int) >= 0"
- "(2::int) >= 0"
- "(3::int) >= 0"
- "int z >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
- apply (auto simp add: zero_le_mult_iff tsub_def pos_imp_zdiv_nonneg_iff)
- apply (cases "y = 0")
- apply (auto simp add: pos_imp_zdiv_nonneg_iff)
- apply (cases "y = 0")
- apply auto
- done
-
-lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]:
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) = nat y) = (x = y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) < nat y) = (x < y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) <= nat y) = (x <= y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) dvd nat y) = (x dvd y)"
- by (auto simp add: zdvd_int)
-
-
-text \<open>first-order quantifiers\<close>
-
-lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
- "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
- "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
- by (rule all_nat, rule ex_nat)
-
-declare transfer_morphism_nat_int [transfer add
- cong: all_cong ex_cong]
-
-
-text \<open>if\<close>
-
-lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
- "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
- by auto
-
-
-text \<open>operations with sets\<close>
-
-definition
- nat_set :: "int set \<Rightarrow> bool"
-where
- "nat_set S = (ALL x:S. x >= 0)"
-
-lemma transfer_nat_int_set_functions [no_atp]:
- "card A = card (int ` A)"
- "{} = nat ` ({}::int set)"
- "A Un B = nat ` (int ` A Un int ` B)"
- "A Int B = nat ` (int ` A Int int ` B)"
- "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
- "{..n} = nat ` {0..int n}"
- "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
- by (rule card_image [symmetric])
- (auto simp add: inj_on_def image_def intro: bexI [of _ "int x" for x] exI [of _ "int x" for x])
-
-lemma transfer_nat_int_set_function_closures [no_atp]:
- "nat_set {}"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "nat_set {x. x >= 0 & P x}"
- "nat_set (int ` C)"
- "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
- "x >= 0 \<Longrightarrow> nat_set {x..y}"
- unfolding nat_set_def apply auto
-done
-
-lemma transfer_nat_int_set_relations [no_atp]:
- "(finite A) = (finite (int ` A))"
- "(x : A) = (int x : int ` A)"
- "(A = B) = (int ` A = int ` B)"
- "(A < B) = (int ` A < int ` B)"
- "(A <= B) = (int ` A <= int ` B)"
- apply (rule iffI)
- apply (erule finite_imageI)
- apply (erule finite_imageD)
- apply (auto simp add: image_def set_eq_iff inj_on_def)
- apply (drule_tac x = "int x" in spec, auto)
- apply (drule_tac x = "int x" in spec, auto)
- apply (drule_tac x = "int x" in spec, auto)
-done
-
-lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \<Longrightarrow>
- (int ` nat ` A = A)"
- by (auto simp add: nat_set_def image_def)
-
-lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
- {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
- by auto
-
-declare transfer_morphism_nat_int [transfer add
- return: transfer_nat_int_set_functions
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_relations
- transfer_nat_int_set_return_embed
- cong: transfer_nat_int_set_cong
-]
-
-
-text \<open>sum and prod\<close>
-
-(* this handles the case where the *domain* of f is nat *)
-lemma transfer_nat_int_sum_prod [no_atp]:
- "sum f A = sum (%x. f (nat x)) (int ` A)"
- "prod f A = prod (%x. f (nat x)) (int ` A)"
- apply (subst sum.reindex)
- apply (unfold inj_on_def, auto)
- apply (subst prod.reindex)
- apply (unfold inj_on_def o_def, auto)
-done
-
-(* this handles the case where the *range* of f is nat *)
-lemma transfer_nat_int_sum_prod2 [no_atp]:
- "sum f A = nat(sum (%x. int (f x)) A)"
- "prod f A = nat(prod (%x. int (f x)) A)"
- apply (simp only: int_sum [symmetric] nat_int)
- apply (simp only: int_prod [symmetric] nat_int)
- done
-
-lemma transfer_nat_int_sum_prod_closure [no_atp]:
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
- unfolding nat_set_def
- apply (rule sum_nonneg)
- apply auto
- apply (rule prod_nonneg)
- apply auto
-done
-
-(* this version doesn't work, even with nat_set A \<Longrightarrow>
- x : A \<Longrightarrow> x >= 0 turned on. Why not?
-
- also: what does =simp=> do?
-
-lemma transfer_nat_int_sum_prod_closure:
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
- unfolding nat_set_def simp_implies_def
- apply (rule sum_nonneg)
- apply auto
- apply (rule prod_nonneg)
- apply auto
-done
-*)
-
-(* Making A = B in this lemma doesn't work. Why not?
- Also, why aren't sum.cong and prod.cong enough,
- with the previously mentioned rule turned on? *)
-
-lemma transfer_nat_int_sum_prod_cong [no_atp]:
- "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- sum f A = sum g B"
- "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- prod f A = prod g B"
- unfolding nat_set_def
- apply (subst sum.cong, assumption)
- apply auto [2]
- apply (subst prod.cong, assumption, auto)
-done
-
-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]
-
-
-subsection \<open>Set up transfer from int to nat\<close>
-
-text \<open>set up transfer direction\<close>
-
-lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
-
-declare transfer_morphism_int_nat [transfer add
- mode: manual
- return: nat_int
- labels: int_nat
-]
-
-
-text \<open>basic functions and relations\<close>
-
-definition
- is_nat :: "int \<Rightarrow> bool"
-where
- "is_nat x = (x >= 0)"
-
-lemma transfer_int_nat_numerals [no_atp]:
- "0 = int 0"
- "1 = int 1"
- "2 = int 2"
- "3 = int 3"
- by auto
-
-lemma transfer_int_nat_functions [no_atp]:
- "(int x) + (int y) = int (x + y)"
- "(int x) * (int y) = int (x * y)"
- "tsub (int x) (int y) = int (x - y)"
- "(int x)^n = int (x^n)"
- "(int x) div (int y) = int (x div y)"
- "(int x) mod (int y) = int (x mod y)"
- by (auto simp add: zdiv_int zmod_int tsub_def)
-
-lemma transfer_int_nat_function_closures [no_atp]:
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
- "is_nat x \<Longrightarrow> is_nat (x^n)"
- "is_nat 0"
- "is_nat 1"
- "is_nat 2"
- "is_nat 3"
- "is_nat (int z)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
- "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)
-
-lemma transfer_int_nat_relations [no_atp]:
- "(int x = int y) = (x = y)"
- "(int x < int y) = (x < y)"
- "(int x <= int y) = (x <= y)"
- "(int x dvd int y) = (x dvd y)"
- by (auto simp add: zdvd_int)
-
-declare transfer_morphism_int_nat [transfer add return:
- transfer_int_nat_numerals
- transfer_int_nat_functions
- transfer_int_nat_function_closures
- transfer_int_nat_relations
-]
-
-
-text \<open>first-order quantifiers\<close>
-
-lemma transfer_int_nat_quantifiers [no_atp]:
- "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
- "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
- apply (subst all_nat)
- apply auto [1]
- apply (subst ex_nat)
- apply auto
-done
-
-declare transfer_morphism_int_nat [transfer add
- return: transfer_int_nat_quantifiers]
-
-
-text \<open>if\<close>
-
-lemma int_if_cong: "(if P then (int x) else (int y)) =
- int (if P then x else y)"
- by auto
-
-declare transfer_morphism_int_nat [transfer add return: int_if_cong]
-
-
-
-text \<open>operations with sets\<close>
-
-lemma transfer_int_nat_set_functions [no_atp]:
- "nat_set A \<Longrightarrow> card A = card (nat ` A)"
- "{} = int ` ({}::nat set)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
- "{x. x >= 0 & P x} = int ` {x. P(int x)}"
- "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
- (* need all variants of these! *)
- by (simp_all only: is_nat_def transfer_nat_int_set_functions
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_return_embed nat_0_le
- cong: transfer_nat_int_set_cong)
-
-lemma transfer_int_nat_set_function_closures [no_atp]:
- "nat_set {}"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "nat_set {x. x >= 0 & P x}"
- "nat_set (int ` C)"
- "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
- "is_nat x \<Longrightarrow> nat_set {x..y}"
- by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
-
-lemma transfer_int_nat_set_relations [no_atp]:
- "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
- "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
- by (simp_all only: is_nat_def transfer_nat_int_set_relations
- transfer_nat_int_set_return_embed nat_0_le)
-
-lemma transfer_int_nat_set_return_embed [no_atp]: "nat ` int ` A = A"
- by (simp only: transfer_nat_int_set_relations
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_return_embed nat_0_le)
-
-lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
- {(x::nat). P x} = {x. P' x}"
- by auto
-
-declare transfer_morphism_int_nat [transfer add
- return: transfer_int_nat_set_functions
- transfer_int_nat_set_function_closures
- transfer_int_nat_set_relations
- transfer_int_nat_set_return_embed
- cong: transfer_int_nat_set_cong
-]
-
-
-text \<open>sum and prod\<close>
-
-(* this handles the case where the *domain* of f is int *)
-lemma transfer_int_nat_sum_prod [no_atp]:
- "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
- "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
- apply (subst sum.reindex)
- apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
- apply (subst prod.reindex)
- apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
- cong: prod.cong)
-done
-
-(* this handles the case where the *range* of f is int *)
-lemma transfer_int_nat_sum_prod2 [no_atp]:
- "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
- "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
- prod f A = int(prod (%x. nat (f x)) A)"
- unfolding is_nat_def
- by (subst int_sum) auto
-
-declare transfer_morphism_int_nat [transfer add
- return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
- cong: sum.cong prod.cong]
-
-declare transfer_morphism_int_nat [transfer add return: even_int_iff]
-
-lemma transfer_nat_int_gcd [no_atp]:
- "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
- "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
- for x y :: int
- unfolding gcd_int_def lcm_int_def by auto
-
-lemma transfer_nat_int_gcd_closures [no_atp]:
- "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
- "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
- for x y :: int
- by (auto simp add: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_nat_int
- [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
-
-lemma transfer_int_nat_gcd [no_atp]:
- "gcd (int x) (int y) = int (gcd x y)"
- "lcm (int x) (int y) = int (lcm x y)"
- by (auto simp: gcd_int_def lcm_int_def)
-
-lemma transfer_int_nat_gcd_closures [no_atp]:
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
- by (auto simp: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_int_nat
- [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
-
-definition embed_list :: "nat list \<Rightarrow> int list" where
-"embed_list l = map int l"
-
-definition nat_list :: "int list \<Rightarrow> bool" where
-"nat_list l = nat_set (set l)"
-
-definition return_list :: "int list \<Rightarrow> nat list" where
-"return_list l = map nat l"
-
-lemma transfer_nat_int_list_return_embed [no_atp]:
- "nat_list l \<longrightarrow> embed_list (return_list l) = l"
- unfolding embed_list_def return_list_def nat_list_def nat_set_def
- apply (induct l)
- apply auto
-done
-
-lemma transfer_nat_int_list_functions [no_atp]:
- "l @ m = return_list (embed_list l @ embed_list m)"
- "[] = return_list []"
- unfolding return_list_def embed_list_def
- apply auto
- apply (induct l, auto)
- apply (induct m, auto)
-done
-
-(*
-lemma transfer_nat_int_fold1: "fold f l x =
- fold (%x. f (nat x)) (embed_list l) x";
-*)
-
-end
--- a/src/HOL/Number_Theory/Cong.thy Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Number_Theory/Cong.thy Tue Oct 31 07:11:03 2017 +0000
@@ -161,54 +161,56 @@
subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
-lemma transfer_nat_int_cong:
- "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
- for x y m :: int
- by (auto simp add: cong_def nat_mod_distrib [symmetric])
- (metis eq_nat_nat_iff le_less mod_by_0 pos_mod_conj)
-
-declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
-
lemma cong_int_iff:
"[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)"
by (simp add: cong_def of_nat_mod [symmetric])
-lemma transfer_int_nat_cong:
- "[int x = int y] (mod (int m)) = [x = y] (mod m)"
- by (fact cong_int_iff)
-
-declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong]
-
lemma cong_Suc_0 [simp, presburger]:
"[m = n] (mod Suc 0)"
using cong_1 [of m n] by simp
-lemma cong_diff_aux_int:
- "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
- a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
- for a b c d :: int
- by (metis cong_diff tsub_eq)
-
lemma cong_diff_nat:
"[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
- and "a \<ge> c" "b \<ge> d" for a b c d m :: nat
- using that by (rule cong_diff_aux_int [transferred])
-
-lemma cong_diff_iff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [tsub a b = 0] (mod m) = [a = b] (mod m)"
- for a b :: int
- by (subst tsub_eq, assumption, rule cong_diff_iff_cong_0)
+ and "a \<ge> c" "b \<ge> d" for a b c d m :: nat
+proof -
+ have "[c + (a - c) = d + (b - d)] (mod m)"
+ using that by simp
+ with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)"
+ using mod_add_cong by (auto simp add: cong_def) fastforce
+ then show ?thesis
+ by (simp add: cong_def nat_mod_eq_iff)
+qed
lemma cong_diff_iff_cong_0_nat:
- fixes a b :: nat
- assumes "a \<ge> b"
- shows "[a - b = 0] (mod m) = [a = b] (mod m)"
- using assms by (rule cong_diff_iff_cong_0_aux_int [transferred])
+ "[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat
+ using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma)
-lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+lemma cong_diff_iff_cong_0_nat':
+ "[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+proof (cases "b \<le> a")
+ case True
+ then show ?thesis
+ by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m])
+next
+ case False
+ then have "a \<le> b"
+ by simp
+ then show ?thesis
+ by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m])
+ (auto simp add: cong_def)
+qed
+
+lemma cong_altdef_nat:
+ "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
for a b :: nat
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
-lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+lemma cong_altdef_nat':
+ "[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
+ by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat')
+
+lemma cong_altdef_int:
+ "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
for a b :: int
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
@@ -224,31 +226,47 @@
apply (auto simp add: field_simps)
done
-lemma cong_mult_rcancel_int: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
- for a k m :: int
- by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
-
-lemma cong_mult_rcancel_nat: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
- for a k m :: nat
- by (metis cong_mult_rcancel_int [transferred])
+lemma cong_mult_rcancel_int:
+ "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+ if "coprime k m" for a k m :: int
+ by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
-lemma cong_mult_lcancel_nat: "coprime k m \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
- for a k m :: nat
- by (simp add: mult.commute cong_mult_rcancel_nat)
+lemma cong_mult_rcancel_nat:
+ "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+ if "coprime k m" for a k m :: nat
+proof -
+ have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>"
+ by (simp add: cong_altdef_nat')
+ also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
+ by (simp add: abs_mult nat_times_as_int)
+ also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
+ by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
+ also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
+ by (simp add: cong_altdef_nat')
+ finally show ?thesis .
+qed
-lemma cong_mult_lcancel_int: "coprime k m \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
- for a k m :: int
- by (simp add: mult.commute cong_mult_rcancel_int)
+lemma cong_mult_lcancel_int:
+ "[k * a = k * b] (mod m) = [a = b] (mod m)"
+ if "coprime k m" for a k m :: int
+ using that by (simp add: cong_mult_rcancel_int ac_simps)
+
+lemma cong_mult_lcancel_nat:
+ "[k * a = k * b] (mod m) = [a = b] (mod m)"
+ if "coprime k m" for a k m :: nat
+ using that by (simp add: cong_mult_rcancel_nat ac_simps)
lemma coprime_cong_mult_int:
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
for a b :: int
- by (metis divides_mult cong_altdef_int)
+ by (simp add: cong_altdef_int divides_mult)
lemma coprime_cong_mult_nat:
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
for a b :: nat
- by (metis coprime_cong_mult_int [transferred])
+ by (simp add: cong_altdef_nat' divides_mult)
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"
for a b :: nat
@@ -292,14 +310,14 @@
by (metis cong_def mult.commute nat_mod_eq_iff)
qed
+lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+ for a b :: nat
+ by (auto simp add: cong_def) (metis gcd_red_nat)
+
lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
for a b :: int
by (auto simp add: cong_def) (metis gcd_red_int)
-lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
- for a b :: nat
- by (metis cong_gcd_eq_int [transferred])
-
lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
for a b :: nat
by (auto simp add: cong_gcd_eq_nat)
--- a/src/HOL/Number_Theory/Residues.thy Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Number_Theory/Residues.thy Tue Oct 31 07:11:03 2017 +0000
@@ -291,8 +291,8 @@
next
case False
with assms show ?thesis
- using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
- by (auto simp add: residues_def gcd_int_def) force
+ using residues.euler_theorem [of "int m" "int a"] cong_int_iff
+ by (auto simp add: residues_def gcd_int_def) fastforce
qed
lemma fermat_theorem:
--- a/src/HOL/ROOT Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/ROOT Tue Oct 31 07:11:03 2017 +0000
@@ -590,7 +590,6 @@
Termination
ThreeDivides
Transfer_Debug
- Transfer_Ex
Transfer_Int_Nat
Transitive_Closure_Table_Ex
Tree23
--- a/src/HOL/ex/Transfer_Ex.thy Mon Oct 30 19:29:06 2017 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-
-section \<open>Various examples for transfer procedure\<close>
-
-theory Transfer_Ex
-imports Main Transfer_Int_Nat
-begin
-
-lemma ex1: "(x::nat) + y = y + x"
- by auto
-
-lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> x + y = y + x"
- by (fact ex1 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> x + y = y + x"
- by (fact ex1 [untransferred])
-
-lemma ex2: "(a::nat) div b * b + a mod b = a"
- by (rule div_mult_mod_eq)
-
-lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
- by (fact ex2 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (a::int) \<Longrightarrow> 0 \<le> (b::int) \<Longrightarrow> a div b * b + a mod b = a"
- by (fact ex2 [untransferred])
-
-lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
- by auto
-
-lemma "\<forall>x\<ge>0::int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
- by (fact ex3 [transferred nat_int])
-
-(* Using new transfer package *)
-lemma "\<forall>x::int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
- by (fact ex3 [untransferred])
-
-lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
- by auto
-
-lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
- by (fact ex4 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
- by (fact ex4 [untransferred])
-
-lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
- by (induct n rule: nat_induct, auto)
-
-lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
- by (fact ex5 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
- by (fact ex5 [untransferred])
-
-lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
- by (fact ex5 [transferred, transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
- by (fact ex5 [untransferred, Transfer.transferred])
-
-end
--- a/src/HOL/ex/Transfer_Int_Nat.thy Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Tue Oct 31 07:11:03 2017 +0000
@@ -39,13 +39,16 @@
unfolding rel_fun_def ZN_def by simp
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
- unfolding rel_fun_def ZN_def by (simp add: of_nat_mult)
+ unfolding rel_fun_def ZN_def by simp
+
+definition tsub :: "int \<Rightarrow> int \<Rightarrow> int"
+ where "tsub k l = max 0 (k - l)"
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
- unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff)
+ unfolding rel_fun_def ZN_def by (auto simp add: of_nat_diff tsub_def)
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
- unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
unfolding rel_fun_def ZN_def by simp
@@ -92,7 +95,7 @@
unfolding rel_fun_def ZN_def by (simp add: zmod_int)
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
- unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd)
+ unfolding rel_fun_def ZN_def by (simp add: gcd_int_def)
lemma ZN_atMost [transfer_rule]:
"(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"