author  haftmann 
Thu, 18 Mar 2010 13:56:33 +0100  
changeset 35821  ee34f03a7d26 
parent 35683  70ace653fe77 
child 39198  f967a16dfcdd 
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 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

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

8 
uses ("Tools/transfer.ML") 
31708  9 
begin 
10 

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

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

12 

35821  13 
definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
14 
where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))" 

35644  15 

16 
lemma transfer_morphismI: 

35821  17 
assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)" 
18 
shows "transfer_morphism f A" 

19 
using assms by (auto simp add: transfer_morphism_def) 

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 
use "Tools/transfer.ML" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

22 

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

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

24 

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

25 

31708  26 
subsection {* Set up transfer from nat to int *} 
27 

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

28 
text {* set up transfer direction *} 
31708  29 

35644  30 
lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" 
35821  31 
by (rule transfer_morphismI) simp 
31708  32 

35683  33 
declare transfer_morphism_nat_int [transfer add 
34 
mode: manual 

31708  35 
return: nat_0_le 
35683  36 
labels: nat_int 
31708  37 
] 
38 

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

39 
text {* basic functions and relations *} 
31708  40 

35683  41 
lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]: 
31708  42 
"(0::nat) = nat 0" 
43 
"(1::nat) = nat 1" 

44 
"(2::nat) = nat 2" 

45 
"(3::nat) = nat 3" 

46 
by auto 

47 

48 
definition 

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

50 
where 

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

52 

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

54 
by (simp add: tsub_def) 

55 

35683  56 
lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]: 
31708  57 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)" 
58 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)" 

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

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

61 
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

62 
nat_power_eq tsub_def) 
31708  63 

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

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

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

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

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

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

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

73 
"int z >= 0" 

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

74 
by (auto simp add: zero_le_mult_iff tsub_def) 
31708  75 

35683  76 
lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]: 
31708  77 
"x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> 
78 
(nat (x::int) = nat y) = (x = y)" 

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

80 
(nat (x::int) < nat y) = (x < y)" 

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

82 
(nat (x::int) <= nat y) = (x <= y)" 

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

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

32558  85 
by (auto simp add: zdvd_int) 
31708  86 

87 

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

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

89 

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

90 
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

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

92 

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

93 
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

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

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

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

97 
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

98 
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

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

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

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

102 
qed 
31708  103 

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

107 
by (rule all_nat, rule ex_nat) 

108 

109 
(* should we restrict these? *) 

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

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

112 
by auto 

113 

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

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

116 
by auto 

117 

35644  118 
declare transfer_morphism_nat_int [transfer add 
31708  119 
cong: all_cong ex_cong] 
120 

121 

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

122 
text {* if *} 
31708  123 

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

31708  126 
by auto 
127 

128 

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

129 
text {* operations with sets *} 
31708  130 

131 
definition 

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

133 
where 

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

135 

136 
lemma transfer_nat_int_set_functions: 

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

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

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

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

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

142 
apply (rule card_image [symmetric]) 

143 
apply (auto simp add: inj_on_def image_def) 

144 
apply (rule_tac x = "int x" in bexI) 

145 
apply auto 

146 
apply (rule_tac x = "int x" in bexI) 

147 
apply auto 

148 
apply (rule_tac x = "int x" in bexI) 

149 
apply auto 

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

151 
apply auto 

152 
done 

153 

154 
lemma transfer_nat_int_set_function_closures: 

155 
"nat_set {}" 

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

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

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

159 
"nat_set (int ` C)" 

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

161 
unfolding nat_set_def apply auto 

162 
done 

163 

164 
lemma transfer_nat_int_set_relations: 

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

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

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

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

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

170 
apply (rule iffI) 

171 
apply (erule finite_imageI) 

172 
apply (erule finite_imageD) 

173 
apply (auto simp add: image_def expand_set_eq inj_on_def) 

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

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

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

177 
done 

178 

179 
lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow> 

180 
(int ` nat ` A = A)" 

181 
by (auto simp add: nat_set_def image_def) 

182 

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

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

185 
by auto 

186 

35644  187 
declare transfer_morphism_nat_int [transfer add 
31708  188 
return: transfer_nat_int_set_functions 
189 
transfer_nat_int_set_function_closures 

190 
transfer_nat_int_set_relations 

191 
transfer_nat_int_set_return_embed 

192 
cong: transfer_nat_int_set_cong 

193 
] 

194 

195 

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

196 
text {* setsum and setprod *} 
31708  197 

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

199 
lemma transfer_nat_int_sum_prod: 

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

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

202 
apply (subst setsum_reindex) 

203 
apply (unfold inj_on_def, auto) 

204 
apply (subst setprod_reindex) 

205 
apply (unfold inj_on_def o_def, auto) 

206 
done 

207 

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

209 
lemma transfer_nat_int_sum_prod2: 

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

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

212 
apply (subst int_setsum [symmetric]) 

213 
apply auto 

214 
apply (subst int_setprod [symmetric]) 

215 
apply auto 

216 
done 

217 

218 
lemma transfer_nat_int_sum_prod_closure: 

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

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

221 
unfolding nat_set_def 

222 
apply (rule setsum_nonneg) 

223 
apply auto 

224 
apply (rule setprod_nonneg) 

225 
apply auto 

226 
done 

227 

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

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

230 

231 
also: what does =simp=> do? 

232 

233 
lemma transfer_nat_int_sum_prod_closure: 

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

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

236 
unfolding nat_set_def simp_implies_def 

237 
apply (rule setsum_nonneg) 

238 
apply auto 

239 
apply (rule setprod_nonneg) 

240 
apply auto 

241 
done 

242 
*) 

243 

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

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

246 
with the previously mentioned rule turned on? *) 

247 

248 
lemma transfer_nat_int_sum_prod_cong: 

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

250 
setsum f A = setsum g B" 

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

252 
setprod f A = setprod g B" 

253 
unfolding nat_set_def 

254 
apply (subst setsum_cong, assumption) 

255 
apply auto [2] 

256 
apply (subst setprod_cong, assumption, auto) 

257 
done 

258 

35644  259 
declare transfer_morphism_nat_int [transfer add 
31708  260 
return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2 
261 
transfer_nat_int_sum_prod_closure 

262 
cong: transfer_nat_int_sum_prod_cong] 

263 

264 

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

266 

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

267 
text {* set up transfer direction *} 
31708  268 

35683  269 
lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" 
35821  270 
by (rule transfer_morphismI) simp 
31708  271 

35644  272 
declare transfer_morphism_int_nat [transfer add 
31708  273 
mode: manual 
274 
return: nat_int 

35683  275 
labels: int_nat 
31708  276 
] 
277 

278 

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

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

280 

31708  281 
definition 
282 
is_nat :: "int \<Rightarrow> bool" 

283 
where 

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

285 

286 
lemma transfer_int_nat_numerals: 

287 
"0 = int 0" 

288 
"1 = int 1" 

289 
"2 = int 2" 

290 
"3 = int 3" 

291 
by auto 

292 

293 
lemma transfer_int_nat_functions: 

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

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

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

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

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

298 
by (auto simp add: int_mult tsub_def int_power) 
31708  299 

300 
lemma transfer_int_nat_function_closures: 

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

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

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

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

305 
"is_nat 0" 

306 
"is_nat 1" 

307 
"is_nat 2" 

308 
"is_nat 3" 

309 
"is_nat (int z)" 

310 
by (simp_all only: is_nat_def transfer_nat_int_function_closures) 

311 

312 
lemma transfer_int_nat_relations: 

313 
"(int x = int y) = (x = y)" 

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

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

316 
"(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

317 
by (auto simp add: zdvd_int) 
32121  318 

35644  319 
declare transfer_morphism_int_nat [transfer add return: 
31708  320 
transfer_int_nat_numerals 
321 
transfer_int_nat_functions 

322 
transfer_int_nat_function_closures 

323 
transfer_int_nat_relations 

324 
] 

325 

326 

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

327 
text {* firstorder quantifiers *} 
31708  328 

329 
lemma transfer_int_nat_quantifiers: 

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

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

332 
apply (subst all_nat) 

333 
apply auto [1] 

334 
apply (subst ex_nat) 

335 
apply auto 

336 
done 

337 

35644  338 
declare transfer_morphism_int_nat [transfer add 
31708  339 
return: transfer_int_nat_quantifiers] 
340 

341 

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

342 
text {* if *} 
31708  343 

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

345 
int (if P then x else y)" 

346 
by auto 

347 

35644  348 
declare transfer_morphism_int_nat [transfer add return: int_if_cong] 
31708  349 

350 

351 

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

352 
text {* operations with sets *} 
31708  353 

354 
lemma transfer_int_nat_set_functions: 

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

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

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

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

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

360 
(* need all variants of these! *) 

361 
by (simp_all only: is_nat_def transfer_nat_int_set_functions 

362 
transfer_nat_int_set_function_closures 

363 
transfer_nat_int_set_return_embed nat_0_le 

364 
cong: transfer_nat_int_set_cong) 

365 

366 
lemma transfer_int_nat_set_function_closures: 

367 
"nat_set {}" 

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

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

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

371 
"nat_set (int ` C)" 

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

373 
by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) 

374 

375 
lemma transfer_int_nat_set_relations: 

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

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

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

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

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

381 
by (simp_all only: is_nat_def transfer_nat_int_set_relations 

382 
transfer_nat_int_set_return_embed nat_0_le) 

383 

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

385 
by (simp only: transfer_nat_int_set_relations 

386 
transfer_nat_int_set_function_closures 

387 
transfer_nat_int_set_return_embed nat_0_le) 

388 

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

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

391 
by auto 

392 

35644  393 
declare transfer_morphism_int_nat [transfer add 
31708  394 
return: transfer_int_nat_set_functions 
395 
transfer_int_nat_set_function_closures 

396 
transfer_int_nat_set_relations 

397 
transfer_int_nat_set_return_embed 

398 
cong: transfer_int_nat_set_cong 

399 
] 

400 

401 

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

402 
text {* setsum and setprod *} 
31708  403 

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

405 
lemma transfer_int_nat_sum_prod: 

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

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

408 
apply (subst setsum_reindex) 

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

410 
apply (subst setprod_reindex) 

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

412 
cong: setprod_cong) 

413 
done 

414 

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

416 
lemma transfer_int_nat_sum_prod2: 

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

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

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

420 
unfolding is_nat_def 

421 
apply (subst int_setsum, auto) 

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

423 
done 

424 

35644  425 
declare transfer_morphism_int_nat [transfer add 
31708  426 
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2 
427 
cong: setsum_cong setprod_cong] 

428 

429 
end 