diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Nat_Transfer.thy --- a/src/HOL/Nat_Transfer.thy Sun Oct 08 22:28:22 2017 +0200 +++ b/src/HOL/Nat_Transfer.thy Sun Oct 08 22:28:22 2017 +0200 @@ -3,7 +3,7 @@ section \Generic transfer machinery; specific transfer from nats to ints and back.\ theory Nat_Transfer -imports Int +imports Int Divides begin subsection \Generic transfer machinery\ @@ -21,7 +21,8 @@ text \set up transfer direction\ -lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" .. +lemma transfer_morphism_nat_int [no_atp]: + "transfer_morphism nat (op <= (0::int))" .. declare transfer_morphism_nat_int [transfer add mode: manual @@ -31,7 +32,7 @@ text \basic functions and relations\ -lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]: +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" @@ -46,15 +47,17 @@ lemma tsub_eq: "x >= y \ tsub x y = x - y" by (simp add: tsub_def) -lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]: +lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]: "(x::int) >= 0 \ y >= 0 \ (nat x) + (nat y) = nat (x + y)" "(x::int) >= 0 \ y >= 0 \ (nat x) * (nat y) = nat (x * y)" "(x::int) >= 0 \ y >= 0 \ (nat x) - (nat y) = nat (tsub x y)" "(x::int) >= 0 \ (nat x)^n = nat (x^n)" + "(x::int) >= 0 \ y >= 0 \ (nat x) div (nat y) = nat (x div y)" + "(x::int) >= 0 \ y >= 0 \ (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_power_eq tsub_def nat_div_distrib nat_mod_distrib) -lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]: +lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]: "(x::int) >= 0 \ y >= 0 \ x + y >= 0" "(x::int) >= 0 \ y >= 0 \ x * y >= 0" "(x::int) >= 0 \ y >= 0 \ tsub x y >= 0" @@ -64,9 +67,16 @@ "(2::int) >= 0" "(3::int) >= 0" "int z >= 0" - by (auto simp add: zero_le_mult_iff tsub_def) + "(x::int) >= 0 \ y >= 0 \ x div y >= 0" + "(x::int) >= 0 \ y >= 0 \ 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 [transfer key: transfer_morphism_nat_int]: +lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]: "x >= 0 \ y >= 0 \ (nat (x::int) = nat y) = (x = y)" "x >= 0 \ y >= 0 \ @@ -94,7 +104,7 @@ then show "\x. P x" by auto qed -lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]: +lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]: "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \ P (nat x))" "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))" by (rule all_nat, rule ex_nat) @@ -126,7 +136,7 @@ where "nat_set S = (ALL x:S. x >= 0)" -lemma transfer_nat_int_set_functions: +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)" @@ -144,7 +154,7 @@ apply auto done -lemma transfer_nat_int_set_function_closures: +lemma transfer_nat_int_set_function_closures [no_atp]: "nat_set {}" "nat_set A \ nat_set B \ nat_set (A Un B)" "nat_set A \ nat_set B \ nat_set (A Int B)" @@ -154,7 +164,7 @@ unfolding nat_set_def apply auto done -lemma transfer_nat_int_set_relations: +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)" @@ -169,11 +179,11 @@ apply (drule_tac x = "int x" in spec, auto) done -lemma transfer_nat_int_set_return_embed: "nat_set A \ +lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \ (int ` nat ` A = A)" by (auto simp add: nat_set_def image_def) -lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \ P x = P' x) \ +lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \ P x = P' x) \ {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}" by auto @@ -189,7 +199,7 @@ text \sum and prod\ (* this handles the case where the *domain* of f is nat *) -lemma transfer_nat_int_sum_prod: +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) @@ -199,14 +209,14 @@ done (* this handles the case where the *range* of f is nat *) -lemma transfer_nat_int_sum_prod2: +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: +lemma transfer_nat_int_sum_prod_closure [no_atp]: "nat_set A \ (!!x. x >= 0 \ f x >= (0::int)) \ sum f A >= 0" "nat_set A \ (!!x. x >= 0 \ f x >= (0::int)) \ prod f A >= 0" unfolding nat_set_def @@ -236,7 +246,7 @@ Also, why aren't sum.cong and prod.cong enough, with the previously mentioned rule turned on? *) -lemma transfer_nat_int_sum_prod_cong: +lemma transfer_nat_int_sum_prod_cong [no_atp]: "A = B \ nat_set B \ (!!x. x >= 0 \ f x = g x) \ sum f A = sum g B" "A = B \ nat_set B \ (!!x. x >= 0 \ f x = g x) \ @@ -257,7 +267,7 @@ text \set up transfer direction\ -lemma transfer_morphism_int_nat: "transfer_morphism int (\n. True)" .. +lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\n. True)" .. declare transfer_morphism_int_nat [transfer add mode: manual @@ -273,21 +283,23 @@ where "is_nat x = (x >= 0)" -lemma transfer_int_nat_numerals: +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: +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)" - by (auto simp add: tsub_def) + "(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: +lemma transfer_int_nat_function_closures [no_atp]: "is_nat x \ is_nat y \ is_nat (x + y)" "is_nat x \ is_nat y \ is_nat (x * y)" "is_nat x \ is_nat y \ is_nat (tsub x y)" @@ -297,9 +309,11 @@ "is_nat 2" "is_nat 3" "is_nat (int z)" + "is_nat x \ is_nat y \ is_nat (x div y)" + "is_nat x \ is_nat y \ is_nat (x mod y)" by (simp_all only: is_nat_def transfer_nat_int_function_closures) -lemma transfer_int_nat_relations: +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)" @@ -316,7 +330,7 @@ text \first-order quantifiers\ -lemma transfer_int_nat_quantifiers: +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) @@ -341,7 +355,7 @@ text \operations with sets\ -lemma transfer_int_nat_set_functions: +lemma transfer_int_nat_set_functions [no_atp]: "nat_set A \ card A = card (nat ` A)" "{} = int ` ({}::nat set)" "nat_set A \ nat_set B \ A Un B = int ` (nat ` A Un nat ` B)" @@ -353,7 +367,7 @@ transfer_nat_int_set_return_embed nat_0_le cong: transfer_nat_int_set_cong) -lemma transfer_int_nat_set_function_closures: +lemma transfer_int_nat_set_function_closures [no_atp]: "nat_set {}" "nat_set A \ nat_set B \ nat_set (A Un B)" "nat_set A \ nat_set B \ nat_set (A Int B)" @@ -362,7 +376,7 @@ "nat_set A \ x : A \ is_nat x" by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) -lemma transfer_int_nat_set_relations: +lemma transfer_int_nat_set_relations [no_atp]: "nat_set A \ finite A = finite (nat ` A)" "is_nat x \ nat_set A \ (x : A) = (nat x : nat ` A)" "nat_set A \ nat_set B \ (A = B) = (nat ` A = nat ` B)" @@ -371,12 +385,12 @@ 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: "nat ` int ` A = A" +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: "(!!x. P x = P' x) \ +lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \ {(x::nat). P x} = {x. P' x}" by auto @@ -392,7 +406,7 @@ text \sum and prod\ (* this handles the case where the *domain* of f is int *) -lemma transfer_int_nat_sum_prod: +lemma transfer_int_nat_sum_prod [no_atp]: "nat_set A \ sum f A = sum (%x. f (int x)) (nat ` A)" "nat_set A \ prod f A = prod (%x. f (int x)) (nat ` A)" apply (subst sum.reindex) @@ -403,7 +417,7 @@ done (* this handles the case where the *range* of f is int *) -lemma transfer_int_nat_sum_prod2: +lemma transfer_int_nat_sum_prod2 [no_atp]: "(!!x. x:A \ is_nat (f x)) \ sum f A = int(sum (%x. nat (f x)) A)" "(!!x. x:A \ is_nat (f x)) \ prod f A = int(prod (%x. nat (f x)) A)" @@ -414,4 +428,6 @@ 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] + end