src/HOL/ex/Transfer_Int_Nat.thy
author wenzelm
Tue Oct 06 17:47:28 2015 +0200 (2015-10-06)
changeset 61343 5b5656a63bd6
parent 61076 bdc1e2f0a86a
child 61649 268d88ec9087
permissions -rw-r--r--
isabelle update_cartouches;
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 \<open>Using the transfer method between nat and int\<close>
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 \<open>Correspondence relation\<close>
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
wenzelm@61343
    16
subsection \<open>Transfer domain rules\<close>
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
wenzelm@61343
    21
subsection \<open>Transfer rules\<close>
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 +)"
blanchet@55945
    40
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    41
huffman@47654
    42
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
blanchet@55945
    43
  unfolding rel_fun_def ZN_def by (simp add: int_mult)
huffman@47654
    44
huffman@47654
    45
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
blanchet@55945
    46
  unfolding rel_fun_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 ^)"
blanchet@55945
    49
  unfolding rel_fun_def ZN_def by (simp add: int_power)
huffman@47654
    50
huffman@47654
    51
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
blanchet@55945
    52
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    53
huffman@47654
    54
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
blanchet@55945
    55
  unfolding rel_fun_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"
blanchet@55945
    59
  unfolding rel_fun_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
blanchet@55945
    64
  unfolding rel_fun_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"
blanchet@55945
    67
  unfolding rel_fun_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>)"
blanchet@55945
    71
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    72
huffman@47654
    73
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
blanchet@55945
    74
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    75
huffman@47654
    76
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
blanchet@55945
    77
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    78
huffman@47654
    79
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
blanchet@55945
    80
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    81
huffman@47654
    82
lemma ZN_numeral [transfer_rule]:
huffman@47654
    83
  "(op = ===> ZN) numeral numeral"
blanchet@55945
    84
  unfolding rel_fun_def ZN_def by simp
huffman@47654
    85
huffman@47654
    86
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
blanchet@55945
    87
  unfolding rel_fun_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)"
blanchet@55945
    90
  unfolding rel_fun_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)"
blanchet@55945
    93
  unfolding rel_fun_def ZN_def by (simp add: zmod_int)
huffman@47654
    94
huffman@47654
    95
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
blanchet@55945
    96
  unfolding rel_fun_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@55945
   100
  unfolding rel_fun_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@55945
   105
  unfolding rel_fun_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"
blanchet@55945
   110
  apply (intro rel_funI)
blanchet@55938
   111
  apply (erule (1) bi_unique_rel_set_lemma)
blanchet@55945
   112
  apply (simp add: setsum.reindex int_setsum ZN_def rel_fun_def)
haftmann@57418
   113
  apply (rule setsum.cong)
haftmann@57418
   114
  apply simp_all
huffman@52360
   115
  done
huffman@52360
   116
wenzelm@61343
   117
text \<open>For derived operations, we can use the @{text "transfer_prover"}
wenzelm@61343
   118
  method to help generate transfer rules.\<close>
huffman@47654
   119
huffman@47654
   120
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
haftmann@58320
   121
  by transfer_prover
huffman@47654
   122
kuncar@53013
   123
end
kuncar@53013
   124
wenzelm@61343
   125
subsection \<open>Transfer examples\<close>
huffman@47654
   126
huffman@47654
   127
lemma
huffman@47654
   128
  assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
huffman@47654
   129
  shows "\<And>i::nat. i + 0 = i"
huffman@47654
   130
apply transfer
huffman@47654
   131
apply fact
huffman@47654
   132
done
huffman@47654
   133
huffman@47654
   134
lemma
huffman@47654
   135
  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
   136
  shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k"
huffman@47654
   137
apply transfer
huffman@47654
   138
apply fact
huffman@47654
   139
done
huffman@47654
   140
huffman@47654
   141
lemma
huffman@47654
   142
  assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
huffman@47654
   143
  shows "\<forall>x y :: nat. x * y div y = x"
huffman@47654
   144
apply transfer
huffman@47654
   145
apply fact
huffman@47654
   146
done
huffman@47654
   147
huffman@47654
   148
lemma
huffman@47654
   149
  assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
huffman@47654
   150
  shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0"
huffman@47654
   151
apply transfer
huffman@47654
   152
apply fact
huffman@47654
   153
done
huffman@47654
   154
huffman@47654
   155
lemma
huffman@47654
   156
  assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
huffman@47654
   157
  shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
huffman@47654
   158
apply transfer
huffman@47654
   159
apply fact
huffman@47654
   160
done
huffman@47654
   161
wenzelm@61343
   162
text \<open>The @{text "fixing"} option prevents generalization over the free
wenzelm@61343
   163
  variable @{text "n"}, allowing the local transfer rule to be used.\<close>
huffman@47654
   164
huffman@47654
   165
lemma
huffman@47654
   166
  assumes [transfer_rule]: "ZN x n"
huffman@47654
   167
  assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
huffman@47654
   168
  shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n"
huffman@47654
   169
apply (transfer fixing: n)
huffman@47654
   170
apply fact
huffman@47654
   171
done
huffman@47654
   172
huffman@47654
   173
lemma
huffman@47654
   174
  assumes "gcd (2^i) (3^j) = (1::int)"
huffman@47654
   175
  shows "gcd (2^i) (3^j) = (1::nat)"
huffman@47654
   176
apply (transfer fixing: i j)
huffman@47654
   177
apply fact
huffman@47654
   178
done
huffman@47654
   179
huffman@47654
   180
lemma
huffman@47654
   181
  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
huffman@47654
   182
    listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
huffman@47654
   183
  shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
huffman@47654
   184
apply transfer
huffman@47654
   185
apply fact
huffman@47654
   186
done
huffman@47654
   187
wenzelm@61343
   188
text \<open>Quantifiers over higher types (e.g. @{text "nat list"}) are
wenzelm@61343
   189
  transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\<close>
huffman@47654
   190
huffman@47654
   191
lemma
kuncar@51956
   192
  assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
huffman@47654
   193
    (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
huffman@47654
   194
  shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
huffman@47654
   195
apply transfer
huffman@47654
   196
apply fact
huffman@47654
   197
done
huffman@47654
   198
wenzelm@61343
   199
text \<open>Equality on a higher type can be transferred if the relations
wenzelm@61343
   200
  involved are bi-unique.\<close>
huffman@47654
   201
huffman@47654
   202
lemma
wenzelm@61076
   203
  assumes "\<And>xs::int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
huffman@47654
   204
    listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
huffman@47654
   205
  shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
huffman@47654
   206
apply transfer
huffman@47654
   207
apply fact
huffman@47654
   208
done
huffman@47654
   209
huffman@47654
   210
end