src/HOL/ex/Transfer_Int_Nat.thy
author blanchet
Thu Mar 06 14:57:14 2014 +0100 (2014-03-06)
changeset 55938 f20d1db5aa3c
parent 53013 3fbcfa911863
child 55945 e96383acecf9
permissions -rw-r--r--
renamed 'set_rel' to 'rel_set'
huffman@47654
     1
(*  Title:      HOL/ex/Transfer_Int_Nat.thy
huffman@47654
     2
    Author:     Brian Huffman, TU Muenchen
huffman@47654
     3
*)
huffman@47654
     4
huffman@47654
     5
header {* 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
huffman@47654
    11
subsection {* Correspondence relation *}
huffman@47654
    12
huffman@47654
    13
definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
huffman@47654
    14
  where "ZN = (\<lambda>z n. z = of_nat n)"
huffman@47654
    15
kuncar@51956
    16
subsection {* Transfer domain rules *}
kuncar@51956
    17
kuncar@51956
    18
lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" 
kuncar@51956
    19
  unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)
kuncar@51956
    20
huffman@47654
    21
subsection {* Transfer rules *}
huffman@47654
    22
kuncar@53013
    23
context
kuncar@53013
    24
begin
kuncar@53013
    25
interpretation lifting_syntax .
kuncar@53013
    26
huffman@47654
    27
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
huffman@47654
    28
  unfolding ZN_def bi_unique_def by simp
huffman@47654
    29
huffman@47654
    30
lemma right_total_ZN [transfer_rule]: "right_total ZN"
huffman@47654
    31
  unfolding ZN_def right_total_def by simp
huffman@47654
    32
huffman@47654
    33
lemma ZN_0 [transfer_rule]: "ZN 0 0"
huffman@47654
    34
  unfolding ZN_def by simp
huffman@47654
    35
huffman@47654
    36
lemma ZN_1 [transfer_rule]: "ZN 1 1"
huffman@47654
    37
  unfolding ZN_def by simp
huffman@47654
    38
huffman@47654
    39
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
huffman@47654
    40
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    41
huffman@47654
    42
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
huffman@47654
    43
  unfolding fun_rel_def ZN_def by (simp add: int_mult)
huffman@47654
    44
huffman@47654
    45
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
huffman@47654
    46
  unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
huffman@47654
    47
huffman@47654
    48
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
huffman@47654
    49
  unfolding fun_rel_def ZN_def by (simp add: int_power)
huffman@47654
    50
huffman@47654
    51
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
huffman@47654
    52
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    53
huffman@47654
    54
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
huffman@47654
    55
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    56
huffman@47654
    57
lemma ZN_All [transfer_rule]:
huffman@47654
    58
  "((ZN ===> op =) ===> op =) (Ball {0..}) All"
huffman@47654
    59
  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
huffman@47654
    60
huffman@47654
    61
lemma ZN_transfer_forall [transfer_rule]:
huffman@47654
    62
  "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
huffman@47654
    63
  unfolding transfer_forall_def transfer_bforall_def
huffman@47654
    64
  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
huffman@47654
    65
huffman@47654
    66
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
huffman@47654
    67
  unfolding fun_rel_def ZN_def Bex_def atLeast_iff
huffman@47654
    68
  by (metis zero_le_imp_eq_int zero_zle_int)
huffman@47654
    69
huffman@47654
    70
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
huffman@47654
    71
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    72
huffman@47654
    73
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
huffman@47654
    74
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    75
huffman@47654
    76
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
huffman@47654
    77
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    78
huffman@47654
    79
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
huffman@47654
    80
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    81
huffman@47654
    82
lemma ZN_numeral [transfer_rule]:
huffman@47654
    83
  "(op = ===> ZN) numeral numeral"
huffman@47654
    84
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    85
huffman@47654
    86
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
huffman@47654
    87
  unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
huffman@47654
    88
huffman@47654
    89
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
huffman@47654
    90
  unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
huffman@47654
    91
huffman@47654
    92
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
huffman@47654
    93
  unfolding fun_rel_def ZN_def by (simp add: zmod_int)
huffman@47654
    94
huffman@47654
    95
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
huffman@47654
    96
  unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
huffman@47654
    97
huffman@52360
    98
lemma ZN_atMost [transfer_rule]:
blanchet@55938
    99
  "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
blanchet@55938
   100
  unfolding fun_rel_def ZN_def rel_set_def
huffman@52360
   101
  by (clarsimp simp add: Bex_def, arith)
huffman@52360
   102
huffman@52360
   103
lemma ZN_atLeastAtMost [transfer_rule]:
blanchet@55938
   104
  "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
blanchet@55938
   105
  unfolding fun_rel_def ZN_def rel_set_def
huffman@52360
   106
  by (clarsimp simp add: Bex_def, arith)
huffman@52360
   107
huffman@52360
   108
lemma ZN_setsum [transfer_rule]:
blanchet@55938
   109
  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
huffman@52360
   110
  apply (intro fun_relI)
blanchet@55938
   111
  apply (erule (1) bi_unique_rel_set_lemma)
huffman@52360
   112
  apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
huffman@52360
   113
  apply (rule setsum_cong2, simp)
huffman@52360
   114
  done
huffman@52360
   115
huffman@47654
   116
text {* For derived operations, we can use the @{text "transfer_prover"}
huffman@47654
   117
  method to help generate transfer rules. *}
huffman@47654
   118
huffman@47654
   119
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
huffman@47654
   120
  unfolding listsum_def [abs_def] by transfer_prover
huffman@47654
   121
kuncar@53013
   122
end
kuncar@53013
   123
huffman@47654
   124
subsection {* Transfer examples *}
huffman@47654
   125
huffman@47654
   126
lemma
huffman@47654
   127
  assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
huffman@47654
   128
  shows "\<And>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 "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k"
huffman@47654
   135
  shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>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 "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
huffman@47654
   142
  shows "\<forall>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 "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
huffman@47654
   149
  shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> 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 "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
huffman@47654
   156
  shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
huffman@47654
   157
apply transfer
huffman@47654
   158
apply fact
huffman@47654
   159
done
huffman@47654
   160
huffman@47654
   161
text {* The @{text "fixing"} option prevents generalization over the free
huffman@47654
   162
  variable @{text "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 "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
huffman@47654
   167
  shows "\<forall>i. i < n \<longrightarrow> 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 "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
huffman@47654
   181
    listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
huffman@47654
   182
  shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
huffman@47654
   183
apply transfer
huffman@47654
   184
apply fact
huffman@47654
   185
done
huffman@47654
   186
kuncar@51956
   187
text {* Quantifiers over higher types (e.g. @{text "nat list"}) are
kuncar@51956
   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 "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
huffman@47654
   192
    (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
huffman@47654
   193
  shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
huffman@47654
   194
apply transfer
huffman@47654
   195
apply fact
huffman@47654
   196
done
huffman@47654
   197
huffman@47654
   198
text {* Equality on a higher type can be transferred if the relations
huffman@47654
   199
  involved are bi-unique. *}
huffman@47654
   200
huffman@47654
   201
lemma
kuncar@51956
   202
  assumes "\<And>xs\<Colon>int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
huffman@47654
   203
    listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
huffman@47654
   204
  shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
huffman@47654
   205
apply transfer
huffman@47654
   206
apply fact
huffman@47654
   207
done
huffman@47654
   208
huffman@47654
   209
end