1 |
1 |
2 (* Authors: Jeremy Avigad and Amine Chaieb *) |
2 (* Authors: Jeremy Avigad and Amine Chaieb *) |
3 |
3 |
4 header {* Sets up transfer from nats to ints and back. *} |
4 header {* Generic transfer machinery; specific transfer from nats to ints and back. *} |
5 |
5 |
6 theory Nat_Transfer |
6 theory Nat_Transfer |
7 imports Main Parity |
7 imports Nat_Numeral |
|
8 uses ("Tools/transfer.ML") |
8 begin |
9 begin |
9 |
10 |
|
11 subsection {* Generic transfer machinery *} |
|
12 |
|
13 definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool" |
|
14 where "TransferMorphism a B \<longleftrightarrow> True" |
|
15 |
|
16 use "Tools/transfer.ML" |
|
17 |
|
18 setup Transfer.setup |
|
19 |
|
20 |
10 subsection {* Set up transfer from nat to int *} |
21 subsection {* Set up transfer from nat to int *} |
11 |
22 |
12 (* set up transfer direction *) |
23 text {* set up transfer direction *} |
13 |
24 |
14 lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))" |
25 lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))" |
15 by (simp add: TransferMorphism_def) |
26 by (simp add: TransferMorphism_def) |
16 |
27 |
17 declare TransferMorphism_nat_int[transfer |
28 declare TransferMorphism_nat_int[transfer |
18 add mode: manual |
29 add mode: manual |
19 return: nat_0_le |
30 return: nat_0_le |
20 labels: natint |
31 labels: natint |
21 ] |
32 ] |
22 |
33 |
23 (* basic functions and relations *) |
34 text {* basic functions and relations *} |
24 |
35 |
25 lemma transfer_nat_int_numerals: |
36 lemma transfer_nat_int_numerals: |
26 "(0::nat) = nat 0" |
37 "(0::nat) = nat 0" |
27 "(1::nat) = nat 1" |
38 "(1::nat) = nat 1" |
28 "(2::nat) = nat 2" |
39 "(2::nat) = nat 2" |
41 lemma transfer_nat_int_functions: |
52 lemma transfer_nat_int_functions: |
42 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)" |
53 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)" |
43 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)" |
54 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)" |
44 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)" |
55 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)" |
45 "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)" |
56 "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)" |
46 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)" |
|
47 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)" |
|
48 by (auto simp add: eq_nat_nat_iff nat_mult_distrib |
57 by (auto simp add: eq_nat_nat_iff nat_mult_distrib |
49 nat_power_eq nat_div_distrib nat_mod_distrib tsub_def) |
58 nat_power_eq tsub_def) |
50 |
59 |
51 lemma transfer_nat_int_function_closures: |
60 lemma transfer_nat_int_function_closures: |
52 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0" |
61 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0" |
53 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0" |
62 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0" |
54 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0" |
63 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0" |
55 "(x::int) >= 0 \<Longrightarrow> x^n >= 0" |
64 "(x::int) >= 0 \<Longrightarrow> x^n >= 0" |
56 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0" |
|
57 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0" |
|
58 "(0::int) >= 0" |
65 "(0::int) >= 0" |
59 "(1::int) >= 0" |
66 "(1::int) >= 0" |
60 "(2::int) >= 0" |
67 "(2::int) >= 0" |
61 "(3::int) >= 0" |
68 "(3::int) >= 0" |
62 "int z >= 0" |
69 "int z >= 0" |
63 apply (auto simp add: zero_le_mult_iff tsub_def) |
70 apply (auto simp add: zero_le_mult_iff tsub_def) |
64 apply (case_tac "y = 0") |
|
65 apply auto |
|
66 apply (subst pos_imp_zdiv_nonneg_iff, auto) |
|
67 apply (case_tac "y = 0") |
|
68 apply force |
|
69 apply (rule pos_mod_sign) |
|
70 apply arith |
|
71 done |
71 done |
72 |
72 |
73 lemma transfer_nat_int_relations: |
73 lemma transfer_nat_int_relations: |
74 "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> |
74 "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> |
75 (nat (x::int) = nat y) = (x = y)" |
75 (nat (x::int) = nat y) = (x = y)" |
87 transfer_nat_int_function_closures |
87 transfer_nat_int_function_closures |
88 transfer_nat_int_relations |
88 transfer_nat_int_relations |
89 ] |
89 ] |
90 |
90 |
91 |
91 |
92 (* first-order quantifiers *) |
92 text {* first-order quantifiers *} |
|
93 |
|
94 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))" |
|
95 by (simp split add: split_nat) |
|
96 |
|
97 lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))" |
|
98 proof |
|
99 assume "\<exists>x. P x" |
|
100 then obtain x where "P x" .. |
|
101 then have "int x \<ge> 0 \<and> P (nat (int x))" by simp |
|
102 then show "\<exists>x\<ge>0. P (nat x)" .. |
|
103 next |
|
104 assume "\<exists>x\<ge>0. P (nat x)" |
|
105 then show "\<exists>x. P x" by auto |
|
106 qed |
93 |
107 |
94 lemma transfer_nat_int_quantifiers: |
108 lemma transfer_nat_int_quantifiers: |
95 "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))" |
109 "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))" |
96 "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))" |
110 "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))" |
97 by (rule all_nat, rule ex_nat) |
111 by (rule all_nat, rule ex_nat) |
108 declare TransferMorphism_nat_int[transfer add |
122 declare TransferMorphism_nat_int[transfer add |
109 return: transfer_nat_int_quantifiers |
123 return: transfer_nat_int_quantifiers |
110 cong: all_cong ex_cong] |
124 cong: all_cong ex_cong] |
111 |
125 |
112 |
126 |
113 (* if *) |
127 text {* if *} |
114 |
128 |
115 lemma nat_if_cong: "(if P then (nat x) else (nat y)) = |
129 lemma nat_if_cong: "(if P then (nat x) else (nat y)) = |
116 nat (if P then x else y)" |
130 nat (if P then x else y)" |
117 by auto |
131 by auto |
118 |
132 |
119 declare TransferMorphism_nat_int [transfer add return: nat_if_cong] |
133 declare TransferMorphism_nat_int [transfer add return: nat_if_cong] |
120 |
134 |
121 |
135 |
122 (* operations with sets *) |
136 text {* operations with sets *} |
123 |
137 |
124 definition |
138 definition |
125 nat_set :: "int set \<Rightarrow> bool" |
139 nat_set :: "int set \<Rightarrow> bool" |
126 where |
140 where |
127 "nat_set S = (ALL x:S. x >= 0)" |
141 "nat_set S = (ALL x:S. x >= 0)" |
130 "card A = card (int ` A)" |
144 "card A = card (int ` A)" |
131 "{} = nat ` ({}::int set)" |
145 "{} = nat ` ({}::int set)" |
132 "A Un B = nat ` (int ` A Un int ` B)" |
146 "A Un B = nat ` (int ` A Un int ` B)" |
133 "A Int B = nat ` (int ` A Int int ` B)" |
147 "A Int B = nat ` (int ` A Int int ` B)" |
134 "{x. P x} = nat ` {x. x >= 0 & P(nat x)}" |
148 "{x. P x} = nat ` {x. x >= 0 & P(nat x)}" |
135 "{..n} = nat ` {0..int n}" |
|
136 "{m..n} = nat ` {int m..int n}" (* need all variants of these! *) |
|
137 apply (rule card_image [symmetric]) |
149 apply (rule card_image [symmetric]) |
138 apply (auto simp add: inj_on_def image_def) |
150 apply (auto simp add: inj_on_def image_def) |
139 apply (rule_tac x = "int x" in bexI) |
151 apply (rule_tac x = "int x" in bexI) |
140 apply auto |
152 apply auto |
141 apply (rule_tac x = "int x" in bexI) |
153 apply (rule_tac x = "int x" in bexI) |
142 apply auto |
154 apply auto |
143 apply (rule_tac x = "int x" in bexI) |
155 apply (rule_tac x = "int x" in bexI) |
144 apply auto |
156 apply auto |
145 apply (rule_tac x = "int x" in exI) |
157 apply (rule_tac x = "int x" in exI) |
146 apply auto |
|
147 apply (rule_tac x = "int x" in bexI) |
|
148 apply auto |
|
149 apply (rule_tac x = "int x" in bexI) |
|
150 apply auto |
158 apply auto |
151 done |
159 done |
152 |
160 |
153 lemma transfer_nat_int_set_function_closures: |
161 lemma transfer_nat_int_set_function_closures: |
154 "nat_set {}" |
162 "nat_set {}" |
155 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)" |
163 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)" |
156 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)" |
164 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)" |
157 "x >= 0 \<Longrightarrow> nat_set {x..y}" |
|
158 "nat_set {x. x >= 0 & P x}" |
165 "nat_set {x. x >= 0 & P x}" |
159 "nat_set (int ` C)" |
166 "nat_set (int ` C)" |
160 "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *) |
167 "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *) |
161 unfolding nat_set_def apply auto |
168 unfolding nat_set_def apply auto |
162 done |
169 done |
165 "(finite A) = (finite (int ` A))" |
172 "(finite A) = (finite (int ` A))" |
166 "(x : A) = (int x : int ` A)" |
173 "(x : A) = (int x : int ` A)" |
167 "(A = B) = (int ` A = int ` B)" |
174 "(A = B) = (int ` A = int ` B)" |
168 "(A < B) = (int ` A < int ` B)" |
175 "(A < B) = (int ` A < int ` B)" |
169 "(A <= B) = (int ` A <= int ` B)" |
176 "(A <= B) = (int ` A <= int ` B)" |
170 |
|
171 apply (rule iffI) |
177 apply (rule iffI) |
172 apply (erule finite_imageI) |
178 apply (erule finite_imageI) |
173 apply (erule finite_imageD) |
179 apply (erule finite_imageD) |
174 apply (auto simp add: image_def expand_set_eq inj_on_def) |
180 apply (auto simp add: image_def expand_set_eq inj_on_def) |
175 apply (drule_tac x = "int x" in spec, auto) |
181 apply (drule_tac x = "int x" in spec, auto) |
192 transfer_nat_int_set_return_embed |
198 transfer_nat_int_set_return_embed |
193 cong: transfer_nat_int_set_cong |
199 cong: transfer_nat_int_set_cong |
194 ] |
200 ] |
195 |
201 |
196 |
202 |
197 (* setsum and setprod *) |
203 text {* setsum and setprod *} |
198 |
204 |
199 (* this handles the case where the *domain* of f is nat *) |
205 (* this handles the case where the *domain* of f is nat *) |
200 lemma transfer_nat_int_sum_prod: |
206 lemma transfer_nat_int_sum_prod: |
201 "setsum f A = setsum (%x. f (nat x)) (int ` A)" |
207 "setsum f A = setsum (%x. f (nat x)) (int ` A)" |
202 "setprod f A = setprod (%x. f (nat x)) (int ` A)" |
208 "setprod f A = setprod (%x. f (nat x)) (int ` A)" |
260 declare TransferMorphism_nat_int[transfer add |
266 declare TransferMorphism_nat_int[transfer add |
261 return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2 |
267 return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2 |
262 transfer_nat_int_sum_prod_closure |
268 transfer_nat_int_sum_prod_closure |
263 cong: transfer_nat_int_sum_prod_cong] |
269 cong: transfer_nat_int_sum_prod_cong] |
264 |
270 |
265 (* lists *) |
|
266 |
|
267 definition |
|
268 embed_list :: "nat list \<Rightarrow> int list" |
|
269 where |
|
270 "embed_list l = map int l"; |
|
271 |
|
272 definition |
|
273 nat_list :: "int list \<Rightarrow> bool" |
|
274 where |
|
275 "nat_list l = nat_set (set l)"; |
|
276 |
|
277 definition |
|
278 return_list :: "int list \<Rightarrow> nat list" |
|
279 where |
|
280 "return_list l = map nat l"; |
|
281 |
|
282 thm nat_0_le; |
|
283 |
|
284 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow> |
|
285 embed_list (return_list l) = l"; |
|
286 unfolding embed_list_def return_list_def nat_list_def nat_set_def |
|
287 apply (induct l); |
|
288 apply auto; |
|
289 done; |
|
290 |
|
291 lemma transfer_nat_int_list_functions: |
|
292 "l @ m = return_list (embed_list l @ embed_list m)" |
|
293 "[] = return_list []"; |
|
294 unfolding return_list_def embed_list_def; |
|
295 apply auto; |
|
296 apply (induct l, auto); |
|
297 apply (induct m, auto); |
|
298 done; |
|
299 |
|
300 (* |
|
301 lemma transfer_nat_int_fold1: "fold f l x = |
|
302 fold (%x. f (nat x)) (embed_list l) x"; |
|
303 *) |
|
304 |
|
305 |
|
306 |
|
307 |
271 |
308 subsection {* Set up transfer from int to nat *} |
272 subsection {* Set up transfer from int to nat *} |
309 |
273 |
310 (* set up transfer direction *) |
274 text {* set up transfer direction *} |
311 |
275 |
312 lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)" |
276 lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)" |
313 by (simp add: TransferMorphism_def) |
277 by (simp add: TransferMorphism_def) |
314 |
278 |
315 declare TransferMorphism_int_nat[transfer add |
279 declare TransferMorphism_int_nat[transfer add |
336 lemma transfer_int_nat_functions: |
304 lemma transfer_int_nat_functions: |
337 "(int x) + (int y) = int (x + y)" |
305 "(int x) + (int y) = int (x + y)" |
338 "(int x) * (int y) = int (x * y)" |
306 "(int x) * (int y) = int (x * y)" |
339 "tsub (int x) (int y) = int (x - y)" |
307 "tsub (int x) (int y) = int (x - y)" |
340 "(int x)^n = int (x^n)" |
308 "(int x)^n = int (x^n)" |
341 "(int x) div (int y) = int (x div y)" |
309 by (auto simp add: int_mult tsub_def int_power) |
342 "(int x) mod (int y) = int (x mod y)" |
|
343 by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int) |
|
344 |
310 |
345 lemma transfer_int_nat_function_closures: |
311 lemma transfer_int_nat_function_closures: |
346 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)" |
312 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)" |
347 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)" |
313 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)" |
348 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)" |
314 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)" |
349 "is_nat x \<Longrightarrow> is_nat (x^n)" |
315 "is_nat x \<Longrightarrow> is_nat (x^n)" |
350 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)" |
|
351 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)" |
|
352 "is_nat 0" |
316 "is_nat 0" |
353 "is_nat 1" |
317 "is_nat 1" |
354 "is_nat 2" |
318 "is_nat 2" |
355 "is_nat 3" |
319 "is_nat 3" |
356 "is_nat (int z)" |
320 "is_nat (int z)" |
359 lemma transfer_int_nat_relations: |
323 lemma transfer_int_nat_relations: |
360 "(int x = int y) = (x = y)" |
324 "(int x = int y) = (x = y)" |
361 "(int x < int y) = (x < y)" |
325 "(int x < int y) = (x < y)" |
362 "(int x <= int y) = (x <= y)" |
326 "(int x <= int y) = (x <= y)" |
363 "(int x dvd int y) = (x dvd y)" |
327 "(int x dvd int y) = (x dvd y)" |
364 "(even (int x)) = (even x)" |
328 by (auto simp add: zdvd_int) |
365 by (auto simp add: zdvd_int even_nat_def) |
|
366 |
|
367 lemma UNIV_apply: |
|
368 "UNIV x = True" |
|
369 by (simp add: top_fun_eq top_bool_eq) |
|
370 |
329 |
371 declare TransferMorphism_int_nat[transfer add return: |
330 declare TransferMorphism_int_nat[transfer add return: |
372 transfer_int_nat_numerals |
331 transfer_int_nat_numerals |
373 transfer_int_nat_functions |
332 transfer_int_nat_functions |
374 transfer_int_nat_function_closures |
333 transfer_int_nat_function_closures |
375 transfer_int_nat_relations |
334 transfer_int_nat_relations |
376 UNIV_apply |
335 UNIV_apply |
377 ] |
336 ] |
378 |
337 |
379 |
338 |
380 (* first-order quantifiers *) |
339 text {* first-order quantifiers *} |
381 |
340 |
382 lemma transfer_int_nat_quantifiers: |
341 lemma transfer_int_nat_quantifiers: |
383 "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))" |
342 "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))" |
384 "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))" |
343 "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))" |
385 apply (subst all_nat) |
344 apply (subst all_nat) |
390 |
349 |
391 declare TransferMorphism_int_nat[transfer add |
350 declare TransferMorphism_int_nat[transfer add |
392 return: transfer_int_nat_quantifiers] |
351 return: transfer_int_nat_quantifiers] |
393 |
352 |
394 |
353 |
395 (* if *) |
354 text {* if *} |
396 |
355 |
397 lemma int_if_cong: "(if P then (int x) else (int y)) = |
356 lemma int_if_cong: "(if P then (int x) else (int y)) = |
398 int (if P then x else y)" |
357 int (if P then x else y)" |
399 by auto |
358 by auto |
400 |
359 |
401 declare TransferMorphism_int_nat [transfer add return: int_if_cong] |
360 declare TransferMorphism_int_nat [transfer add return: int_if_cong] |
402 |
361 |
403 |
362 |
404 |
363 |
405 (* operations with sets *) |
364 text {* operations with sets *} |
406 |
365 |
407 lemma transfer_int_nat_set_functions: |
366 lemma transfer_int_nat_set_functions: |
408 "nat_set A \<Longrightarrow> card A = card (nat ` A)" |
367 "nat_set A \<Longrightarrow> card A = card (nat ` A)" |
409 "{} = int ` ({}::nat set)" |
368 "{} = int ` ({}::nat set)" |
410 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)" |
369 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)" |
411 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)" |
370 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)" |
412 "{x. x >= 0 & P x} = int ` {x. P(int x)}" |
371 "{x. x >= 0 & P x} = int ` {x. P(int x)}" |
413 "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}" |
|
414 (* need all variants of these! *) |
372 (* need all variants of these! *) |
415 by (simp_all only: is_nat_def transfer_nat_int_set_functions |
373 by (simp_all only: is_nat_def transfer_nat_int_set_functions |
416 transfer_nat_int_set_function_closures |
374 transfer_nat_int_set_function_closures |
417 transfer_nat_int_set_return_embed nat_0_le |
375 transfer_nat_int_set_return_embed nat_0_le |
418 cong: transfer_nat_int_set_cong) |
376 cong: transfer_nat_int_set_cong) |
419 |
377 |
420 lemma transfer_int_nat_set_function_closures: |
378 lemma transfer_int_nat_set_function_closures: |
421 "nat_set {}" |
379 "nat_set {}" |
422 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)" |
380 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)" |
423 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)" |
381 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)" |
424 "is_nat x \<Longrightarrow> nat_set {x..y}" |
|
425 "nat_set {x. x >= 0 & P x}" |
382 "nat_set {x. x >= 0 & P x}" |
426 "nat_set (int ` C)" |
383 "nat_set (int ` C)" |
427 "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x" |
384 "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x" |
428 by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) |
385 by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) |
429 |
386 |
452 transfer_int_nat_set_return_embed |
409 transfer_int_nat_set_return_embed |
453 cong: transfer_int_nat_set_cong |
410 cong: transfer_int_nat_set_cong |
454 ] |
411 ] |
455 |
412 |
456 |
413 |
457 (* setsum and setprod *) |
414 text {* setsum and setprod *} |
458 |
415 |
459 (* this handles the case where the *domain* of f is int *) |
416 (* this handles the case where the *domain* of f is int *) |
460 lemma transfer_int_nat_sum_prod: |
417 lemma transfer_int_nat_sum_prod: |
461 "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)" |
418 "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)" |
462 "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)" |
419 "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)" |