author | paulson <lp15@cam.ac.uk> |
Wed, 10 Apr 2019 13:34:55 +0100 | |
changeset 70097 | 4005298550a6 |
parent 69064 | 5840724b1d71 |
permissions | -rw-r--r-- |
47654 | 1 |
(* Title: HOL/ex/Transfer_Int_Nat.thy |
2 |
Author: Brian Huffman, TU Muenchen |
|
3 |
*) |
|
4 |
||
61343 | 5 |
section \<open>Using the transfer method between nat and int\<close> |
47654 | 6 |
|
7 |
theory Transfer_Int_Nat |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
64267
diff
changeset
|
8 |
imports Main |
47654 | 9 |
begin |
10 |
||
61343 | 11 |
subsection \<open>Correspondence relation\<close> |
47654 | 12 |
|
13 |
definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool" |
|
14 |
where "ZN = (\<lambda>z n. z = of_nat n)" |
|
15 |
||
61343 | 16 |
subsection \<open>Transfer domain rules\<close> |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset
|
17 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
64267
diff
changeset
|
18 |
lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset
|
19 |
unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset
|
20 |
|
61343 | 21 |
subsection \<open>Transfer rules\<close> |
47654 | 22 |
|
63343 | 23 |
context includes lifting_syntax |
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
24 |
begin |
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
25 |
|
47654 | 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 |
||
67399 | 38 |
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (+) (+)" |
55945 | 39 |
unfolding rel_fun_def ZN_def by simp |
47654 | 40 |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
67399
diff
changeset
|
41 |
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))" |
66954 | 42 |
unfolding rel_fun_def ZN_def by simp |
43 |
||
44 |
definition tsub :: "int \<Rightarrow> int \<Rightarrow> int" |
|
45 |
where "tsub k l = max 0 (k - l)" |
|
47654 | 46 |
|
67399 | 47 |
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (-)" |
66954 | 48 |
unfolding rel_fun_def ZN_def by (auto simp add: of_nat_diff tsub_def) |
47654 | 49 |
|
67399 | 50 |
lemma ZN_power [transfer_rule]: "(ZN ===> (=) ===> ZN) (^) (^)" |
66954 | 51 |
unfolding rel_fun_def ZN_def by simp |
47654 | 52 |
|
67399 | 53 |
lemma ZN_nat_id [transfer_rule]: "(ZN ===> (=)) nat id" |
55945 | 54 |
unfolding rel_fun_def ZN_def by simp |
47654 | 55 |
|
67399 | 56 |
lemma ZN_id_int [transfer_rule]: "(ZN ===> (=)) id int" |
55945 | 57 |
unfolding rel_fun_def ZN_def by simp |
47654 | 58 |
|
59 |
lemma ZN_All [transfer_rule]: |
|
67399 | 60 |
"((ZN ===> (=)) ===> (=)) (Ball {0..}) All" |
55945 | 61 |
unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int) |
47654 | 62 |
|
63 |
lemma ZN_transfer_forall [transfer_rule]: |
|
67399 | 64 |
"((ZN ===> (=)) ===> (=)) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall" |
47654 | 65 |
unfolding transfer_forall_def transfer_bforall_def |
55945 | 66 |
unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int) |
47654 | 67 |
|
67399 | 68 |
lemma ZN_Ex [transfer_rule]: "((ZN ===> (=)) ===> (=)) (Bex {0..}) Ex" |
55945 | 69 |
unfolding rel_fun_def ZN_def Bex_def atLeast_iff |
62348 | 70 |
by (metis zero_le_imp_eq_int of_nat_0_le_iff) |
47654 | 71 |
|
67399 | 72 |
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> (=)) (\<le>) (\<le>)" |
55945 | 73 |
unfolding rel_fun_def ZN_def by simp |
47654 | 74 |
|
67399 | 75 |
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> (=)) (<) (<)" |
55945 | 76 |
unfolding rel_fun_def ZN_def by simp |
47654 | 77 |
|
67399 | 78 |
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> (=)) (=) (=)" |
55945 | 79 |
unfolding rel_fun_def ZN_def by simp |
47654 | 80 |
|
81 |
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc" |
|
55945 | 82 |
unfolding rel_fun_def ZN_def by simp |
47654 | 83 |
|
84 |
lemma ZN_numeral [transfer_rule]: |
|
67399 | 85 |
"((=) ===> ZN) numeral numeral" |
55945 | 86 |
unfolding rel_fun_def ZN_def by simp |
47654 | 87 |
|
67399 | 88 |
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> (=)) (dvd) (dvd)" |
67118 | 89 |
unfolding rel_fun_def ZN_def by simp |
47654 | 90 |
|
67399 | 91 |
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (div) (div)" |
55945 | 92 |
unfolding rel_fun_def ZN_def by (simp add: zdiv_int) |
47654 | 93 |
|
67399 | 94 |
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (mod) (mod)" |
55945 | 95 |
unfolding rel_fun_def ZN_def by (simp add: zmod_int) |
47654 | 96 |
|
97 |
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" |
|
66954 | 98 |
unfolding rel_fun_def ZN_def by (simp add: gcd_int_def) |
47654 | 99 |
|
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
100 |
lemma ZN_atMost [transfer_rule]: |
55938 | 101 |
"(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost" |
55945 | 102 |
unfolding rel_fun_def ZN_def rel_set_def |
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
103 |
by (clarsimp simp add: Bex_def, arith) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
104 |
|
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
105 |
lemma ZN_atLeastAtMost [transfer_rule]: |
55938 | 106 |
"(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost" |
55945 | 107 |
unfolding rel_fun_def ZN_def rel_set_def |
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
108 |
by (clarsimp simp add: Bex_def, arith) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
109 |
|
64267 | 110 |
lemma ZN_sum [transfer_rule]: |
111 |
"bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) sum sum" |
|
55945 | 112 |
apply (intro rel_funI) |
55938 | 113 |
apply (erule (1) bi_unique_rel_set_lemma) |
64267 | 114 |
apply (simp add: sum.reindex int_sum ZN_def rel_fun_def) |
115 |
apply (rule sum.cong) |
|
57418 | 116 |
apply simp_all |
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
117 |
done |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
118 |
|
61933 | 119 |
text \<open>For derived operations, we can use the \<open>transfer_prover\<close> |
61343 | 120 |
method to help generate transfer rules.\<close> |
47654 | 121 |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
122 |
lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list" |
58320 | 123 |
by transfer_prover |
47654 | 124 |
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
125 |
end |
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
126 |
|
61343 | 127 |
subsection \<open>Transfer examples\<close> |
47654 | 128 |
|
129 |
lemma |
|
130 |
assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i" |
|
131 |
shows "\<And>i::nat. i + 0 = i" |
|
132 |
apply transfer |
|
133 |
apply fact |
|
134 |
done |
|
135 |
||
136 |
lemma |
|
137 |
assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k" |
|
138 |
shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k" |
|
139 |
apply transfer |
|
140 |
apply fact |
|
141 |
done |
|
142 |
||
143 |
lemma |
|
144 |
assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x" |
|
145 |
shows "\<forall>x y :: nat. x * y div y = x" |
|
146 |
apply transfer |
|
147 |
apply fact |
|
148 |
done |
|
149 |
||
150 |
lemma |
|
151 |
assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0" |
|
152 |
shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0" |
|
153 |
apply transfer |
|
154 |
apply fact |
|
155 |
done |
|
156 |
||
157 |
lemma |
|
158 |
assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z" |
|
159 |
shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z" |
|
160 |
apply transfer |
|
161 |
apply fact |
|
162 |
done |
|
163 |
||
61933 | 164 |
text \<open>The \<open>fixing\<close> option prevents generalization over the free |
165 |
variable \<open>n\<close>, allowing the local transfer rule to be used.\<close> |
|
47654 | 166 |
|
167 |
lemma |
|
168 |
assumes [transfer_rule]: "ZN x n" |
|
169 |
assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x" |
|
170 |
shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n" |
|
171 |
apply (transfer fixing: n) |
|
172 |
apply fact |
|
173 |
done |
|
174 |
||
175 |
lemma |
|
176 |
assumes "gcd (2^i) (3^j) = (1::int)" |
|
177 |
shows "gcd (2^i) (3^j) = (1::nat)" |
|
178 |
apply (transfer fixing: i j) |
|
179 |
apply fact |
|
180 |
done |
|
181 |
||
182 |
lemma |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
64267
diff
changeset
|
183 |
assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
184 |
sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
185 |
shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" |
47654 | 186 |
apply transfer |
187 |
apply fact |
|
188 |
done |
|
189 |
||
61933 | 190 |
text \<open>Quantifiers over higher types (e.g. \<open>nat list\<close>) are |
61343 | 191 |
transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\<close> |
47654 | 192 |
|
193 |
lemma |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset
|
194 |
assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
195 |
(sum_list xs = 0) = list_all (\<lambda>x. x = 0) xs" |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
196 |
shows "sum_list xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs" |
47654 | 197 |
apply transfer |
198 |
apply fact |
|
199 |
done |
|
200 |
||
61343 | 201 |
text \<open>Equality on a higher type can be transferred if the relations |
202 |
involved are bi-unique.\<close> |
|
47654 | 203 |
|
204 |
lemma |
|
61076 | 205 |
assumes "\<And>xs::int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
206 |
sum_list xs < sum_list (map (\<lambda>x. x + 1) xs)" |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
207 |
shows "xs \<noteq> [] \<Longrightarrow> sum_list xs < sum_list (map Suc xs)" |
47654 | 208 |
apply transfer |
209 |
apply fact |
|
210 |
done |
|
211 |
||
212 |
end |