author | huffman |
Mon, 10 Jun 2013 06:08:17 -0700 | |
changeset 52360 | ac7ac2b242a2 |
parent 51956 | a4d81cdebf8b |
child 53013 | 3fbcfa911863 |
permissions | -rw-r--r-- |
47654 | 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 |
||
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
|
16 |
subsection {* Transfer domain rules *} |
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 |
|
47654 | 21 |
subsection {* Transfer rules *} |
22 |
||
23 |
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN" |
|
24 |
unfolding ZN_def bi_unique_def by simp |
|
25 |
||
26 |
lemma right_total_ZN [transfer_rule]: "right_total ZN" |
|
27 |
unfolding ZN_def right_total_def by simp |
|
28 |
||
29 |
lemma ZN_0 [transfer_rule]: "ZN 0 0" |
|
30 |
unfolding ZN_def by simp |
|
31 |
||
32 |
lemma ZN_1 [transfer_rule]: "ZN 1 1" |
|
33 |
unfolding ZN_def by simp |
|
34 |
||
35 |
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)" |
|
36 |
unfolding fun_rel_def ZN_def by simp |
|
37 |
||
38 |
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)" |
|
39 |
unfolding fun_rel_def ZN_def by (simp add: int_mult) |
|
40 |
||
41 |
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)" |
|
42 |
unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int) |
|
43 |
||
44 |
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)" |
|
45 |
unfolding fun_rel_def ZN_def by (simp add: int_power) |
|
46 |
||
47 |
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id" |
|
48 |
unfolding fun_rel_def ZN_def by simp |
|
49 |
||
50 |
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int" |
|
51 |
unfolding fun_rel_def ZN_def by simp |
|
52 |
||
53 |
lemma ZN_All [transfer_rule]: |
|
54 |
"((ZN ===> op =) ===> op =) (Ball {0..}) All" |
|
55 |
unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int) |
|
56 |
||
57 |
lemma ZN_transfer_forall [transfer_rule]: |
|
58 |
"((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall" |
|
59 |
unfolding transfer_forall_def transfer_bforall_def |
|
60 |
unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int) |
|
61 |
||
62 |
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex" |
|
63 |
unfolding fun_rel_def ZN_def Bex_def atLeast_iff |
|
64 |
by (metis zero_le_imp_eq_int zero_zle_int) |
|
65 |
||
66 |
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)" |
|
67 |
unfolding fun_rel_def ZN_def by simp |
|
68 |
||
69 |
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)" |
|
70 |
unfolding fun_rel_def ZN_def by simp |
|
71 |
||
72 |
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)" |
|
73 |
unfolding fun_rel_def ZN_def by simp |
|
74 |
||
75 |
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc" |
|
76 |
unfolding fun_rel_def ZN_def by simp |
|
77 |
||
78 |
lemma ZN_numeral [transfer_rule]: |
|
79 |
"(op = ===> ZN) numeral numeral" |
|
80 |
unfolding fun_rel_def ZN_def by simp |
|
81 |
||
82 |
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)" |
|
83 |
unfolding fun_rel_def ZN_def by (simp add: zdvd_int) |
|
84 |
||
85 |
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)" |
|
86 |
unfolding fun_rel_def ZN_def by (simp add: zdiv_int) |
|
87 |
||
88 |
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)" |
|
89 |
unfolding fun_rel_def ZN_def by (simp add: zmod_int) |
|
90 |
||
91 |
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" |
|
92 |
unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd) |
|
93 |
||
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
94 |
lemma ZN_atMost [transfer_rule]: |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
95 |
"(ZN ===> set_rel ZN) (atLeastAtMost 0) atMost" |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
96 |
unfolding fun_rel_def ZN_def set_rel_def |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
97 |
by (clarsimp simp add: Bex_def, arith) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
98 |
|
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
99 |
lemma ZN_atLeastAtMost [transfer_rule]: |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
100 |
"(ZN ===> ZN ===> set_rel ZN) atLeastAtMost atLeastAtMost" |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
101 |
unfolding fun_rel_def ZN_def set_rel_def |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
102 |
by (clarsimp simp add: Bex_def, arith) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
103 |
|
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
104 |
lemma ZN_setsum [transfer_rule]: |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
105 |
"bi_unique A \<Longrightarrow> ((A ===> ZN) ===> set_rel A ===> ZN) setsum setsum" |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
106 |
apply (intro fun_relI) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
107 |
apply (erule (1) bi_unique_set_rel_lemma) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
108 |
apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
109 |
apply (rule setsum_cong2, simp) |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
110 |
done |
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset
|
111 |
|
47654 | 112 |
text {* For derived operations, we can use the @{text "transfer_prover"} |
113 |
method to help generate transfer rules. *} |
|
114 |
||
115 |
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum" |
|
116 |
unfolding listsum_def [abs_def] by transfer_prover |
|
117 |
||
118 |
subsection {* Transfer examples *} |
|
119 |
||
120 |
lemma |
|
121 |
assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i" |
|
122 |
shows "\<And>i::nat. i + 0 = i" |
|
123 |
apply transfer |
|
124 |
apply fact |
|
125 |
done |
|
126 |
||
127 |
lemma |
|
128 |
assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k" |
|
129 |
shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k" |
|
130 |
apply transfer |
|
131 |
apply fact |
|
132 |
done |
|
133 |
||
134 |
lemma |
|
135 |
assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x" |
|
136 |
shows "\<forall>x y :: nat. x * y div y = x" |
|
137 |
apply transfer |
|
138 |
apply fact |
|
139 |
done |
|
140 |
||
141 |
lemma |
|
142 |
assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0" |
|
143 |
shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0" |
|
144 |
apply transfer |
|
145 |
apply fact |
|
146 |
done |
|
147 |
||
148 |
lemma |
|
149 |
assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z" |
|
150 |
shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z" |
|
151 |
apply transfer |
|
152 |
apply fact |
|
153 |
done |
|
154 |
||
155 |
text {* The @{text "fixing"} option prevents generalization over the free |
|
156 |
variable @{text "n"}, allowing the local transfer rule to be used. *} |
|
157 |
||
158 |
lemma |
|
159 |
assumes [transfer_rule]: "ZN x n" |
|
160 |
assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x" |
|
161 |
shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n" |
|
162 |
apply (transfer fixing: n) |
|
163 |
apply fact |
|
164 |
done |
|
165 |
||
166 |
lemma |
|
167 |
assumes "gcd (2^i) (3^j) = (1::int)" |
|
168 |
shows "gcd (2^i) (3^j) = (1::nat)" |
|
169 |
apply (transfer fixing: i j) |
|
170 |
apply fact |
|
171 |
done |
|
172 |
||
173 |
lemma |
|
174 |
assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> |
|
175 |
listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" |
|
176 |
shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" |
|
177 |
apply transfer |
|
178 |
apply fact |
|
179 |
done |
|
180 |
||
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
|
181 |
text {* Quantifiers over higher types (e.g. @{text "nat list"}) are |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset
|
182 |
transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN} *} |
47654 | 183 |
|
184 |
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
|
185 |
assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow> |
47654 | 186 |
(listsum xs = 0) = list_all (\<lambda>x. x = 0) xs" |
187 |
shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs" |
|
188 |
apply transfer |
|
189 |
apply fact |
|
190 |
done |
|
191 |
||
192 |
text {* Equality on a higher type can be transferred if the relations |
|
193 |
involved are bi-unique. *} |
|
194 |
||
195 |
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
|
196 |
assumes "\<And>xs\<Colon>int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> |
47654 | 197 |
listsum xs < listsum (map (\<lambda>x. x + 1) xs)" |
198 |
shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)" |
|
199 |
apply transfer |
|
200 |
apply fact |
|
201 |
done |
|
202 |
||
203 |
end |