src/HOL/Nat_Transfer.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63648 f9f3006a5579 child 64267 b9a1486e79be permissions -rw-r--r--
tuned proofs;
1 (* Authors: Jeremy Avigad and Amine Chaieb *)
3 section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
5 theory Nat_Transfer
6 imports Int
7 begin
9 subsection \<open>Generic transfer machinery\<close>
11 definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
12   where "transfer_morphism f A \<longleftrightarrow> True"
14 lemma transfer_morphismI[intro]: "transfer_morphism f A"
17 ML_file "Tools/legacy_transfer.ML"
20 subsection \<open>Set up transfer from nat to int\<close>
22 text \<open>set up transfer direction\<close>
24 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
27   mode: manual
28   return: nat_0_le
29   labels: nat_int
30 ]
32 text \<open>basic functions and relations\<close>
34 lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
35     "(0::nat) = nat 0"
36     "(1::nat) = nat 1"
37     "(2::nat) = nat 2"
38     "(3::nat) = nat 3"
39   by auto
41 definition
42   tsub :: "int \<Rightarrow> int \<Rightarrow> int"
43 where
44   "tsub x y = (if x >= y then x - y else 0)"
46 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
49 lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
50     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
51     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
52     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
53     "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
54   by (auto simp add: eq_nat_nat_iff nat_mult_distrib
55       nat_power_eq tsub_def)
57 lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
58     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
59     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
60     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
61     "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
62     "(0::int) >= 0"
63     "(1::int) >= 0"
64     "(2::int) >= 0"
65     "(3::int) >= 0"
66     "int z >= 0"
67   by (auto simp add: zero_le_mult_iff tsub_def)
69 lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
70     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
71       (nat (x::int) = nat y) = (x = y)"
72     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
73       (nat (x::int) < nat y) = (x < y)"
74     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
75       (nat (x::int) <= nat y) = (x <= y)"
76     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
77       (nat (x::int) dvd nat y) = (x dvd y)"
78   by (auto simp add: zdvd_int)
81 text \<open>first-order quantifiers\<close>
83 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
84   by (simp split: split_nat)
86 lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
87 proof
88   assume "\<exists>x. P x"
89   then obtain x where "P x" ..
90   then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
91   then show "\<exists>x\<ge>0. P (nat x)" ..
92 next
93   assume "\<exists>x\<ge>0. P (nat x)"
94   then show "\<exists>x. P x" by auto
95 qed
97 lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
98     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
99     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
100   by (rule all_nat, rule ex_nat)
102 (* should we restrict these? *)
103 lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
104     (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
105   by auto
107 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
108     (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
109   by auto
112   cong: all_cong ex_cong]
115 text \<open>if\<close>
117 lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
118   "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
119   by auto
122 text \<open>operations with sets\<close>
124 definition
125   nat_set :: "int set \<Rightarrow> bool"
126 where
127   "nat_set S = (ALL x:S. x >= 0)"
129 lemma transfer_nat_int_set_functions:
130     "card A = card (int ` A)"
131     "{} = nat ` ({}::int set)"
132     "A Un B = nat ` (int ` A Un int ` B)"
133     "A Int B = nat ` (int ` A Int int ` B)"
134     "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
135   apply (rule card_image [symmetric])
136   apply (auto simp add: inj_on_def image_def)
137   apply (rule_tac x = "int x" in bexI)
138   apply auto
139   apply (rule_tac x = "int x" in bexI)
140   apply auto
141   apply (rule_tac x = "int x" in bexI)
142   apply auto
143   apply (rule_tac x = "int x" in exI)
144   apply auto
145 done
147 lemma transfer_nat_int_set_function_closures:
148     "nat_set {}"
149     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
150     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
151     "nat_set {x. x >= 0 & P x}"
152     "nat_set (int ` C)"
153     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
154   unfolding nat_set_def apply auto
155 done
157 lemma transfer_nat_int_set_relations:
158     "(finite A) = (finite (int ` A))"
159     "(x : A) = (int x : int ` A)"
160     "(A = B) = (int ` A = int ` B)"
161     "(A < B) = (int ` A < int ` B)"
162     "(A <= B) = (int ` A <= int ` B)"
163   apply (rule iffI)
164   apply (erule finite_imageI)
165   apply (erule finite_imageD)
166   apply (auto simp add: image_def set_eq_iff inj_on_def)
167   apply (drule_tac x = "int x" in spec, auto)
168   apply (drule_tac x = "int x" in spec, auto)
169   apply (drule_tac x = "int x" in spec, auto)
170 done
172 lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
173     (int ` nat ` A = A)"
174   by (auto simp add: nat_set_def image_def)
176 lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
177     {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
178   by auto
181   return: transfer_nat_int_set_functions
182     transfer_nat_int_set_function_closures
183     transfer_nat_int_set_relations
184     transfer_nat_int_set_return_embed
185   cong: transfer_nat_int_set_cong
186 ]
189 text \<open>setsum and setprod\<close>
191 (* this handles the case where the *domain* of f is nat *)
192 lemma transfer_nat_int_sum_prod:
193     "setsum f A = setsum (%x. f (nat x)) (int ` A)"
194     "setprod f A = setprod (%x. f (nat x)) (int ` A)"
195   apply (subst setsum.reindex)
196   apply (unfold inj_on_def, auto)
197   apply (subst setprod.reindex)
198   apply (unfold inj_on_def o_def, auto)
199 done
201 (* this handles the case where the *range* of f is nat *)
202 lemma transfer_nat_int_sum_prod2:
203     "setsum f A = nat(setsum (%x. int (f x)) A)"
204     "setprod f A = nat(setprod (%x. int (f x)) A)"
205   apply (simp only: int_setsum [symmetric] nat_int)
206   apply (simp only: int_setprod [symmetric] nat_int)
207   done
209 lemma transfer_nat_int_sum_prod_closure:
210     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
211     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
212   unfolding nat_set_def
213   apply (rule setsum_nonneg)
214   apply auto
215   apply (rule setprod_nonneg)
216   apply auto
217 done
219 (* this version doesn't work, even with nat_set A \<Longrightarrow>
220       x : A \<Longrightarrow> x >= 0 turned on. Why not?
222   also: what does =simp=> do?
224 lemma transfer_nat_int_sum_prod_closure:
225     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
226     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
227   unfolding nat_set_def simp_implies_def
228   apply (rule setsum_nonneg)
229   apply auto
230   apply (rule setprod_nonneg)
231   apply auto
232 done
233 *)
235 (* Making A = B in this lemma doesn't work. Why not?
236    Also, why aren't setsum.cong and setprod.cong enough,
237    with the previously mentioned rule turned on? *)
239 lemma transfer_nat_int_sum_prod_cong:
240     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
241       setsum f A = setsum g B"
242     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
243       setprod f A = setprod g B"
244   unfolding nat_set_def
245   apply (subst setsum.cong, assumption)
246   apply auto [2]
247   apply (subst setprod.cong, assumption, auto)
248 done
251   return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
252     transfer_nat_int_sum_prod_closure
253   cong: transfer_nat_int_sum_prod_cong]
256 subsection \<open>Set up transfer from int to nat\<close>
258 text \<open>set up transfer direction\<close>
260 lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
263   mode: manual
264   return: nat_int
265   labels: int_nat
266 ]
269 text \<open>basic functions and relations\<close>
271 definition
272   is_nat :: "int \<Rightarrow> bool"
273 where
274   "is_nat x = (x >= 0)"
276 lemma transfer_int_nat_numerals:
277     "0 = int 0"
278     "1 = int 1"
279     "2 = int 2"
280     "3 = int 3"
281   by auto
283 lemma transfer_int_nat_functions:
284     "(int x) + (int y) = int (x + y)"
285     "(int x) * (int y) = int (x * y)"
286     "tsub (int x) (int y) = int (x - y)"
287     "(int x)^n = int (x^n)"
288   by (auto simp add: of_nat_mult tsub_def of_nat_power)
290 lemma transfer_int_nat_function_closures:
291     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
292     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
293     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
294     "is_nat x \<Longrightarrow> is_nat (x^n)"
295     "is_nat 0"
296     "is_nat 1"
297     "is_nat 2"
298     "is_nat 3"
299     "is_nat (int z)"
300   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
302 lemma transfer_int_nat_relations:
303     "(int x = int y) = (x = y)"
304     "(int x < int y) = (x < y)"
305     "(int x <= int y) = (x <= y)"
306     "(int x dvd int y) = (x dvd y)"
307   by (auto simp add: zdvd_int)
309 declare transfer_morphism_int_nat [transfer add return:
310   transfer_int_nat_numerals
311   transfer_int_nat_functions
312   transfer_int_nat_function_closures
313   transfer_int_nat_relations
314 ]
317 text \<open>first-order quantifiers\<close>
319 lemma transfer_int_nat_quantifiers:
320     "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
321     "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
322   apply (subst all_nat)
323   apply auto [1]
324   apply (subst ex_nat)
325   apply auto
326 done
329   return: transfer_int_nat_quantifiers]
332 text \<open>if\<close>
334 lemma int_if_cong: "(if P then (int x) else (int y)) =
335     int (if P then x else y)"
336   by auto
338 declare transfer_morphism_int_nat [transfer add return: int_if_cong]
342 text \<open>operations with sets\<close>
344 lemma transfer_int_nat_set_functions:
345     "nat_set A \<Longrightarrow> card A = card (nat ` A)"
346     "{} = int ` ({}::nat set)"
347     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
348     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
349     "{x. x >= 0 & P x} = int ` {x. P(int x)}"
350        (* need all variants of these! *)
351   by (simp_all only: is_nat_def transfer_nat_int_set_functions
352           transfer_nat_int_set_function_closures
353           transfer_nat_int_set_return_embed nat_0_le
354           cong: transfer_nat_int_set_cong)
356 lemma transfer_int_nat_set_function_closures:
357     "nat_set {}"
358     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
359     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
360     "nat_set {x. x >= 0 & P x}"
361     "nat_set (int ` C)"
362     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
363   by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
365 lemma transfer_int_nat_set_relations:
366     "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
367     "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
368     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
369     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
370     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
371   by (simp_all only: is_nat_def transfer_nat_int_set_relations
372     transfer_nat_int_set_return_embed nat_0_le)
374 lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
375   by (simp only: transfer_nat_int_set_relations
376     transfer_nat_int_set_function_closures
377     transfer_nat_int_set_return_embed nat_0_le)
379 lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
380     {(x::nat). P x} = {x. P' x}"
381   by auto
384   return: transfer_int_nat_set_functions
385     transfer_int_nat_set_function_closures
386     transfer_int_nat_set_relations
387     transfer_int_nat_set_return_embed
388   cong: transfer_int_nat_set_cong
389 ]
392 text \<open>setsum and setprod\<close>
394 (* this handles the case where the *domain* of f is int *)
395 lemma transfer_int_nat_sum_prod:
396     "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
397     "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
398   apply (subst setsum.reindex)
399   apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
400   apply (subst setprod.reindex)
401   apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
402             cong: setprod.cong)
403 done
405 (* this handles the case where the *range* of f is int *)
406 lemma transfer_int_nat_sum_prod2:
407     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
408     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
409       setprod f A = int(setprod (%x. nat (f x)) A)"
410   unfolding is_nat_def
411   by (subst int_setsum) auto