src/HOL/ex/Transfer_Int_Nat.thy
 author nipkow Thu Sep 15 11:48:20 2016 +0200 (2016-09-15) changeset 63882 018998c00003 parent 63343 fb5d8a50c641 child 64267 b9a1486e79be permissions -rw-r--r--
renamed listsum -> sum_list, listprod ~> prod_list
 huffman@47654 ` 1` ```(* Title: HOL/ex/Transfer_Int_Nat.thy ``` huffman@47654 ` 2` ``` Author: Brian Huffman, TU Muenchen ``` huffman@47654 ` 3` ```*) ``` huffman@47654 ` 4` wenzelm@61343 ` 5` ```section \Using the transfer method between nat and int\ ``` huffman@47654 ` 6` huffman@47654 ` 7` ```theory Transfer_Int_Nat ``` kuncar@53013 ` 8` ```imports GCD ``` huffman@47654 ` 9` ```begin ``` huffman@47654 ` 10` wenzelm@61343 ` 11` ```subsection \Correspondence relation\ ``` huffman@47654 ` 12` huffman@47654 ` 13` ```definition ZN :: "int \ nat \ bool" ``` huffman@47654 ` 14` ``` where "ZN = (\z n. z = of_nat n)" ``` huffman@47654 ` 15` wenzelm@61343 ` 16` ```subsection \Transfer domain rules\ ``` kuncar@51956 ` 17` kuncar@51956 ` 18` ```lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\x. x \ 0)" ``` kuncar@51956 ` 19` ``` unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int) ``` kuncar@51956 ` 20` wenzelm@61343 ` 21` ```subsection \Transfer rules\ ``` huffman@47654 ` 22` wenzelm@63343 ` 23` ```context includes lifting_syntax ``` kuncar@53013 ` 24` ```begin ``` kuncar@53013 ` 25` huffman@47654 ` 26` ```lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN" ``` huffman@47654 ` 27` ``` unfolding ZN_def bi_unique_def by simp ``` huffman@47654 ` 28` huffman@47654 ` 29` ```lemma right_total_ZN [transfer_rule]: "right_total ZN" ``` huffman@47654 ` 30` ``` unfolding ZN_def right_total_def by simp ``` huffman@47654 ` 31` huffman@47654 ` 32` ```lemma ZN_0 [transfer_rule]: "ZN 0 0" ``` huffman@47654 ` 33` ``` unfolding ZN_def by simp ``` huffman@47654 ` 34` huffman@47654 ` 35` ```lemma ZN_1 [transfer_rule]: "ZN 1 1" ``` huffman@47654 ` 36` ``` unfolding ZN_def by simp ``` huffman@47654 ` 37` huffman@47654 ` 38` ```lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)" ``` blanchet@55945 ` 39` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 40` huffman@47654 ` 41` ```lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)" ``` haftmann@62348 ` 42` ``` unfolding rel_fun_def ZN_def by (simp add: of_nat_mult) ``` huffman@47654 ` 43` huffman@47654 ` 44` ```lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)" ``` haftmann@62348 ` 45` ``` unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff) ``` huffman@47654 ` 46` huffman@47654 ` 47` ```lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)" ``` lp15@61649 ` 48` ``` unfolding rel_fun_def ZN_def by (simp add: of_nat_power) ``` huffman@47654 ` 49` huffman@47654 ` 50` ```lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id" ``` blanchet@55945 ` 51` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 52` huffman@47654 ` 53` ```lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int" ``` blanchet@55945 ` 54` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 55` huffman@47654 ` 56` ```lemma ZN_All [transfer_rule]: ``` huffman@47654 ` 57` ``` "((ZN ===> op =) ===> op =) (Ball {0..}) All" ``` blanchet@55945 ` 58` ``` unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int) ``` huffman@47654 ` 59` huffman@47654 ` 60` ```lemma ZN_transfer_forall [transfer_rule]: ``` huffman@47654 ` 61` ``` "((ZN ===> op =) ===> op =) (transfer_bforall (\x. 0 \ x)) transfer_forall" ``` huffman@47654 ` 62` ``` unfolding transfer_forall_def transfer_bforall_def ``` blanchet@55945 ` 63` ``` unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int) ``` huffman@47654 ` 64` huffman@47654 ` 65` ```lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex" ``` blanchet@55945 ` 66` ``` unfolding rel_fun_def ZN_def Bex_def atLeast_iff ``` haftmann@62348 ` 67` ``` by (metis zero_le_imp_eq_int of_nat_0_le_iff) ``` huffman@47654 ` 68` huffman@47654 ` 69` ```lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \) (op \)" ``` blanchet@55945 ` 70` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 71` huffman@47654 ` 72` ```lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)" ``` blanchet@55945 ` 73` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 74` huffman@47654 ` 75` ```lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)" ``` blanchet@55945 ` 76` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 77` huffman@47654 ` 78` ```lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\x. x + 1) Suc" ``` blanchet@55945 ` 79` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 80` huffman@47654 ` 81` ```lemma ZN_numeral [transfer_rule]: ``` huffman@47654 ` 82` ``` "(op = ===> ZN) numeral numeral" ``` blanchet@55945 ` 83` ``` unfolding rel_fun_def ZN_def by simp ``` huffman@47654 ` 84` huffman@47654 ` 85` ```lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)" ``` blanchet@55945 ` 86` ``` unfolding rel_fun_def ZN_def by (simp add: zdvd_int) ``` huffman@47654 ` 87` huffman@47654 ` 88` ```lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)" ``` blanchet@55945 ` 89` ``` unfolding rel_fun_def ZN_def by (simp add: zdiv_int) ``` huffman@47654 ` 90` huffman@47654 ` 91` ```lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)" ``` blanchet@55945 ` 92` ``` unfolding rel_fun_def ZN_def by (simp add: zmod_int) ``` huffman@47654 ` 93` huffman@47654 ` 94` ```lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" ``` blanchet@55945 ` 95` ``` unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd) ``` huffman@47654 ` 96` huffman@52360 ` 97` ```lemma ZN_atMost [transfer_rule]: ``` blanchet@55938 ` 98` ``` "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost" ``` blanchet@55945 ` 99` ``` unfolding rel_fun_def ZN_def rel_set_def ``` huffman@52360 ` 100` ``` by (clarsimp simp add: Bex_def, arith) ``` huffman@52360 ` 101` huffman@52360 ` 102` ```lemma ZN_atLeastAtMost [transfer_rule]: ``` blanchet@55938 ` 103` ``` "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost" ``` blanchet@55945 ` 104` ``` unfolding rel_fun_def ZN_def rel_set_def ``` huffman@52360 ` 105` ``` by (clarsimp simp add: Bex_def, arith) ``` huffman@52360 ` 106` huffman@52360 ` 107` ```lemma ZN_setsum [transfer_rule]: ``` blanchet@55938 ` 108` ``` "bi_unique A \ ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum" ``` blanchet@55945 ` 109` ``` apply (intro rel_funI) ``` blanchet@55938 ` 110` ``` apply (erule (1) bi_unique_rel_set_lemma) ``` blanchet@55945 ` 111` ``` apply (simp add: setsum.reindex int_setsum ZN_def rel_fun_def) ``` haftmann@57418 ` 112` ``` apply (rule setsum.cong) ``` haftmann@57418 ` 113` ``` apply simp_all ``` huffman@52360 ` 114` ``` done ``` huffman@52360 ` 115` wenzelm@61933 ` 116` ```text \For derived operations, we can use the \transfer_prover\ ``` wenzelm@61343 ` 117` ``` method to help generate transfer rules.\ ``` huffman@47654 ` 118` nipkow@63882 ` 119` ```lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list" ``` haftmann@58320 ` 120` ``` by transfer_prover ``` huffman@47654 ` 121` kuncar@53013 ` 122` ```end ``` kuncar@53013 ` 123` wenzelm@61343 ` 124` ```subsection \Transfer examples\ ``` huffman@47654 ` 125` huffman@47654 ` 126` ```lemma ``` huffman@47654 ` 127` ``` assumes "\i::int. 0 \ i \ i + 0 = i" ``` huffman@47654 ` 128` ``` shows "\i::nat. i + 0 = i" ``` huffman@47654 ` 129` ```apply transfer ``` huffman@47654 ` 130` ```apply fact ``` huffman@47654 ` 131` ```done ``` huffman@47654 ` 132` huffman@47654 ` 133` ```lemma ``` huffman@47654 ` 134` ``` assumes "\i k::int. \0 \ i; 0 \ k; i < k\ \ \j\{0..}. i + j = k" ``` huffman@47654 ` 135` ``` shows "\i k::nat. i < k \ \j. i + j = k" ``` huffman@47654 ` 136` ```apply transfer ``` huffman@47654 ` 137` ```apply fact ``` huffman@47654 ` 138` ```done ``` huffman@47654 ` 139` huffman@47654 ` 140` ```lemma ``` huffman@47654 ` 141` ``` assumes "\x\{0::int..}. \y\{0..}. x * y div y = x" ``` huffman@47654 ` 142` ``` shows "\x y :: nat. x * y div y = x" ``` huffman@47654 ` 143` ```apply transfer ``` huffman@47654 ` 144` ```apply fact ``` huffman@47654 ` 145` ```done ``` huffman@47654 ` 146` huffman@47654 ` 147` ```lemma ``` huffman@47654 ` 148` ``` assumes "\m n::int. \0 \ m; 0 \ n; m * n = 0\ \ m = 0 \ n = 0" ``` huffman@47654 ` 149` ``` shows "m * n = (0::nat) \ m = 0 \ n = 0" ``` huffman@47654 ` 150` ```apply transfer ``` huffman@47654 ` 151` ```apply fact ``` huffman@47654 ` 152` ```done ``` huffman@47654 ` 153` huffman@47654 ` 154` ```lemma ``` huffman@47654 ` 155` ``` assumes "\x\{0::int..}. \y\{0..}. \z\{0..}. x + 3 * y = 5 * z" ``` huffman@47654 ` 156` ``` shows "\x::nat. \y z. x + 3 * y = 5 * z" ``` huffman@47654 ` 157` ```apply transfer ``` huffman@47654 ` 158` ```apply fact ``` huffman@47654 ` 159` ```done ``` huffman@47654 ` 160` wenzelm@61933 ` 161` ```text \The \fixing\ option prevents generalization over the free ``` wenzelm@61933 ` 162` ``` variable \n\, allowing the local transfer rule to be used.\ ``` huffman@47654 ` 163` huffman@47654 ` 164` ```lemma ``` huffman@47654 ` 165` ``` assumes [transfer_rule]: "ZN x n" ``` huffman@47654 ` 166` ``` assumes "\i\{0..}. i < x \ 2 * i < 3 * x" ``` huffman@47654 ` 167` ``` shows "\i. i < n \ 2 * i < 3 * n" ``` huffman@47654 ` 168` ```apply (transfer fixing: n) ``` huffman@47654 ` 169` ```apply fact ``` huffman@47654 ` 170` ```done ``` huffman@47654 ` 171` huffman@47654 ` 172` ```lemma ``` huffman@47654 ` 173` ``` assumes "gcd (2^i) (3^j) = (1::int)" ``` huffman@47654 ` 174` ``` shows "gcd (2^i) (3^j) = (1::nat)" ``` huffman@47654 ` 175` ```apply (transfer fixing: i j) ``` huffman@47654 ` 176` ```apply fact ``` huffman@47654 ` 177` ```done ``` huffman@47654 ` 178` huffman@47654 ` 179` ```lemma ``` huffman@47654 ` 180` ``` assumes "\x y z::int. \0 \ x; 0 \ y; 0 \ z\ \ ``` nipkow@63882 ` 181` ``` sum_list [x, y, z] = 0 \ list_all (\x. x = 0) [x, y, z]" ``` nipkow@63882 ` 182` ``` shows "sum_list [x, y, z] = (0::nat) \ list_all (\x. x = 0) [x, y, z]" ``` huffman@47654 ` 183` ```apply transfer ``` huffman@47654 ` 184` ```apply fact ``` huffman@47654 ` 185` ```done ``` huffman@47654 ` 186` wenzelm@61933 ` 187` ```text \Quantifiers over higher types (e.g. \nat list\) are ``` wenzelm@61343 ` 188` ``` transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\ ``` huffman@47654 ` 189` huffman@47654 ` 190` ```lemma ``` kuncar@51956 ` 191` ``` assumes "\xs::int list. list_all (\x. x \ 0) xs \ ``` nipkow@63882 ` 192` ``` (sum_list xs = 0) = list_all (\x. x = 0) xs" ``` nipkow@63882 ` 193` ``` shows "sum_list xs = (0::nat) \ list_all (\x. x = 0) xs" ``` huffman@47654 ` 194` ```apply transfer ``` huffman@47654 ` 195` ```apply fact ``` huffman@47654 ` 196` ```done ``` huffman@47654 ` 197` wenzelm@61343 ` 198` ```text \Equality on a higher type can be transferred if the relations ``` wenzelm@61343 ` 199` ``` involved are bi-unique.\ ``` huffman@47654 ` 200` huffman@47654 ` 201` ```lemma ``` wenzelm@61076 ` 202` ``` assumes "\xs::int list. \list_all (\x. x \ 0) xs; xs \ []\ \ ``` nipkow@63882 ` 203` ``` sum_list xs < sum_list (map (\x. x + 1) xs)" ``` nipkow@63882 ` 204` ``` shows "xs \ [] \ sum_list xs < sum_list (map Suc xs)" ``` huffman@47654 ` 205` ```apply transfer ``` huffman@47654 ` 206` ```apply fact ``` huffman@47654 ` 207` ```done ``` huffman@47654 ` 208` huffman@47654 ` 209` ```end ```