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 |
|
|
16 |
subsection {* Transfer rules *}
|
|
17 |
|
|
18 |
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
|
|
19 |
unfolding ZN_def bi_unique_def by simp
|
|
20 |
|
|
21 |
lemma right_total_ZN [transfer_rule]: "right_total ZN"
|
|
22 |
unfolding ZN_def right_total_def by simp
|
|
23 |
|
|
24 |
lemma ZN_0 [transfer_rule]: "ZN 0 0"
|
|
25 |
unfolding ZN_def by simp
|
|
26 |
|
|
27 |
lemma ZN_1 [transfer_rule]: "ZN 1 1"
|
|
28 |
unfolding ZN_def by simp
|
|
29 |
|
|
30 |
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
|
|
31 |
unfolding fun_rel_def ZN_def by simp
|
|
32 |
|
|
33 |
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
|
|
34 |
unfolding fun_rel_def ZN_def by (simp add: int_mult)
|
|
35 |
|
|
36 |
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
|
|
37 |
unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
|
|
38 |
|
|
39 |
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
|
|
40 |
unfolding fun_rel_def ZN_def by (simp add: int_power)
|
|
41 |
|
|
42 |
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
|
|
43 |
unfolding fun_rel_def ZN_def by simp
|
|
44 |
|
|
45 |
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
|
|
46 |
unfolding fun_rel_def ZN_def by simp
|
|
47 |
|
|
48 |
lemma ZN_All [transfer_rule]:
|
|
49 |
"((ZN ===> op =) ===> op =) (Ball {0..}) All"
|
|
50 |
unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
|
|
51 |
|
|
52 |
lemma ZN_transfer_forall [transfer_rule]:
|
|
53 |
"((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
|
|
54 |
unfolding transfer_forall_def transfer_bforall_def
|
|
55 |
unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
|
|
56 |
|
|
57 |
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
|
|
58 |
unfolding fun_rel_def ZN_def Bex_def atLeast_iff
|
|
59 |
by (metis zero_le_imp_eq_int zero_zle_int)
|
|
60 |
|
|
61 |
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
|
|
62 |
unfolding fun_rel_def ZN_def by simp
|
|
63 |
|
|
64 |
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
|
|
65 |
unfolding fun_rel_def ZN_def by simp
|
|
66 |
|
|
67 |
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
|
|
68 |
unfolding fun_rel_def ZN_def by simp
|
|
69 |
|
|
70 |
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
|
|
71 |
unfolding fun_rel_def ZN_def by simp
|
|
72 |
|
|
73 |
lemma ZN_numeral [transfer_rule]:
|
|
74 |
"(op = ===> ZN) numeral numeral"
|
|
75 |
unfolding fun_rel_def ZN_def by simp
|
|
76 |
|
|
77 |
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
|
|
78 |
unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
|
|
79 |
|
|
80 |
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
|
|
81 |
unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
|
|
82 |
|
|
83 |
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
|
|
84 |
unfolding fun_rel_def ZN_def by (simp add: zmod_int)
|
|
85 |
|
|
86 |
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
|
|
87 |
unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
|
|
88 |
|
|
89 |
text {* For derived operations, we can use the @{text "transfer_prover"}
|
|
90 |
method to help generate transfer rules. *}
|
|
91 |
|
|
92 |
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
|
|
93 |
unfolding listsum_def [abs_def] by transfer_prover
|
|
94 |
|
|
95 |
subsection {* Transfer examples *}
|
|
96 |
|
|
97 |
lemma
|
|
98 |
assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
|
|
99 |
shows "\<And>i::nat. i + 0 = i"
|
|
100 |
apply transfer
|
|
101 |
apply fact
|
|
102 |
done
|
|
103 |
|
|
104 |
lemma
|
|
105 |
assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k"
|
|
106 |
shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k"
|
|
107 |
apply transfer
|
|
108 |
apply fact
|
|
109 |
done
|
|
110 |
|
|
111 |
lemma
|
|
112 |
assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
|
|
113 |
shows "\<forall>x y :: nat. x * y div y = x"
|
|
114 |
apply transfer
|
|
115 |
apply fact
|
|
116 |
done
|
|
117 |
|
|
118 |
lemma
|
|
119 |
assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
|
|
120 |
shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0"
|
|
121 |
apply transfer
|
|
122 |
apply fact
|
|
123 |
done
|
|
124 |
|
|
125 |
lemma
|
|
126 |
assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
|
|
127 |
shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
|
|
128 |
apply transfer
|
|
129 |
apply fact
|
|
130 |
done
|
|
131 |
|
|
132 |
text {* The @{text "fixing"} option prevents generalization over the free
|
|
133 |
variable @{text "n"}, allowing the local transfer rule to be used. *}
|
|
134 |
|
|
135 |
lemma
|
|
136 |
assumes [transfer_rule]: "ZN x n"
|
|
137 |
assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
|
|
138 |
shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n"
|
|
139 |
apply (transfer fixing: n)
|
|
140 |
apply fact
|
|
141 |
done
|
|
142 |
|
|
143 |
lemma
|
|
144 |
assumes "gcd (2^i) (3^j) = (1::int)"
|
|
145 |
shows "gcd (2^i) (3^j) = (1::nat)"
|
|
146 |
apply (transfer fixing: i j)
|
|
147 |
apply fact
|
|
148 |
done
|
|
149 |
|
|
150 |
lemma
|
|
151 |
assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow>
|
|
152 |
listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
|
|
153 |
shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
|
|
154 |
apply transfer
|
|
155 |
apply fact
|
|
156 |
done
|
|
157 |
|
|
158 |
text {* Quantifiers over higher types (e.g. @{text "nat list"}) may
|
|
159 |
generate @{text "Domainp"} assumptions when transferred. *}
|
|
160 |
|
|
161 |
lemma
|
|
162 |
assumes "\<And>xs::int list. Domainp (list_all2 ZN) xs \<Longrightarrow>
|
|
163 |
(listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
|
|
164 |
shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
|
|
165 |
apply transfer
|
|
166 |
apply fact
|
|
167 |
done
|
|
168 |
|
|
169 |
text {* Equality on a higher type can be transferred if the relations
|
|
170 |
involved are bi-unique. *}
|
|
171 |
|
|
172 |
lemma
|
|
173 |
assumes "\<And>xs\<Colon>int list. \<lbrakk>Domainp (list_all2 ZN) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
|
|
174 |
listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
|
|
175 |
shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
|
|
176 |
apply transfer
|
|
177 |
apply fact
|
|
178 |
done
|
|
179 |
|
|
180 |
end
|