src/HOL/ex/Transfer_Int_Nat.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 47654 f7df7104d13e
child 51956 a4d81cdebf8b
permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/ex/Transfer_Int_Nat.thy
     2     Author:     Brian Huffman, TU Muenchen
     3 *)
     4 
     5 header {* Using the transfer method between nat and int *}
     6 
     7 theory Transfer_Int_Nat
     8 imports GCD "~~/src/HOL/Library/Quotient_List"
     9 begin
    10 
    11 subsection {* Correspondence relation *}
    12 
    13 definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
    14   where "ZN = (\<lambda>z n. z = of_nat n)"
    15 
    16 subsection {* Transfer rules *}
    17 
    18 lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
    19   unfolding ZN_def bi_unique_def by simp
    20 
    21 lemma right_total_ZN [transfer_rule]: "right_total ZN"
    22   unfolding ZN_def right_total_def by simp
    23 
    24 lemma ZN_0 [transfer_rule]: "ZN 0 0"
    25   unfolding ZN_def by simp
    26 
    27 lemma ZN_1 [transfer_rule]: "ZN 1 1"
    28   unfolding ZN_def by simp
    29 
    30 lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
    31   unfolding fun_rel_def ZN_def by simp
    32 
    33 lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
    34   unfolding fun_rel_def ZN_def by (simp add: int_mult)
    35 
    36 lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
    37   unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
    38 
    39 lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
    40   unfolding fun_rel_def ZN_def by (simp add: int_power)
    41 
    42 lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
    43   unfolding fun_rel_def ZN_def by simp
    44 
    45 lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
    46   unfolding fun_rel_def ZN_def by simp
    47 
    48 lemma ZN_All [transfer_rule]:
    49   "((ZN ===> op =) ===> op =) (Ball {0..}) All"
    50   unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
    51 
    52 lemma ZN_transfer_forall [transfer_rule]:
    53   "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
    54   unfolding transfer_forall_def transfer_bforall_def
    55   unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
    56 
    57 lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
    58   unfolding fun_rel_def ZN_def Bex_def atLeast_iff
    59   by (metis zero_le_imp_eq_int zero_zle_int)
    60 
    61 lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
    62   unfolding fun_rel_def ZN_def by simp
    63 
    64 lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
    65   unfolding fun_rel_def ZN_def by simp
    66 
    67 lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
    68   unfolding fun_rel_def ZN_def by simp
    69 
    70 lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
    71   unfolding fun_rel_def ZN_def by simp
    72 
    73 lemma ZN_numeral [transfer_rule]:
    74   "(op = ===> ZN) numeral numeral"
    75   unfolding fun_rel_def ZN_def by simp
    76 
    77 lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
    78   unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
    79 
    80 lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
    81   unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
    82 
    83 lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
    84   unfolding fun_rel_def ZN_def by (simp add: zmod_int)
    85 
    86 lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
    87   unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
    88 
    89 text {* For derived operations, we can use the @{text "transfer_prover"}
    90   method to help generate transfer rules. *}
    91 
    92 lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
    93   unfolding listsum_def [abs_def] by transfer_prover
    94 
    95 subsection {* Transfer examples *}
    96 
    97 lemma
    98   assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
    99   shows "\<And>i::nat. i + 0 = i"
   100 apply transfer
   101 apply fact
   102 done
   103 
   104 lemma
   105   assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k"
   106   shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k"
   107 apply transfer
   108 apply fact
   109 done
   110 
   111 lemma
   112   assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
   113   shows "\<forall>x y :: nat. x * y div y = x"
   114 apply transfer
   115 apply fact
   116 done
   117 
   118 lemma
   119   assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
   120   shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0"
   121 apply transfer
   122 apply fact
   123 done
   124 
   125 lemma
   126   assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
   127   shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
   128 apply transfer
   129 apply fact
   130 done
   131 
   132 text {* The @{text "fixing"} option prevents generalization over the free
   133   variable @{text "n"}, allowing the local transfer rule to be used. *}
   134 
   135 lemma
   136   assumes [transfer_rule]: "ZN x n"
   137   assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
   138   shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n"
   139 apply (transfer fixing: n)
   140 apply fact
   141 done
   142 
   143 lemma
   144   assumes "gcd (2^i) (3^j) = (1::int)"
   145   shows "gcd (2^i) (3^j) = (1::nat)"
   146 apply (transfer fixing: i j)
   147 apply fact
   148 done
   149 
   150 lemma
   151   assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
   152     listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   153   shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   154 apply transfer
   155 apply fact
   156 done
   157 
   158 text {* Quantifiers over higher types (e.g. @{text "nat list"}) may
   159   generate @{text "Domainp"} assumptions when transferred. *}
   160 
   161 lemma
   162   assumes "\<And>xs::int list. Domainp (list_all2 ZN) xs \<Longrightarrow>
   163     (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
   164   shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
   165 apply transfer
   166 apply fact
   167 done
   168 
   169 text {* Equality on a higher type can be transferred if the relations
   170   involved are bi-unique. *}
   171 
   172 lemma
   173   assumes "\<And>xs\<Colon>int list. \<lbrakk>Domainp (list_all2 ZN) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
   174     listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
   175   shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
   176 apply transfer
   177 apply fact
   178 done
   179 
   180 end