huffman@31708: haftmann@32554: (* Authors: Jeremy Avigad and Amine Chaieb *) huffman@31708: haftmann@32554: header {* Sets up transfer from nats to ints and back. *} huffman@31708: huffman@31708: theory NatTransfer huffman@31708: imports Main Parity huffman@31708: begin huffman@31708: huffman@31708: subsection {* Set up transfer from nat to int *} huffman@31708: huffman@31708: (* set up transfer direction *) huffman@31708: huffman@31708: lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))" huffman@31708: by (simp add: TransferMorphism_def) huffman@31708: huffman@31708: declare TransferMorphism_nat_int[transfer huffman@31708: add mode: manual huffman@31708: return: nat_0_le huffman@31708: labels: natint huffman@31708: ] huffman@31708: huffman@31708: (* basic functions and relations *) huffman@31708: huffman@31708: lemma transfer_nat_int_numerals: huffman@31708: "(0::nat) = nat 0" huffman@31708: "(1::nat) = nat 1" huffman@31708: "(2::nat) = nat 2" huffman@31708: "(3::nat) = nat 3" huffman@31708: by auto huffman@31708: huffman@31708: definition huffman@31708: tsub :: "int \ int \ int" huffman@31708: where huffman@31708: "tsub x y = (if x >= y then x - y else 0)" huffman@31708: huffman@31708: lemma tsub_eq: "x >= y \ tsub x y = x - y" huffman@31708: by (simp add: tsub_def) huffman@31708: huffman@31708: huffman@31708: lemma transfer_nat_int_functions: huffman@31708: "(x::int) >= 0 \ y >= 0 \ (nat x) + (nat y) = nat (x + y)" huffman@31708: "(x::int) >= 0 \ y >= 0 \ (nat x) * (nat y) = nat (x * y)" huffman@31708: "(x::int) >= 0 \ y >= 0 \ (nat x) - (nat y) = nat (tsub x y)" huffman@31708: "(x::int) >= 0 \ (nat x)^n = nat (x^n)" huffman@31708: "(x::int) >= 0 \ y >= 0 \ (nat x) div (nat y) = nat (x div y)" huffman@31708: "(x::int) >= 0 \ y >= 0 \ (nat x) mod (nat y) = nat (x mod y)" huffman@31708: by (auto simp add: eq_nat_nat_iff nat_mult_distrib huffman@31708: nat_power_eq nat_div_distrib nat_mod_distrib tsub_def) huffman@31708: huffman@31708: lemma transfer_nat_int_function_closures: huffman@31708: "(x::int) >= 0 \ y >= 0 \ x + y >= 0" huffman@31708: "(x::int) >= 0 \ y >= 0 \ x * y >= 0" huffman@31708: "(x::int) >= 0 \ y >= 0 \ tsub x y >= 0" huffman@31708: "(x::int) >= 0 \ x^n >= 0" huffman@31708: "(x::int) >= 0 \ y >= 0 \ x div y >= 0" huffman@31708: "(x::int) >= 0 \ y >= 0 \ x mod y >= 0" huffman@31708: "(0::int) >= 0" huffman@31708: "(1::int) >= 0" huffman@31708: "(2::int) >= 0" huffman@31708: "(3::int) >= 0" huffman@31708: "int z >= 0" huffman@31708: apply (auto simp add: zero_le_mult_iff tsub_def) huffman@31708: apply (case_tac "y = 0") huffman@31708: apply auto huffman@31708: apply (subst pos_imp_zdiv_nonneg_iff, auto) huffman@31708: apply (case_tac "y = 0") huffman@31708: apply force huffman@31708: apply (rule pos_mod_sign) huffman@31708: apply arith huffman@31708: done huffman@31708: huffman@31708: lemma transfer_nat_int_relations: huffman@31708: "x >= 0 \ y >= 0 \ huffman@31708: (nat (x::int) = nat y) = (x = y)" huffman@31708: "x >= 0 \ y >= 0 \ huffman@31708: (nat (x::int) < nat y) = (x < y)" huffman@31708: "x >= 0 \ y >= 0 \ huffman@31708: (nat (x::int) <= nat y) = (x <= y)" huffman@31708: "x >= 0 \ y >= 0 \ huffman@31708: (nat (x::int) dvd nat y) = (x dvd y)" huffman@31708: by (auto simp add: zdvd_int even_nat_def) huffman@31708: huffman@31708: declare TransferMorphism_nat_int[transfer add return: huffman@31708: transfer_nat_int_numerals huffman@31708: transfer_nat_int_functions huffman@31708: transfer_nat_int_function_closures huffman@31708: transfer_nat_int_relations huffman@31708: ] huffman@31708: huffman@31708: huffman@31708: (* first-order quantifiers *) huffman@31708: huffman@31708: lemma transfer_nat_int_quantifiers: huffman@31708: "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \ P (nat x))" huffman@31708: "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))" huffman@31708: by (rule all_nat, rule ex_nat) huffman@31708: huffman@31708: (* should we restrict these? *) huffman@31708: lemma all_cong: "(\x. Q x \ P x = P' x) \ huffman@31708: (ALL x. Q x \ P x) = (ALL x. Q x \ P' x)" huffman@31708: by auto huffman@31708: huffman@31708: lemma ex_cong: "(\x. Q x \ P x = P' x) \ huffman@31708: (EX x. Q x \ P x) = (EX x. Q x \ P' x)" huffman@31708: by auto huffman@31708: huffman@31708: declare TransferMorphism_nat_int[transfer add huffman@31708: return: transfer_nat_int_quantifiers huffman@31708: cong: all_cong ex_cong] huffman@31708: huffman@31708: huffman@31708: (* if *) huffman@31708: huffman@31708: lemma nat_if_cong: "(if P then (nat x) else (nat y)) = huffman@31708: nat (if P then x else y)" huffman@31708: by auto huffman@31708: huffman@31708: declare TransferMorphism_nat_int [transfer add return: nat_if_cong] huffman@31708: huffman@31708: huffman@31708: (* operations with sets *) huffman@31708: huffman@31708: definition huffman@31708: nat_set :: "int set \ bool" huffman@31708: where huffman@31708: "nat_set S = (ALL x:S. x >= 0)" huffman@31708: huffman@31708: lemma transfer_nat_int_set_functions: huffman@31708: "card A = card (int ` A)" huffman@31708: "{} = nat ` ({}::int set)" huffman@31708: "A Un B = nat ` (int ` A Un int ` B)" huffman@31708: "A Int B = nat ` (int ` A Int int ` B)" huffman@31708: "{x. P x} = nat ` {x. x >= 0 & P(nat x)}" huffman@31708: "{..n} = nat ` {0..int n}" huffman@31708: "{m..n} = nat ` {int m..int n}" (* need all variants of these! *) huffman@31708: apply (rule card_image [symmetric]) huffman@31708: apply (auto simp add: inj_on_def image_def) huffman@31708: apply (rule_tac x = "int x" in bexI) huffman@31708: apply auto huffman@31708: apply (rule_tac x = "int x" in bexI) huffman@31708: apply auto huffman@31708: apply (rule_tac x = "int x" in bexI) huffman@31708: apply auto huffman@31708: apply (rule_tac x = "int x" in exI) huffman@31708: apply auto huffman@31708: apply (rule_tac x = "int x" in bexI) huffman@31708: apply auto huffman@31708: apply (rule_tac x = "int x" in bexI) huffman@31708: apply auto huffman@31708: done huffman@31708: huffman@31708: lemma transfer_nat_int_set_function_closures: huffman@31708: "nat_set {}" huffman@31708: "nat_set A \ nat_set B \ nat_set (A Un B)" huffman@31708: "nat_set A \ nat_set B \ nat_set (A Int B)" huffman@31708: "x >= 0 \ nat_set {x..y}" huffman@31708: "nat_set {x. x >= 0 & P x}" huffman@31708: "nat_set (int ` C)" huffman@31708: "nat_set A \ x : A \ x >= 0" (* does it hurt to turn this on? *) huffman@31708: unfolding nat_set_def apply auto huffman@31708: done huffman@31708: huffman@31708: lemma transfer_nat_int_set_relations: huffman@31708: "(finite A) = (finite (int ` A))" huffman@31708: "(x : A) = (int x : int ` A)" huffman@31708: "(A = B) = (int ` A = int ` B)" huffman@31708: "(A < B) = (int ` A < int ` B)" huffman@31708: "(A <= B) = (int ` A <= int ` B)" huffman@31708: huffman@31708: apply (rule iffI) huffman@31708: apply (erule finite_imageI) huffman@31708: apply (erule finite_imageD) huffman@31708: apply (auto simp add: image_def expand_set_eq inj_on_def) huffman@31708: apply (drule_tac x = "int x" in spec, auto) huffman@31708: apply (drule_tac x = "int x" in spec, auto) huffman@31708: apply (drule_tac x = "int x" in spec, auto) huffman@31708: done huffman@31708: huffman@31708: lemma transfer_nat_int_set_return_embed: "nat_set A \ huffman@31708: (int ` nat ` A = A)" huffman@31708: by (auto simp add: nat_set_def image_def) huffman@31708: huffman@31708: lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \ P x = P' x) \ huffman@31708: {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}" huffman@31708: by auto huffman@31708: huffman@31708: declare TransferMorphism_nat_int[transfer add huffman@31708: return: transfer_nat_int_set_functions huffman@31708: transfer_nat_int_set_function_closures huffman@31708: transfer_nat_int_set_relations huffman@31708: transfer_nat_int_set_return_embed huffman@31708: cong: transfer_nat_int_set_cong huffman@31708: ] huffman@31708: huffman@31708: huffman@31708: (* setsum and setprod *) huffman@31708: huffman@31708: (* this handles the case where the *domain* of f is nat *) huffman@31708: lemma transfer_nat_int_sum_prod: huffman@31708: "setsum f A = setsum (%x. f (nat x)) (int ` A)" huffman@31708: "setprod f A = setprod (%x. f (nat x)) (int ` A)" huffman@31708: apply (subst setsum_reindex) huffman@31708: apply (unfold inj_on_def, auto) huffman@31708: apply (subst setprod_reindex) huffman@31708: apply (unfold inj_on_def o_def, auto) huffman@31708: done huffman@31708: huffman@31708: (* this handles the case where the *range* of f is nat *) huffman@31708: lemma transfer_nat_int_sum_prod2: huffman@31708: "setsum f A = nat(setsum (%x. int (f x)) A)" huffman@31708: "setprod f A = nat(setprod (%x. int (f x)) A)" huffman@31708: apply (subst int_setsum [symmetric]) huffman@31708: apply auto huffman@31708: apply (subst int_setprod [symmetric]) huffman@31708: apply auto huffman@31708: done huffman@31708: huffman@31708: lemma transfer_nat_int_sum_prod_closure: huffman@31708: "nat_set A \ (!!x. x >= 0 \ f x >= (0::int)) \ setsum f A >= 0" huffman@31708: "nat_set A \ (!!x. x >= 0 \ f x >= (0::int)) \ setprod f A >= 0" huffman@31708: unfolding nat_set_def huffman@31708: apply (rule setsum_nonneg) huffman@31708: apply auto huffman@31708: apply (rule setprod_nonneg) huffman@31708: apply auto huffman@31708: done huffman@31708: huffman@31708: (* this version doesn't work, even with nat_set A \ huffman@31708: x : A \ x >= 0 turned on. Why not? huffman@31708: huffman@31708: also: what does =simp=> do? huffman@31708: huffman@31708: lemma transfer_nat_int_sum_prod_closure: huffman@31708: "(!!x. x : A ==> f x >= (0::int)) \ setsum f A >= 0" huffman@31708: "(!!x. x : A ==> f x >= (0::int)) \ setprod f A >= 0" huffman@31708: unfolding nat_set_def simp_implies_def huffman@31708: apply (rule setsum_nonneg) huffman@31708: apply auto huffman@31708: apply (rule setprod_nonneg) huffman@31708: apply auto huffman@31708: done huffman@31708: *) huffman@31708: huffman@31708: (* Making A = B in this lemma doesn't work. Why not? huffman@31708: Also, why aren't setsum_cong and setprod_cong enough, huffman@31708: with the previously mentioned rule turned on? *) huffman@31708: huffman@31708: lemma transfer_nat_int_sum_prod_cong: huffman@31708: "A = B \ nat_set B \ (!!x. x >= 0 \ f x = g x) \ huffman@31708: setsum f A = setsum g B" huffman@31708: "A = B \ nat_set B \ (!!x. x >= 0 \ f x = g x) \ huffman@31708: setprod f A = setprod g B" huffman@31708: unfolding nat_set_def huffman@31708: apply (subst setsum_cong, assumption) huffman@31708: apply auto [2] huffman@31708: apply (subst setprod_cong, assumption, auto) huffman@31708: done huffman@31708: huffman@31708: declare TransferMorphism_nat_int[transfer add huffman@31708: return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2 huffman@31708: transfer_nat_int_sum_prod_closure huffman@31708: cong: transfer_nat_int_sum_prod_cong] huffman@31708: huffman@31708: (* lists *) huffman@31708: huffman@31708: definition huffman@31708: embed_list :: "nat list \ int list" huffman@31708: where huffman@31708: "embed_list l = map int l"; huffman@31708: huffman@31708: definition huffman@31708: nat_list :: "int list \ bool" huffman@31708: where huffman@31708: "nat_list l = nat_set (set l)"; huffman@31708: huffman@31708: definition huffman@31708: return_list :: "int list \ nat list" huffman@31708: where huffman@31708: "return_list l = map nat l"; huffman@31708: huffman@31708: thm nat_0_le; huffman@31708: huffman@31708: lemma transfer_nat_int_list_return_embed: "nat_list l \ huffman@31708: embed_list (return_list l) = l"; huffman@31708: unfolding embed_list_def return_list_def nat_list_def nat_set_def huffman@31708: apply (induct l); huffman@31708: apply auto; huffman@31708: done; huffman@31708: huffman@31708: lemma transfer_nat_int_list_functions: huffman@31708: "l @ m = return_list (embed_list l @ embed_list m)" huffman@31708: "[] = return_list []"; huffman@31708: unfolding return_list_def embed_list_def; huffman@31708: apply auto; huffman@31708: apply (induct l, auto); huffman@31708: apply (induct m, auto); huffman@31708: done; huffman@31708: huffman@31708: (* huffman@31708: lemma transfer_nat_int_fold1: "fold f l x = huffman@31708: fold (%x. f (nat x)) (embed_list l) x"; huffman@31708: *) huffman@31708: huffman@31708: huffman@31708: huffman@31708: huffman@31708: subsection {* Set up transfer from int to nat *} huffman@31708: huffman@31708: (* set up transfer direction *) huffman@31708: huffman@31708: lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)" huffman@31708: by (simp add: TransferMorphism_def) huffman@31708: huffman@31708: declare TransferMorphism_int_nat[transfer add huffman@31708: mode: manual huffman@31708: (* labels: int-nat *) huffman@31708: return: nat_int huffman@31708: ] huffman@31708: huffman@31708: huffman@31708: (* basic functions and relations *) huffman@31708: huffman@31708: definition huffman@31708: is_nat :: "int \ bool" huffman@31708: where huffman@31708: "is_nat x = (x >= 0)" huffman@31708: huffman@31708: lemma transfer_int_nat_numerals: huffman@31708: "0 = int 0" huffman@31708: "1 = int 1" huffman@31708: "2 = int 2" huffman@31708: "3 = int 3" huffman@31708: by auto huffman@31708: huffman@31708: lemma transfer_int_nat_functions: huffman@31708: "(int x) + (int y) = int (x + y)" huffman@31708: "(int x) * (int y) = int (x * y)" huffman@31708: "tsub (int x) (int y) = int (x - y)" huffman@31708: "(int x)^n = int (x^n)" huffman@31708: "(int x) div (int y) = int (x div y)" huffman@31708: "(int x) mod (int y) = int (x mod y)" huffman@31708: by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int) huffman@31708: huffman@31708: lemma transfer_int_nat_function_closures: huffman@31708: "is_nat x \ is_nat y \ is_nat (x + y)" huffman@31708: "is_nat x \ is_nat y \ is_nat (x * y)" huffman@31708: "is_nat x \ is_nat y \ is_nat (tsub x y)" huffman@31708: "is_nat x \ is_nat (x^n)" huffman@31708: "is_nat x \ is_nat y \ is_nat (x div y)" huffman@31708: "is_nat x \ is_nat y \ is_nat (x mod y)" huffman@31708: "is_nat 0" huffman@31708: "is_nat 1" huffman@31708: "is_nat 2" huffman@31708: "is_nat 3" huffman@31708: "is_nat (int z)" huffman@31708: by (simp_all only: is_nat_def transfer_nat_int_function_closures) huffman@31708: huffman@31708: lemma transfer_int_nat_relations: huffman@31708: "(int x = int y) = (x = y)" huffman@31708: "(int x < int y) = (x < y)" huffman@31708: "(int x <= int y) = (x <= y)" huffman@31708: "(int x dvd int y) = (x dvd y)" huffman@31708: "(even (int x)) = (even x)" huffman@31708: by (auto simp add: zdvd_int even_nat_def) huffman@31708: haftmann@32121: lemma UNIV_apply: haftmann@32121: "UNIV x = True" haftmann@32264: by (simp add: top_fun_eq top_bool_eq) haftmann@32121: huffman@31708: declare TransferMorphism_int_nat[transfer add return: huffman@31708: transfer_int_nat_numerals huffman@31708: transfer_int_nat_functions huffman@31708: transfer_int_nat_function_closures huffman@31708: transfer_int_nat_relations haftmann@32121: UNIV_apply huffman@31708: ] huffman@31708: huffman@31708: huffman@31708: (* first-order quantifiers *) huffman@31708: huffman@31708: lemma transfer_int_nat_quantifiers: huffman@31708: "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))" huffman@31708: "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))" huffman@31708: apply (subst all_nat) huffman@31708: apply auto [1] huffman@31708: apply (subst ex_nat) huffman@31708: apply auto huffman@31708: done huffman@31708: huffman@31708: declare TransferMorphism_int_nat[transfer add huffman@31708: return: transfer_int_nat_quantifiers] huffman@31708: huffman@31708: huffman@31708: (* if *) huffman@31708: huffman@31708: lemma int_if_cong: "(if P then (int x) else (int y)) = huffman@31708: int (if P then x else y)" huffman@31708: by auto huffman@31708: huffman@31708: declare TransferMorphism_int_nat [transfer add return: int_if_cong] huffman@31708: huffman@31708: huffman@31708: huffman@31708: (* operations with sets *) huffman@31708: huffman@31708: lemma transfer_int_nat_set_functions: huffman@31708: "nat_set A \ card A = card (nat ` A)" huffman@31708: "{} = int ` ({}::nat set)" huffman@31708: "nat_set A \ nat_set B \ A Un B = int ` (nat ` A Un nat ` B)" huffman@31708: "nat_set A \ nat_set B \ A Int B = int ` (nat ` A Int nat ` B)" huffman@31708: "{x. x >= 0 & P x} = int ` {x. P(int x)}" huffman@31708: "is_nat m \ is_nat n \ {m..n} = int ` {nat m..nat n}" huffman@31708: (* need all variants of these! *) huffman@31708: by (simp_all only: is_nat_def transfer_nat_int_set_functions huffman@31708: transfer_nat_int_set_function_closures huffman@31708: transfer_nat_int_set_return_embed nat_0_le huffman@31708: cong: transfer_nat_int_set_cong) huffman@31708: huffman@31708: lemma transfer_int_nat_set_function_closures: huffman@31708: "nat_set {}" huffman@31708: "nat_set A \ nat_set B \ nat_set (A Un B)" huffman@31708: "nat_set A \ nat_set B \ nat_set (A Int B)" huffman@31708: "is_nat x \ nat_set {x..y}" huffman@31708: "nat_set {x. x >= 0 & P x}" huffman@31708: "nat_set (int ` C)" huffman@31708: "nat_set A \ x : A \ is_nat x" huffman@31708: by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) huffman@31708: huffman@31708: lemma transfer_int_nat_set_relations: huffman@31708: "nat_set A \ finite A = finite (nat ` A)" huffman@31708: "is_nat x \ nat_set A \ (x : A) = (nat x : nat ` A)" huffman@31708: "nat_set A \ nat_set B \ (A = B) = (nat ` A = nat ` B)" huffman@31708: "nat_set A \ nat_set B \ (A < B) = (nat ` A < nat ` B)" huffman@31708: "nat_set A \ nat_set B \ (A <= B) = (nat ` A <= nat ` B)" huffman@31708: by (simp_all only: is_nat_def transfer_nat_int_set_relations huffman@31708: transfer_nat_int_set_return_embed nat_0_le) huffman@31708: huffman@31708: lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A" huffman@31708: by (simp only: transfer_nat_int_set_relations huffman@31708: transfer_nat_int_set_function_closures huffman@31708: transfer_nat_int_set_return_embed nat_0_le) huffman@31708: huffman@31708: lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \ huffman@31708: {(x::nat). P x} = {x. P' x}" huffman@31708: by auto huffman@31708: huffman@31708: declare TransferMorphism_int_nat[transfer add huffman@31708: return: transfer_int_nat_set_functions huffman@31708: transfer_int_nat_set_function_closures huffman@31708: transfer_int_nat_set_relations huffman@31708: transfer_int_nat_set_return_embed huffman@31708: cong: transfer_int_nat_set_cong huffman@31708: ] huffman@31708: huffman@31708: huffman@31708: (* setsum and setprod *) huffman@31708: huffman@31708: (* this handles the case where the *domain* of f is int *) huffman@31708: lemma transfer_int_nat_sum_prod: huffman@31708: "nat_set A \ setsum f A = setsum (%x. f (int x)) (nat ` A)" huffman@31708: "nat_set A \ setprod f A = setprod (%x. f (int x)) (nat ` A)" huffman@31708: apply (subst setsum_reindex) huffman@31708: apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff) huffman@31708: apply (subst setprod_reindex) huffman@31708: apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff huffman@31708: cong: setprod_cong) huffman@31708: done huffman@31708: huffman@31708: (* this handles the case where the *range* of f is int *) huffman@31708: lemma transfer_int_nat_sum_prod2: huffman@31708: "(!!x. x:A \ is_nat (f x)) \ setsum f A = int(setsum (%x. nat (f x)) A)" huffman@31708: "(!!x. x:A \ is_nat (f x)) \ huffman@31708: setprod f A = int(setprod (%x. nat (f x)) A)" huffman@31708: unfolding is_nat_def huffman@31708: apply (subst int_setsum, auto) huffman@31708: apply (subst int_setprod, auto simp add: cong: setprod_cong) huffman@31708: done huffman@31708: huffman@31708: declare TransferMorphism_int_nat[transfer add huffman@31708: return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2 huffman@31708: cong: setsum_cong setprod_cong] huffman@31708: huffman@31708: end