author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47324  ed2bad9b7c6a 
child 48891  c0eafbd55de3 
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 
47324
ed2bad9b7c6a
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
huffman
parents:
47255
diff
changeset

8 
uses ("Tools/legacy_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" 
42870
36abaf4cce1f
clarified vacuous nature of predicate "transfer_morphism"  equivalent to previous definiton
krauss
parents:
39302
diff
changeset

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

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

16 
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

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

18 

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

19 
use "Tools/legacy_transfer.ML" 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
32558
diff
changeset

20 

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

21 
setup Legacy_Transfer.setup 
33318
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 

31708  24 
subsection {* Set up transfer from nat to int *} 
25 

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

26 
text {* set up transfer direction *} 
31708  27 

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

28 
lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" .. 
31708  29 

35683  30 
declare transfer_morphism_nat_int [transfer add 
31 
mode: manual 

31708  32 
return: nat_0_le 
35683  33 
labels: nat_int 
31708  34 
] 
35 

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

36 
text {* basic functions and relations *} 
31708  37 

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

41 
"(2::nat) = nat 2" 

42 
"(3::nat) = nat 3" 

43 
by auto 

44 

45 
definition 

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

47 
where 

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

49 

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

51 
by (simp add: tsub_def) 

52 

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

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

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

58 
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

59 
nat_power_eq tsub_def) 
31708  60 

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

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

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

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

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

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

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

70 
"int z >= 0" 

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

71 
by (auto simp add: zero_le_mult_iff tsub_def) 
31708  72 

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

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

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

32558  82 
by (auto simp add: zdvd_int) 
31708  83 

84 

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

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

86 

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

87 
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

88 
by (simp split add: split_nat) 
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 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

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

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

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

94 
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

95 
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

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

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

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

99 
qed 
31708  100 

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

104 
by (rule all_nat, rule ex_nat) 

105 

106 
(* should we restrict these? *) 

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

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

109 
by auto 

110 

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

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

113 
by auto 

114 

35644  115 
declare transfer_morphism_nat_int [transfer add 
31708  116 
cong: all_cong ex_cong] 
117 

118 

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

119 
text {* if *} 
31708  120 

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

31708  123 
by auto 
124 

125 

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

126 
text {* operations with sets *} 
31708  127 

128 
definition 

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

130 
where 

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

132 

133 
lemma transfer_nat_int_set_functions: 

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

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

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

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

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

139 
apply (rule card_image [symmetric]) 

140 
apply (auto simp add: inj_on_def image_def) 

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

146 
apply auto 

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

148 
apply auto 

149 
done 

150 

151 
lemma transfer_nat_int_set_function_closures: 

152 
"nat_set {}" 

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

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

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

156 
"nat_set (int ` C)" 

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

158 
unfolding nat_set_def apply auto 

159 
done 

160 

161 
lemma transfer_nat_int_set_relations: 

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

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

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

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

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

167 
apply (rule iffI) 

168 
apply (erule finite_imageI) 

169 
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

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

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

174 
done 

175 

176 
lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow> 

177 
(int ` nat ` A = A)" 

178 
by (auto simp add: nat_set_def image_def) 

179 

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

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

182 
by auto 

183 

35644  184 
declare transfer_morphism_nat_int [transfer add 
31708  185 
return: transfer_nat_int_set_functions 
186 
transfer_nat_int_set_function_closures 

187 
transfer_nat_int_set_relations 

188 
transfer_nat_int_set_return_embed 

189 
cong: transfer_nat_int_set_cong 

190 
] 

191 

192 

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

193 
text {* setsum and setprod *} 
31708  194 

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

196 
lemma transfer_nat_int_sum_prod: 

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

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

199 
apply (subst setsum_reindex) 

200 
apply (unfold inj_on_def, auto) 

201 
apply (subst setprod_reindex) 

202 
apply (unfold inj_on_def o_def, auto) 

203 
done 

204 

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

206 
lemma transfer_nat_int_sum_prod2: 

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

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

209 
apply (subst int_setsum [symmetric]) 

210 
apply auto 

211 
apply (subst int_setprod [symmetric]) 

212 
apply auto 

213 
done 

214 

215 
lemma transfer_nat_int_sum_prod_closure: 

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

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

218 
unfolding nat_set_def 

219 
apply (rule setsum_nonneg) 

220 
apply auto 

221 
apply (rule setprod_nonneg) 

222 
apply auto 

223 
done 

224 

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

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

227 

228 
also: what does =simp=> do? 

229 

230 
lemma transfer_nat_int_sum_prod_closure: 

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

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

233 
unfolding nat_set_def simp_implies_def 

234 
apply (rule setsum_nonneg) 

235 
apply auto 

236 
apply (rule setprod_nonneg) 

237 
apply auto 

238 
done 

239 
*) 

240 

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

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

243 
with the previously mentioned rule turned on? *) 

244 

245 
lemma transfer_nat_int_sum_prod_cong: 

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

247 
setsum f A = setsum g B" 

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

249 
setprod f A = setprod g B" 

250 
unfolding nat_set_def 

251 
apply (subst setsum_cong, assumption) 

252 
apply auto [2] 

253 
apply (subst setprod_cong, assumption, auto) 

254 
done 

255 

35644  256 
declare transfer_morphism_nat_int [transfer add 
31708  257 
return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2 
258 
transfer_nat_int_sum_prod_closure 

259 
cong: transfer_nat_int_sum_prod_cong] 

260 

261 

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

263 

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

264 
text {* set up transfer direction *} 
31708  265 

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

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

35644  268 
declare transfer_morphism_int_nat [transfer add 
31708  269 
mode: manual 
270 
return: nat_int 

35683  271 
labels: int_nat 
31708  272 
] 
273 

274 

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

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

276 

31708  277 
definition 
278 
is_nat :: "int \<Rightarrow> bool" 

279 
where 

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

281 

282 
lemma transfer_int_nat_numerals: 

283 
"0 = int 0" 

284 
"1 = int 1" 

285 
"2 = int 2" 

286 
"3 = int 3" 

287 
by auto 

288 

289 
lemma transfer_int_nat_functions: 

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

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

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

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

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

294 
by (auto simp add: int_mult tsub_def int_power) 
31708  295 

296 
lemma transfer_int_nat_function_closures: 

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

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

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

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

301 
"is_nat 0" 

302 
"is_nat 1" 

303 
"is_nat 2" 

304 
"is_nat 3" 

305 
"is_nat (int z)" 

306 
by (simp_all only: is_nat_def transfer_nat_int_function_closures) 

307 

308 
lemma transfer_int_nat_relations: 

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

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

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

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

313 
by (auto simp add: zdvd_int) 
32121  314 

35644  315 
declare transfer_morphism_int_nat [transfer add return: 
31708  316 
transfer_int_nat_numerals 
317 
transfer_int_nat_functions 

318 
transfer_int_nat_function_closures 

319 
transfer_int_nat_relations 

320 
] 

321 

322 

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

323 
text {* firstorder quantifiers *} 
31708  324 

325 
lemma transfer_int_nat_quantifiers: 

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

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

328 
apply (subst all_nat) 

329 
apply auto [1] 

330 
apply (subst ex_nat) 

331 
apply auto 

332 
done 

333 

35644  334 
declare transfer_morphism_int_nat [transfer add 
31708  335 
return: transfer_int_nat_quantifiers] 
336 

337 

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

338 
text {* if *} 
31708  339 

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

341 
int (if P then x else y)" 

342 
by auto 

343 

35644  344 
declare transfer_morphism_int_nat [transfer add return: int_if_cong] 
31708  345 

346 

347 

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

348 
text {* operations with sets *} 
31708  349 

350 
lemma transfer_int_nat_set_functions: 

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

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

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

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

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

356 
(* need all variants of these! *) 

357 
by (simp_all only: is_nat_def transfer_nat_int_set_functions 

358 
transfer_nat_int_set_function_closures 

359 
transfer_nat_int_set_return_embed nat_0_le 

360 
cong: transfer_nat_int_set_cong) 

361 

362 
lemma transfer_int_nat_set_function_closures: 

363 
"nat_set {}" 

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

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

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

367 
"nat_set (int ` C)" 

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

369 
by (simp_all only: transfer_nat_int_set_function_closures is_nat_def) 

370 

371 
lemma transfer_int_nat_set_relations: 

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

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

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

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

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

377 
by (simp_all only: is_nat_def transfer_nat_int_set_relations 

378 
transfer_nat_int_set_return_embed nat_0_le) 

379 

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

381 
by (simp only: transfer_nat_int_set_relations 

382 
transfer_nat_int_set_function_closures 

383 
transfer_nat_int_set_return_embed nat_0_le) 

384 

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

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

387 
by auto 

388 

35644  389 
declare transfer_morphism_int_nat [transfer add 
31708  390 
return: transfer_int_nat_set_functions 
391 
transfer_int_nat_set_function_closures 

392 
transfer_int_nat_set_relations 

393 
transfer_int_nat_set_return_embed 

394 
cong: transfer_int_nat_set_cong 

395 
] 

396 

397 

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

398 
text {* setsum and setprod *} 
31708  399 

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

401 
lemma transfer_int_nat_sum_prod: 

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

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

404 
apply (subst setsum_reindex) 

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

406 
apply (subst setprod_reindex) 

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

408 
cong: setprod_cong) 

409 
done 

410 

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

412 
lemma transfer_int_nat_sum_prod2: 

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

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

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

416 
unfolding is_nat_def 

417 
apply (subst int_setsum, auto) 

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

419 
done 

420 

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

424 

425 
end 