author  wenzelm 
Thu, 28 Feb 2013 11:40:23 +0100  
changeset 51299  30b014246e21 
parent 50422  ee729dbd1b7f 
child 57418  6ab1c7cb0b8d 
permissions  rwrr 
31708  1 

32554  2 
(* Authors: Jeremy Avigad and Amine Chaieb *) 
31708  3 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

4 
header {* Generic transfer machinery; specific transfer from nats to ints and back. *} 
31708  5 

32558  6 
theory Nat_Transfer 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
42870
diff
changeset

7 
imports Int 
31708  8 
begin 
9 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

10 
subsection {* Generic transfer machinery *} 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

11 

35821  12 
definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
42870
36abaf4cce1f
clarified vacuous nature of predicate "transfer_morphism"  equivalent to previous definiton
krauss
parents:
39302
diff
changeset

13 
where "transfer_morphism f A \<longleftrightarrow> True" 
35644  14 

42870
36abaf4cce1f
clarified vacuous nature of predicate "transfer_morphism"  equivalent to previous definiton
krauss
parents:
39302
diff
changeset

15 
lemma transfer_morphismI[intro]: "transfer_morphism f A" 
36abaf4cce1f
clarified vacuous nature of predicate "transfer_morphism"  equivalent to previous definiton
krauss
parents:
39302
diff
changeset

16 
by (simp add: transfer_morphism_def) 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

17 

48891  18 
ML_file "Tools/legacy_transfer.ML" 
47324
ed2bad9b7c6a
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
huffman
parents:
47255
diff
changeset

19 
setup Legacy_Transfer.setup 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

20 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

21 

31708  22 
subsection {* Set up transfer from nat to int *} 
23 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

24 
text {* set up transfer direction *} 
31708  25 

42870
36abaf4cce1f
clarified vacuous nature of predicate "transfer_morphism"  equivalent to previous definiton
krauss
parents:
39302
diff
changeset

26 
lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" .. 
31708  27 

35683  28 
declare transfer_morphism_nat_int [transfer add 
29 
mode: manual 

31708  30 
return: nat_0_le 
35683  31 
labels: nat_int 
31708  32 
] 
33 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

34 
text {* basic functions and relations *} 
31708  35 

35683  36 
lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]: 
31708  37 
"(0::nat) = nat 0" 
38 
"(1::nat) = nat 1" 

39 
"(2::nat) = nat 2" 

40 
"(3::nat) = nat 3" 

41 
by auto 

42 

43 
definition 

44 
tsub :: "int \<Rightarrow> int \<Rightarrow> int" 

45 
where 

46 
"tsub x y = (if x >= y then x  y else 0)" 

47 

48 
lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x  y" 

49 
by (simp add: tsub_def) 

50 

35683  51 
lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]: 
31708  52 
"(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)" 

54 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x)  (nat y) = nat (tsub x y)" 

55 
"(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)" 

56 
by (auto simp add: eq_nat_nat_iff nat_mult_distrib 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

57 
nat_power_eq tsub_def) 
31708  58 

35683  59 
lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]: 
31708  60 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0" 
61 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0" 

62 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0" 

63 
"(x::int) >= 0 \<Longrightarrow> x^n >= 0" 

64 
"(0::int) >= 0" 

65 
"(1::int) >= 0" 

66 
"(2::int) >= 0" 

67 
"(3::int) >= 0" 

68 
"int z >= 0" 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

69 
by (auto simp add: zero_le_mult_iff tsub_def) 
31708  70 

35683  71 
lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]: 
31708  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) <= nat y) = (x <= y)" 

78 
"x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> 

79 
(nat (x::int) dvd nat y) = (x dvd y)" 

32558  80 
by (auto simp add: zdvd_int) 
31708  81 

82 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

83 
text {* firstorder quantifiers *} 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

84 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

85 
lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

86 
by (simp split add: split_nat) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

87 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

88 
lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

89 
proof 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

90 
assume "\<exists>x. P x" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

91 
then obtain x where "P x" .. 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

92 
then have "int x \<ge> 0 \<and> P (nat (int x))" by simp 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

93 
then show "\<exists>x\<ge>0. P (nat x)" .. 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

94 
next 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

95 
assume "\<exists>x\<ge>0. P (nat x)" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

96 
then show "\<exists>x. P x" by auto 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

97 
qed 
31708  98 

35683  99 
lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]: 
31708  100 
"(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))" 
101 
"(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))" 

102 
by (rule all_nat, rule ex_nat) 

103 

104 
(* should we restrict these? *) 

105 
lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> 

106 
(ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)" 

107 
by auto 

108 

109 
lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow> 

110 
(EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)" 

111 
by auto 

112 

35644  113 
declare transfer_morphism_nat_int [transfer add 
31708  114 
cong: all_cong ex_cong] 
115 

116 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

117 
text {* if *} 
31708  118 

35683  119 
lemma nat_if_cong [transfer key: transfer_morphism_nat_int]: 
120 
"(if P then (nat x) else (nat y)) = nat (if P then x else y)" 

31708  121 
by auto 
122 

123 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

124 
text {* operations with sets *} 
31708  125 

126 
definition 

127 
nat_set :: "int set \<Rightarrow> bool" 

128 
where 

129 
"nat_set S = (ALL x:S. x >= 0)" 

130 

131 
lemma transfer_nat_int_set_functions: 

132 
"card A = card (int ` A)" 

133 
"{} = nat ` ({}::int set)" 

134 
"A Un B = nat ` (int ` A Un int ` B)" 

135 
"A Int B = nat ` (int ` A Int int ` B)" 

136 
"{x. P x} = nat ` {x. x >= 0 & P(nat x)}" 

137 
apply (rule card_image [symmetric]) 

138 
apply (auto simp add: inj_on_def image_def) 

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 bexI) 

144 
apply auto 

145 
apply (rule_tac x = "int x" in exI) 

146 
apply auto 

147 
done 

148 

149 
lemma transfer_nat_int_set_function_closures: 

150 
"nat_set {}" 

151 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)" 

152 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)" 

153 
"nat_set {x. x >= 0 & P x}" 

154 
"nat_set (int ` C)" 

155 
"nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *) 

156 
unfolding nat_set_def apply auto 

157 
done 

158 

159 
lemma transfer_nat_int_set_relations: 

160 
"(finite A) = (finite (int ` A))" 

161 
"(x : A) = (int x : int ` A)" 

162 
"(A = B) = (int ` A = int ` B)" 

163 
"(A < B) = (int ` A < int ` B)" 

164 
"(A <= B) = (int ` A <= int ` B)" 

165 
apply (rule iffI) 

166 
apply (erule finite_imageI) 

167 
apply (erule finite_imageD) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

168 
apply (auto simp add: image_def set_eq_iff inj_on_def) 
31708  169 
apply (drule_tac x = "int x" in spec, auto) 
170 
apply (drule_tac x = "int x" in spec, auto) 

171 
apply (drule_tac x = "int x" in spec, auto) 

172 
done 

173 

174 
lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow> 

175 
(int ` nat ` A = A)" 

176 
by (auto simp add: nat_set_def image_def) 

177 

178 
lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow> 

179 
{(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}" 

180 
by auto 

181 

35644  182 
declare transfer_morphism_nat_int [transfer add 
31708  183 
return: transfer_nat_int_set_functions 
184 
transfer_nat_int_set_function_closures 

185 
transfer_nat_int_set_relations 

186 
transfer_nat_int_set_return_embed 

187 
cong: transfer_nat_int_set_cong 

188 
] 

189 

190 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

191 
text {* setsum and setprod *} 
31708  192 

193 
(* this handles the case where the *domain* of f is nat *) 

194 
lemma transfer_nat_int_sum_prod: 

195 
"setsum f A = setsum (%x. f (nat x)) (int ` A)" 

196 
"setprod f A = setprod (%x. f (nat x)) (int ` A)" 

197 
apply (subst setsum_reindex) 

198 
apply (unfold inj_on_def, auto) 

199 
apply (subst setprod_reindex) 

200 
apply (unfold inj_on_def o_def, auto) 

201 
done 

202 

203 
(* this handles the case where the *range* of f is nat *) 

204 
lemma transfer_nat_int_sum_prod2: 

205 
"setsum f A = nat(setsum (%x. int (f x)) A)" 

206 
"setprod f A = nat(setprod (%x. int (f x)) A)" 

207 
apply (subst int_setsum [symmetric]) 

208 
apply auto 

209 
apply (subst int_setprod [symmetric]) 

210 
apply auto 

211 
done 

212 

213 
lemma transfer_nat_int_sum_prod_closure: 

214 
"nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0" 

215 
"nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0" 

216 
unfolding nat_set_def 

217 
apply (rule setsum_nonneg) 

218 
apply auto 

219 
apply (rule setprod_nonneg) 

220 
apply auto 

221 
done 

222 

223 
(* this version doesn't work, even with nat_set A \<Longrightarrow> 

224 
x : A \<Longrightarrow> x >= 0 turned on. Why not? 

225 

226 
also: what does =simp=> do? 

227 

228 
lemma transfer_nat_int_sum_prod_closure: 

229 
"(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0" 

230 
"(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0" 

231 
unfolding nat_set_def simp_implies_def 

232 
apply (rule setsum_nonneg) 

233 
apply auto 

234 
apply (rule setprod_nonneg) 

235 
apply auto 

236 
done 

237 
*) 

238 

239 
(* Making A = B in this lemma doesn't work. Why not? 

240 
Also, why aren't setsum_cong and setprod_cong enough, 

241 
with the previously mentioned rule turned on? *) 

242 

243 
lemma transfer_nat_int_sum_prod_cong: 

244 
"A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow> 

245 
setsum f A = setsum g B" 

246 
"A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow> 

247 
setprod f A = setprod g B" 

248 
unfolding nat_set_def 

249 
apply (subst setsum_cong, assumption) 

250 
apply auto [2] 

251 
apply (subst setprod_cong, assumption, auto) 

252 
done 

253 

35644  254 
declare transfer_morphism_nat_int [transfer add 
31708  255 
return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2 
256 
transfer_nat_int_sum_prod_closure 

257 
cong: transfer_nat_int_sum_prod_cong] 

258 

259 

260 
subsection {* Set up transfer from int to nat *} 

261 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

262 
text {* set up transfer direction *} 
31708  263 

42870
36abaf4cce1f
clarified vacuous nature of predicate "transfer_morphism"  equivalent to previous definiton
krauss
parents:
39302
diff
changeset

264 
lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" .. 
31708  265 

35644  266 
declare transfer_morphism_int_nat [transfer add 
31708  267 
mode: manual 
268 
return: nat_int 

35683  269 
labels: int_nat 
31708  270 
] 
271 

272 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

273 
text {* basic functions and relations *} 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

274 

31708  275 
definition 
276 
is_nat :: "int \<Rightarrow> bool" 

277 
where 

278 
"is_nat x = (x >= 0)" 

279 

280 
lemma transfer_int_nat_numerals: 

281 
"0 = int 0" 

282 
"1 = int 1" 

283 
"2 = int 2" 

284 
"3 = int 3" 

285 
by auto 

286 

287 
lemma transfer_int_nat_functions: 

288 
"(int x) + (int y) = int (x + y)" 

289 
"(int x) * (int y) = int (x * y)" 

290 
"tsub (int x) (int y) = int (x  y)" 

291 
"(int x)^n = int (x^n)" 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

292 
by (auto simp add: int_mult tsub_def int_power) 
31708  293 

294 
lemma transfer_int_nat_function_closures: 

295 
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)" 

296 
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)" 

297 
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)" 

298 
"is_nat x \<Longrightarrow> is_nat (x^n)" 

299 
"is_nat 0" 

300 
"is_nat 1" 

301 
"is_nat 2" 

302 
"is_nat 3" 

303 
"is_nat (int z)" 

304 
by (simp_all only: is_nat_def transfer_nat_int_function_closures) 

305 

306 
lemma transfer_int_nat_relations: 

307 
"(int x = int y) = (x = y)" 

308 
"(int x < int y) = (x < y)" 

309 
"(int x <= int y) = (x <= y)" 

310 
"(int x dvd int y) = (x dvd y)" 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

311 
by (auto simp add: zdvd_int) 
32121  312 

35644  313 
declare transfer_morphism_int_nat [transfer add return: 
31708  314 
transfer_int_nat_numerals 
315 
transfer_int_nat_functions 

316 
transfer_int_nat_function_closures 

317 
transfer_int_nat_relations 

318 
] 

319 

320 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

321 
text {* firstorder quantifiers *} 
31708  322 

323 
lemma transfer_int_nat_quantifiers: 

324 
"(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))" 

325 
"(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))" 

326 
apply (subst all_nat) 

327 
apply auto [1] 

328 
apply (subst ex_nat) 

329 
apply auto 

330 
done 

331 

35644  332 
declare transfer_morphism_int_nat [transfer add 
31708  333 
return: transfer_int_nat_quantifiers] 
334 

335 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

336 
text {* if *} 
31708  337 

338 
lemma int_if_cong: "(if P then (int x) else (int y)) = 

339 
int (if P then x else y)" 

340 
by auto 

341 

35644  342 
declare transfer_morphism_int_nat [transfer add return: int_if_cong] 
31708  343 

344 

345 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

346 
text {* operations with sets *} 
31708  347 

348 
lemma transfer_int_nat_set_functions: 

349 
"nat_set A \<Longrightarrow> card A = card (nat ` A)" 

350 
"{} = int ` ({}::nat set)" 

351 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)" 

352 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)" 

353 
"{x. x >= 0 & P x} = int ` {x. P(int x)}" 

354 
(* need all variants of these! *) 

355 
by (simp_all only: is_nat_def transfer_nat_int_set_functions 

356 
transfer_nat_int_set_function_closures 

357 
transfer_nat_int_set_return_embed nat_0_le 

358 
cong: transfer_nat_int_set_cong) 

359 

360 
lemma transfer_int_nat_set_function_closures: 

361 
"nat_set {}" 

362 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)" 

363 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)" 

364 
"nat_set {x. x >= 0 & P x}" 

365 
"nat_set (int ` C)" 

366 
"nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x" 

367 
by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) 

368 

369 
lemma transfer_int_nat_set_relations: 

370 
"nat_set A \<Longrightarrow> finite A = finite (nat ` A)" 

371 
"is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)" 

372 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)" 

373 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)" 

374 
"nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)" 

375 
by (simp_all only: is_nat_def transfer_nat_int_set_relations 

376 
transfer_nat_int_set_return_embed nat_0_le) 

377 

378 
lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A" 

379 
by (simp only: transfer_nat_int_set_relations 

380 
transfer_nat_int_set_function_closures 

381 
transfer_nat_int_set_return_embed nat_0_le) 

382 

383 
lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow> 

384 
{(x::nat). P x} = {x. P' x}" 

385 
by auto 

386 

35644  387 
declare transfer_morphism_int_nat [transfer add 
31708  388 
return: transfer_int_nat_set_functions 
389 
transfer_int_nat_set_function_closures 

390 
transfer_int_nat_set_relations 

391 
transfer_int_nat_set_return_embed 

392 
cong: transfer_int_nat_set_cong 

393 
] 

394 

395 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

396 
text {* setsum and setprod *} 
31708  397 

398 
(* this handles the case where the *domain* of f is int *) 

399 
lemma transfer_int_nat_sum_prod: 

400 
"nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)" 

401 
"nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)" 

402 
apply (subst setsum_reindex) 

403 
apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff) 

404 
apply (subst setprod_reindex) 

405 
apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff 

406 
cong: setprod_cong) 

407 
done 

408 

409 
(* this handles the case where the *range* of f is int *) 

410 
lemma transfer_int_nat_sum_prod2: 

411 
"(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)" 

412 
"(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> 

413 
setprod f A = int(setprod (%x. nat (f x)) A)" 

414 
unfolding is_nat_def 

415 
apply (subst int_setsum, auto) 

416 
apply (subst int_setprod, auto simp add: cong: setprod_cong) 

417 
done 

418 

35644  419 
declare transfer_morphism_int_nat [transfer add 
31708  420 
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2 
421 
cong: setsum_cong setprod_cong] 

422 

423 
end 