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