author | nipkow |
Mon, 17 Oct 2016 11:46:22 +0200 | |
changeset 64267 | b9a1486e79be |
parent 63882 | 018998c00003 |
child 65552 | f533820e7248 |
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 |
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
8 |
imports GCD |
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 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset
|
18 |
lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" |
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 |
||
38 |
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)" |
|
55945 | 39 |
unfolding rel_fun_def ZN_def by simp |
47654 | 40 |
|
41 |
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)" |
|
62348 | 42 |
unfolding rel_fun_def ZN_def by (simp add: of_nat_mult) |
47654 | 43 |
|
44 |
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)" |
|
62348 | 45 |
unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff) |
47654 | 46 |
|
47 |
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)" |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61343
diff
changeset
|
48 |
unfolding rel_fun_def ZN_def by (simp add: of_nat_power) |
47654 | 49 |
|
50 |
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id" |
|
55945 | 51 |
unfolding rel_fun_def ZN_def by simp |
47654 | 52 |
|
53 |
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int" |
|
55945 | 54 |
unfolding rel_fun_def ZN_def by simp |
47654 | 55 |
|
56 |
lemma ZN_All [transfer_rule]: |
|
57 |
"((ZN ===> op =) ===> op =) (Ball {0..}) All" |
|
55945 | 58 |
unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int) |
47654 | 59 |
|
60 |
lemma ZN_transfer_forall [transfer_rule]: |
|
61 |
"((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall" |
|
62 |
unfolding transfer_forall_def transfer_bforall_def |
|
55945 | 63 |
unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int) |
47654 | 64 |
|
65 |
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex" |
|
55945 | 66 |
unfolding rel_fun_def ZN_def Bex_def atLeast_iff |
62348 | 67 |
by (metis zero_le_imp_eq_int of_nat_0_le_iff) |
47654 | 68 |
|
69 |
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)" |
|
55945 | 70 |
unfolding rel_fun_def ZN_def by simp |
47654 | 71 |
|
72 |
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)" |
|
55945 | 73 |
unfolding rel_fun_def ZN_def by simp |
47654 | 74 |
|
75 |
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)" |
|
55945 | 76 |
unfolding rel_fun_def ZN_def by simp |
47654 | 77 |
|
78 |
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc" |
|
55945 | 79 |
unfolding rel_fun_def ZN_def by simp |
47654 | 80 |
|
81 |
lemma ZN_numeral [transfer_rule]: |
|
82 |
"(op = ===> ZN) numeral numeral" |
|
55945 | 83 |
unfolding rel_fun_def ZN_def by simp |
47654 | 84 |
|
85 |
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)" |
|
55945 | 86 |
unfolding rel_fun_def ZN_def by (simp add: zdvd_int) |
47654 | 87 |
|
88 |
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)" |
|
55945 | 89 |
unfolding rel_fun_def ZN_def by (simp add: zdiv_int) |
47654 | 90 |
|
91 |
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)" |
|
55945 | 92 |
unfolding rel_fun_def ZN_def by (simp add: zmod_int) |
47654 | 93 |
|
94 |
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" |
|
55945 | 95 |
unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd) |
47654 | 96 |
|
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
97 |
lemma ZN_atMost [transfer_rule]: |
55938 | 98 |
"(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost" |
55945 | 99 |
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
|
100 |
by (clarsimp simp add: Bex_def, arith) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
101 |
|
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
102 |
lemma ZN_atLeastAtMost [transfer_rule]: |
55938 | 103 |
"(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost" |
55945 | 104 |
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
|
105 |
by (clarsimp simp add: Bex_def, arith) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
106 |
|
64267 | 107 |
lemma ZN_sum [transfer_rule]: |
108 |
"bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) sum sum" |
|
55945 | 109 |
apply (intro rel_funI) |
55938 | 110 |
apply (erule (1) bi_unique_rel_set_lemma) |
64267 | 111 |
apply (simp add: sum.reindex int_sum ZN_def rel_fun_def) |
112 |
apply (rule sum.cong) |
|
57418 | 113 |
apply simp_all |
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
114 |
done |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
115 |
|
61933 | 116 |
text \<open>For derived operations, we can use the \<open>transfer_prover\<close> |
61343 | 117 |
method to help generate transfer rules.\<close> |
47654 | 118 |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
119 |
lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list" |
58320 | 120 |
by transfer_prover |
47654 | 121 |
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
122 |
end |
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset
|
123 |
|
61343 | 124 |
subsection \<open>Transfer examples\<close> |
47654 | 125 |
|
126 |
lemma |
|
127 |
assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i" |
|
128 |
shows "\<And>i::nat. i + 0 = i" |
|
129 |
apply transfer |
|
130 |
apply fact |
|
131 |
done |
|
132 |
||
133 |
lemma |
|
134 |
assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k" |
|
135 |
shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k" |
|
136 |
apply transfer |
|
137 |
apply fact |
|
138 |
done |
|
139 |
||
140 |
lemma |
|
141 |
assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x" |
|
142 |
shows "\<forall>x y :: nat. x * y div y = x" |
|
143 |
apply transfer |
|
144 |
apply fact |
|
145 |
done |
|
146 |
||
147 |
lemma |
|
148 |
assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0" |
|
149 |
shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0" |
|
150 |
apply transfer |
|
151 |
apply fact |
|
152 |
done |
|
153 |
||
154 |
lemma |
|
155 |
assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z" |
|
156 |
shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z" |
|
157 |
apply transfer |
|
158 |
apply fact |
|
159 |
done |
|
160 |
||
61933 | 161 |
text \<open>The \<open>fixing\<close> option prevents generalization over the free |
162 |
variable \<open>n\<close>, allowing the local transfer rule to be used.\<close> |
|
47654 | 163 |
|
164 |
lemma |
|
165 |
assumes [transfer_rule]: "ZN x n" |
|
166 |
assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x" |
|
167 |
shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n" |
|
168 |
apply (transfer fixing: n) |
|
169 |
apply fact |
|
170 |
done |
|
171 |
||
172 |
lemma |
|
173 |
assumes "gcd (2^i) (3^j) = (1::int)" |
|
174 |
shows "gcd (2^i) (3^j) = (1::nat)" |
|
175 |
apply (transfer fixing: i j) |
|
176 |
apply fact |
|
177 |
done |
|
178 |
||
179 |
lemma |
|
180 |
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
|
181 |
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
|
182 |
shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" |
47654 | 183 |
apply transfer |
184 |
apply fact |
|
185 |
done |
|
186 |
||
61933 | 187 |
text \<open>Quantifiers over higher types (e.g. \<open>nat list\<close>) are |
61343 | 188 |
transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\<close> |
47654 | 189 |
|
190 |
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
|
191 |
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
|
192 |
(sum_list xs = 0) = list_all (\<lambda>x. x = 0) xs" |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
193 |
shows "sum_list xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs" |
47654 | 194 |
apply transfer |
195 |
apply fact |
|
196 |
done |
|
197 |
||
61343 | 198 |
text \<open>Equality on a higher type can be transferred if the relations |
199 |
involved are bi-unique.\<close> |
|
47654 | 200 |
|
201 |
lemma |
|
61076 | 202 |
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
|
203 |
sum_list xs < sum_list (map (\<lambda>x. x + 1) xs)" |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
204 |
shows "xs \<noteq> [] \<Longrightarrow> sum_list xs < sum_list (map Suc xs)" |
47654 | 205 |
apply transfer |
206 |
apply fact |
|
207 |
done |
|
208 |
||
209 |
end |