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