author  berghofe 
Fri, 09 Jun 2006 17:32:38 +0200  
changeset 19834  2290cc06049b 
parent 19772  45897b49fdd2 
child 19856  7408a891424e 
permissions  rwrr 
17870  1 
(* $Id$ *) 
2 

19494  3 
theory Nominal 
17870  4 
imports Main 
18068  5 
uses 
6 
("nominal_atoms.ML") 

7 
("nominal_package.ML") 

18264  8 
("nominal_induct.ML") 
18068  9 
("nominal_permeq.ML") 
17870  10 
begin 
11 

12 
section {* Permutations *} 

13 
(*======================*) 

14 

15 
types 

16 
'x prm = "('x \<times> 'x) list" 

17 

19477  18 
(* polymorphic operations for permutation and swapping *) 
17870  19 
consts 
18491  20 
perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) 
17870  21 
swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" 
22 

19477  23 
(* for the decision procedure involving permutations *) 
24 
(* (to make the permcomposition to be terminating *) 

25 
constdefs 

26 
"perm_aux pi x \<equiv> pi\<bullet>x" 

27 

17870  28 
(* permutation on sets *) 
19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

29 
defs (unchecked overloaded) 
17870  30 
perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a  a. a\<in>X}" 
31 

18656  32 
lemma perm_empty: 
33 
shows "pi\<bullet>{} = {}" 

34 
by (simp add: perm_set_def) 

35 

18264  36 
lemma perm_union: 
37 
shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)" 

38 
by (auto simp add: perm_set_def) 

39 

18656  40 
lemma perm_insert: 
41 
shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)" 

42 
by (auto simp add: perm_set_def) 

43 

17870  44 
(* permutation on units and products *) 
19687  45 
primrec (unchecked perm_unit) 
46 
"pi\<bullet>() = ()" 

47 

48 
primrec (unchecked perm_prod) 

49 
"pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)" 

17870  50 

51 
lemma perm_fst: 

52 
"pi\<bullet>(fst x) = fst (pi\<bullet>x)" 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

53 
by (cases x) simp 
17870  54 

55 
lemma perm_snd: 

56 
"pi\<bullet>(snd x) = snd (pi\<bullet>x)" 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

57 
by (cases x) simp 
17870  58 

59 
(* permutation on lists *) 

19687  60 
primrec (unchecked perm_list) 
61 
perm_nil_def: "pi\<bullet>[] = []" 

62 
perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)" 

17870  63 

64 
lemma perm_append: 

65 
fixes pi :: "'x prm" 

66 
and l1 :: "'a list" 

67 
and l2 :: "'a list" 

68 
shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)" 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

69 
by (induct l1) auto 
17870  70 

71 
lemma perm_rev: 

72 
fixes pi :: "'x prm" 

73 
and l :: "'a list" 

74 
shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)" 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

75 
by (induct l) (simp_all add: perm_append) 
17870  76 

77 
(* permutation on functions *) 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

78 
defs (unchecked overloaded) 
17870  79 
perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))" 
80 

81 
(* permutation on bools *) 

19687  82 
primrec (unchecked perm_bool) 
17870  83 
perm_true_def: "pi\<bullet>True = True" 
84 
perm_false_def: "pi\<bullet>False = False" 

85 

18264  86 
lemma perm_bool: 
87 
shows "pi\<bullet>(b::bool) = b" 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

88 
by (cases b) auto 
18264  89 

17870  90 
(* permutation on options *) 
19687  91 
primrec (unchecked perm_option) 
92 
perm_some_def: "pi\<bullet>Some(x) = Some(pi\<bullet>x)" 

93 
perm_none_def: "pi\<bullet>None = None" 

17870  94 

95 
(* a "private" copy of the option type used in the abstraction function *) 

18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18578
diff
changeset

96 
datatype 'a noption = nSome 'a  nNone 
17870  97 

19687  98 
primrec (unchecked perm_noption) 
99 
perm_nSome_def: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)" 

100 
perm_nNone_def: "pi\<bullet>nNone = nNone" 

18600  101 

102 
(* a "private" copy of the product type used in the nominal induct method *) 

103 
datatype ('a,'b) nprod = nPair 'a 'b 

104 

19687  105 
primrec (unchecked perm_nprod) 
106 
perm_nProd_def: "pi\<bullet>(nPair x1 x2) = nPair (pi\<bullet>x1) (pi\<bullet>x2)" 

17870  107 

108 
(* permutation on characters (used in strings) *) 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

109 
defs (unchecked overloaded) 
17870  110 
perm_char_def: "pi\<bullet>(s::char) \<equiv> s" 
111 

112 
(* permutation on ints *) 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

113 
defs (unchecked overloaded) 
17870  114 
perm_int_def: "pi\<bullet>(i::int) \<equiv> i" 
115 

116 
(* permutation on nats *) 

19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

117 
defs (unchecked overloaded) 
17870  118 
perm_nat_def: "pi\<bullet>(i::nat) \<equiv> i" 
119 

120 
section {* permutation equality *} 

121 
(*==============================*) 

122 

123 
constdefs 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

124 
prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) 
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

125 
"pi1 \<triangleq> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a" 
17870  126 

127 
section {* Support, Freshness and Supports*} 

128 
(*========================================*) 

129 
constdefs 

130 
supp :: "'a \<Rightarrow> ('x set)" 

131 
"supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}" 

132 

17871  133 
fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) 
17870  134 
"a \<sharp> x \<equiv> a \<notin> supp x" 
135 

136 
supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80) 

137 
"S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)" 

138 

139 
lemma supp_fresh_iff: 

140 
fixes x :: "'a" 

141 
shows "(supp x) = {a::'x. \<not>a\<sharp>x}" 

142 
apply(simp add: fresh_def) 

143 
done 

144 

145 
lemma supp_unit: 

146 
shows "supp () = {}" 

147 
by (simp add: supp_def) 

148 

18264  149 
lemma supp_set_empty: 
150 
shows "supp {} = {}" 

151 
by (force simp add: supp_def perm_set_def) 

152 

153 
lemma supp_singleton: 

154 
shows "supp {x} = supp x" 

155 
by (force simp add: supp_def perm_set_def) 

156 

17870  157 
lemma supp_prod: 
158 
fixes x :: "'a" 

159 
and y :: "'b" 

160 
shows "(supp (x,y)) = (supp x)\<union>(supp y)" 

161 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

162 

18600  163 
lemma supp_nprod: 
164 
fixes x :: "'a" 

165 
and y :: "'b" 

166 
shows "(supp (nPair x y)) = (supp x)\<union>(supp y)" 

167 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

168 

17870  169 
lemma supp_list_nil: 
170 
shows "supp [] = {}" 

171 
apply(simp add: supp_def) 

172 
done 

173 

174 
lemma supp_list_cons: 

175 
fixes x :: "'a" 

176 
and xs :: "'a list" 

177 
shows "supp (x#xs) = (supp x)\<union>(supp xs)" 

178 
apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq) 

179 
done 

180 

181 
lemma supp_list_append: 

182 
fixes xs :: "'a list" 

183 
and ys :: "'a list" 

184 
shows "supp (xs@ys) = (supp xs)\<union>(supp ys)" 

185 
by (induct xs, auto simp add: supp_list_nil supp_list_cons) 

186 

187 
lemma supp_list_rev: 

188 
fixes xs :: "'a list" 

189 
shows "supp (rev xs) = (supp xs)" 

190 
by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil) 

191 

192 
lemma supp_bool: 

193 
fixes x :: "bool" 

194 
shows "supp (x) = {}" 

195 
apply(case_tac "x") 

196 
apply(simp_all add: supp_def) 

197 
done 

198 

199 
lemma supp_some: 

200 
fixes x :: "'a" 

201 
shows "supp (Some x) = (supp x)" 

202 
apply(simp add: supp_def) 

203 
done 

204 

205 
lemma supp_none: 

206 
fixes x :: "'a" 

207 
shows "supp (None) = {}" 

208 
apply(simp add: supp_def) 

209 
done 

210 

211 
lemma supp_int: 

212 
fixes i::"int" 

213 
shows "supp (i) = {}" 

214 
apply(simp add: supp_def perm_int_def) 

215 
done 

216 

18627  217 
lemma supp_char: 
218 
fixes c::"char" 

219 
shows "supp (c) = {}" 

220 
apply(simp add: supp_def perm_char_def) 

221 
done 

222 

223 
lemma supp_string: 

224 
fixes s::"string" 

225 
shows "supp (s) = {}" 

226 
apply(induct s) 

227 
apply(auto simp add: supp_char supp_list_nil supp_list_cons) 

228 
done 

229 

18264  230 
lemma fresh_set_empty: 
231 
shows "a\<sharp>{}" 

232 
by (simp add: fresh_def supp_set_empty) 

233 

18578  234 
lemma fresh_singleton: 
235 
shows "a\<sharp>{x} = a\<sharp>x" 

236 
by (simp add: fresh_def supp_singleton) 

237 

17870  238 
lemma fresh_prod: 
239 
fixes a :: "'x" 

240 
and x :: "'a" 

241 
and y :: "'b" 

242 
shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)" 

243 
by (simp add: fresh_def supp_prod) 

244 

245 
lemma fresh_list_nil: 

246 
fixes a :: "'x" 

18264  247 
shows "a\<sharp>[]" 
17870  248 
by (simp add: fresh_def supp_list_nil) 
249 

250 
lemma fresh_list_cons: 

251 
fixes a :: "'x" 

252 
and x :: "'a" 

253 
and xs :: "'a list" 

254 
shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)" 

255 
by (simp add: fresh_def supp_list_cons) 

256 

257 
lemma fresh_list_append: 

258 
fixes a :: "'x" 

259 
and xs :: "'a list" 

260 
and ys :: "'a list" 

261 
shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)" 

262 
by (simp add: fresh_def supp_list_append) 

263 

264 
lemma fresh_list_rev: 

265 
fixes a :: "'x" 

266 
and xs :: "'a list" 

267 
shows "a\<sharp>(rev xs) = a\<sharp>xs" 

268 
by (simp add: fresh_def supp_list_rev) 

269 

270 
lemma fresh_none: 

271 
fixes a :: "'x" 

272 
shows "a\<sharp>None" 

273 
apply(simp add: fresh_def supp_none) 

274 
done 

275 

276 
lemma fresh_some: 

277 
fixes a :: "'x" 

278 
and x :: "'a" 

279 
shows "a\<sharp>(Some x) = a\<sharp>x" 

280 
apply(simp add: fresh_def supp_some) 

281 
done 

282 

18294
bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

283 
text {* Normalization of freshness results; cf.\ @{text nominal_induct} *} 
bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

284 

18656  285 
lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C" 
18294
bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

286 
by (simp add: fresh_def supp_unit) 
bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

287 

18656  288 
lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)" 
18294
bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

289 
by rule (simp_all add: fresh_prod) 
bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

290 

bbfd64cc91ab
fresh_unit_elim and fresh_prod_elim  for nominal_induct;
wenzelm
parents:
18268
diff
changeset

291 

17870  292 
section {* Abstract Properties for Permutations and Atoms *} 
293 
(*=========================================================*) 

294 

295 
(* properties for being a permutation type *) 

296 
constdefs 

297 
"pt TYPE('a) TYPE('x) \<equiv> 

298 
(\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 

299 
(\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

300 
(\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)" 
17870  301 

302 
(* properties for being an atom type *) 

303 
constdefs 

304 
"at TYPE('x) \<equiv> 

305 
(\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and> 

306 
(\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and> 

307 
(\<forall>(a::'x) (b::'x) (c::'x). swap (a,b) c = (if a=c then b else (if b=c then a else c))) \<and> 

308 
(infinite (UNIV::'x set))" 

309 

310 
(* property of two atomtypes being disjoint *) 

311 
constdefs 

312 
"disjoint TYPE('x) TYPE('y) \<equiv> 

313 
(\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 

314 
(\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)" 

315 

316 
(* composition property of two permutation on a type 'a *) 

317 
constdefs 

318 
"cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 

319 
(\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 

320 

321 
(* property of having finite support *) 

322 
constdefs 

323 
"fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)" 

324 

325 
section {* Lemmas about the atomtype properties*} 

326 
(*==============================================*) 

327 

328 
lemma at1: 

329 
fixes x::"'x" 

330 
assumes a: "at TYPE('x)" 

331 
shows "([]::'x prm)\<bullet>x = x" 

332 
using a by (simp add: at_def) 

333 

334 
lemma at2: 

335 
fixes a ::"'x" 

336 
and b ::"'x" 

337 
and x ::"'x" 

338 
and pi::"'x prm" 

339 
assumes a: "at TYPE('x)" 

340 
shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)" 

341 
using a by (simp only: at_def) 

342 

343 
lemma at3: 

344 
fixes a ::"'x" 

345 
and b ::"'x" 

346 
and c ::"'x" 

347 
assumes a: "at TYPE('x)" 

348 
shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))" 

349 
using a by (simp only: at_def) 

350 

351 
(* rules to calculate simple premutations *) 

352 
lemmas at_calc = at2 at1 at3 

353 

354 
lemma at4: 

355 
assumes a: "at TYPE('x)" 

356 
shows "infinite (UNIV::'x set)" 

357 
using a by (simp add: at_def) 

358 

359 
lemma at_append: 

360 
fixes pi1 :: "'x prm" 

361 
and pi2 :: "'x prm" 

362 
and c :: "'x" 

363 
assumes at: "at TYPE('x)" 

364 
shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)" 

365 
proof (induct pi1) 

366 
case Nil show ?case by (simp add: at1[OF at]) 

367 
next 

368 
case (Cons x xs) 

18053
2719a6b7d95e
some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents:
18048
diff
changeset

369 
have "(xs@pi2)\<bullet>c = xs\<bullet>(pi2\<bullet>c)" by fact 
2719a6b7d95e
some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents:
18048
diff
changeset

370 
also have "(x#xs)@pi2 = x#(xs@pi2)" by simp 
2719a6b7d95e
some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents:
18048
diff
changeset

371 
ultimately show ?case by (cases "x", simp add: at2[OF at]) 
17870  372 
qed 
373 

374 
lemma at_swap: 

375 
fixes a :: "'x" 

376 
and b :: "'x" 

377 
and c :: "'x" 

378 
assumes at: "at TYPE('x)" 

379 
shows "swap (a,b) (swap (a,b) c) = c" 

380 
by (auto simp add: at3[OF at]) 

381 

382 
lemma at_rev_pi: 

383 
fixes pi :: "'x prm" 

384 
and c :: "'x" 

385 
assumes at: "at TYPE('x)" 

386 
shows "(rev pi)\<bullet>(pi\<bullet>c) = c" 

387 
proof(induct pi) 

388 
case Nil show ?case by (simp add: at1[OF at]) 

389 
next 

390 
case (Cons x xs) thus ?case 

391 
by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at]) 

392 
qed 

393 

394 
lemma at_pi_rev: 

395 
fixes pi :: "'x prm" 

396 
and x :: "'x" 

397 
assumes at: "at TYPE('x)" 

398 
shows "pi\<bullet>((rev pi)\<bullet>x) = x" 

399 
by (rule at_rev_pi[OF at, of "rev pi" _,simplified]) 

400 

401 
lemma at_bij1: 

402 
fixes pi :: "'x prm" 

403 
and x :: "'x" 

404 
and y :: "'x" 

405 
assumes at: "at TYPE('x)" 

406 
and a: "(pi\<bullet>x) = y" 

407 
shows "x=(rev pi)\<bullet>y" 

408 
proof  

409 
from a have "y=(pi\<bullet>x)" by (rule sym) 

410 
thus ?thesis by (simp only: at_rev_pi[OF at]) 

411 
qed 

412 

413 
lemma at_bij2: 

414 
fixes pi :: "'x prm" 

415 
and x :: "'x" 

416 
and y :: "'x" 

417 
assumes at: "at TYPE('x)" 

418 
and a: "((rev pi)\<bullet>x) = y" 

419 
shows "x=pi\<bullet>y" 

420 
proof  

421 
from a have "y=((rev pi)\<bullet>x)" by (rule sym) 

422 
thus ?thesis by (simp only: at_pi_rev[OF at]) 

423 
qed 

424 

425 
lemma at_bij: 

426 
fixes pi :: "'x prm" 

427 
and x :: "'x" 

428 
and y :: "'x" 

429 
assumes at: "at TYPE('x)" 

430 
shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)" 

431 
proof 

432 
assume "pi\<bullet>x = pi\<bullet>y" 

433 
hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 

434 
thus "x=y" by (simp only: at_rev_pi[OF at]) 

435 
next 

436 
assume "x=y" 

437 
thus "pi\<bullet>x = pi\<bullet>y" by simp 

438 
qed 

439 

440 
lemma at_supp: 

441 
fixes x :: "'x" 

442 
assumes at: "at TYPE('x)" 

443 
shows "supp x = {x}" 

444 
proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto) 

445 
assume f: "finite {b::'x. b \<noteq> x}" 

446 
have a1: "{b::'x. b \<noteq> x} = UNIV{x}" by force 

447 
have a2: "infinite (UNIV::'x set)" by (rule at4[OF at]) 

448 
from f a1 a2 show False by force 

449 
qed 

450 

451 
lemma at_fresh: 

452 
fixes a :: "'x" 

453 
and b :: "'x" 

454 
assumes at: "at TYPE('x)" 

455 
shows "(a\<sharp>b) = (a\<noteq>b)" 

456 
by (simp add: at_supp[OF at] fresh_def) 

457 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

458 
lemma at_prm_fresh: 
17870  459 
fixes c :: "'x" 
460 
and pi:: "'x prm" 

461 
assumes at: "at TYPE('x)" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

462 
and a: "c\<sharp>pi" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

463 
shows "pi\<bullet>c = c" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

464 
using a 
17870  465 
apply(induct pi) 
466 
apply(simp add: at1[OF at]) 

467 
apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at]) 

468 
done 

469 

470 
lemma at_prm_rev_eq: 

471 
fixes pi1 :: "'x prm" 

472 
and pi2 :: "'x prm" 

473 
assumes at: "at TYPE('x)" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

474 
shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)" 
17870  475 
proof (simp add: prm_eq_def, auto) 
476 
fix x 

477 
assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x" 

478 
hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp 

479 
hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at]) 

480 
hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at]) 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

481 
thus "pi1\<bullet>x = pi2\<bullet>x" by simp 
17870  482 
next 
483 
fix x 

484 
assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x" 

485 
hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp 

486 
hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at]) 

487 
hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at]) 

488 
thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp 

489 
qed 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

490 

b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

491 
lemma at_prm_eq_append: 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

492 
fixes pi1 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

493 
and pi2 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

494 
and pi3 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

495 
assumes at: "at TYPE('x)" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

496 
and a: "pi1 \<triangleq> pi2" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

497 
shows "(pi3@pi1) \<triangleq> (pi3@pi2)" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

498 
using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at]) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

499 

19325  500 
lemma at_prm_eq_append': 
501 
fixes pi1 :: "'x prm" 

502 
and pi2 :: "'x prm" 

503 
and pi3 :: "'x prm" 

504 
assumes at: "at TYPE('x)" 

505 
and a: "pi1 \<triangleq> pi2" 

506 
shows "(pi1@pi3) \<triangleq> (pi2@pi3)" 

507 
using a by (simp add: prm_eq_def at_append[OF at]) 

508 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

509 
lemma at_prm_eq_trans: 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

510 
fixes pi1 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

511 
and pi2 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

512 
and pi3 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

513 
assumes a1: "pi1 \<triangleq> pi2" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

514 
and a2: "pi2 \<triangleq> pi3" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

515 
shows "pi1 \<triangleq> pi3" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

516 
using a1 a2 by (auto simp add: prm_eq_def) 
17870  517 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

518 
lemma at_prm_eq_refl: 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

519 
fixes pi :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

520 
shows "pi \<triangleq> pi" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

521 
by (simp add: prm_eq_def) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

522 

17870  523 
lemma at_prm_rev_eq1: 
524 
fixes pi1 :: "'x prm" 

525 
and pi2 :: "'x prm" 

526 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

527 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)" 
17870  528 
by (simp add: at_prm_rev_eq[OF at]) 
529 

530 
lemma at_ds1: 

531 
fixes a :: "'x" 

532 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

533 
shows "[(a,a)] \<triangleq> []" 
17870  534 
by (force simp add: prm_eq_def at_calc[OF at]) 
535 

536 
lemma at_ds2: 

537 
fixes pi :: "'x prm" 

538 
and a :: "'x" 

539 
and b :: "'x" 

540 
assumes at: "at TYPE('x)" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

541 
shows "([(a,b)]@pi) \<triangleq> (pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)])" 
17870  542 
by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
543 
at_rev_pi[OF at] at_calc[OF at]) 

544 

545 
lemma at_ds3: 

546 
fixes a :: "'x" 

547 
and b :: "'x" 

548 
and c :: "'x" 

549 
assumes at: "at TYPE('x)" 

550 
and a: "distinct [a,b,c]" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

551 
shows "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" 
17870  552 
using a by (force simp add: prm_eq_def at_calc[OF at]) 
553 

554 
lemma at_ds4: 

555 
fixes a :: "'x" 

556 
and b :: "'x" 

557 
and pi :: "'x prm" 

558 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

559 
shows "(pi@[(a,(rev pi)\<bullet>b)]) \<triangleq> ([(pi\<bullet>a,b)]@pi)" 
17870  560 
by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
561 
at_pi_rev[OF at] at_rev_pi[OF at]) 

562 

563 
lemma at_ds5: 

564 
fixes a :: "'x" 

565 
and b :: "'x" 

566 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

567 
shows "[(a,b)] \<triangleq> [(b,a)]" 
17870  568 
by (force simp add: prm_eq_def at_calc[OF at]) 
569 

19164  570 
lemma at_ds5': 
571 
fixes a :: "'x" 

572 
and b :: "'x" 

573 
assumes at: "at TYPE('x)" 

574 
shows "[(a,b),(b,a)] \<triangleq> []" 

575 
by (force simp add: prm_eq_def at_calc[OF at]) 

576 

17870  577 
lemma at_ds6: 
578 
fixes a :: "'x" 

579 
and b :: "'x" 

580 
and c :: "'x" 

581 
assumes at: "at TYPE('x)" 

582 
and a: "distinct [a,b,c]" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

583 
shows "[(a,c),(a,b)] \<triangleq> [(b,c),(a,c)]" 
17870  584 
using a by (force simp add: prm_eq_def at_calc[OF at]) 
585 

586 
lemma at_ds7: 

587 
fixes pi :: "'x prm" 

588 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

589 
shows "((rev pi)@pi) \<triangleq> []" 
17870  590 
by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at]) 
591 

592 
lemma at_ds8_aux: 

593 
fixes pi :: "'x prm" 

594 
and a :: "'x" 

595 
and b :: "'x" 

596 
and c :: "'x" 

597 
assumes at: "at TYPE('x)" 

598 
shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)" 

599 
by (force simp add: at_calc[OF at] at_bij[OF at]) 

600 

601 
lemma at_ds8: 

602 
fixes pi1 :: "'x prm" 

603 
and pi2 :: "'x prm" 

604 
and a :: "'x" 

605 
and b :: "'x" 

606 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

607 
shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)" 
17870  608 
apply(induct_tac pi2) 
609 
apply(simp add: prm_eq_def) 

610 
apply(auto simp add: prm_eq_def) 

611 
apply(simp add: at2[OF at]) 

612 
apply(drule_tac x="aa" in spec) 

613 
apply(drule sym) 

614 
apply(simp) 

615 
apply(simp add: at_append[OF at]) 

616 
apply(simp add: at2[OF at]) 

617 
apply(simp add: at_ds8_aux[OF at]) 

618 
done 

619 

620 
lemma at_ds9: 

621 
fixes pi1 :: "'x prm" 

622 
and pi2 :: "'x prm" 

623 
and a :: "'x" 

624 
and b :: "'x" 

625 
assumes at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

626 
shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" 
17870  627 
apply(induct_tac pi2) 
628 
apply(simp add: prm_eq_def) 

629 
apply(auto simp add: prm_eq_def) 

630 
apply(simp add: at_append[OF at]) 

631 
apply(simp add: at2[OF at] at1[OF at]) 

632 
apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec) 

633 
apply(drule sym) 

634 
apply(simp) 

635 
apply(simp add: at_ds8_aux[OF at]) 

636 
apply(simp add: at_rev_pi[OF at]) 

637 
done 

638 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

639 
lemma at_ds10: 
19132  640 
fixes pi :: "'x prm" 
19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

641 
and a :: "'x" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

642 
and b :: "'x" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

643 
assumes at: "at TYPE('x)" 
19132  644 
and a: "b\<sharp>(rev pi)" 
645 
shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

646 
using a 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

647 
apply  
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

648 
apply(rule at_prm_eq_trans) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

649 
apply(rule at_ds2[OF at]) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

650 
apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at]) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

651 
apply(rule at_prm_eq_refl) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

652 
done 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

653 

17870  654 
"there always exists an atom not being in a finite set" 
655 
lemma ex_in_inf: 

656 
fixes A::"'x set" 

657 
assumes at: "at TYPE('x)" 

658 
and fs: "finite A" 

659 
shows "\<exists>c::'x. c\<notin>A" 

660 
proof  

661 
from fs at4[OF at] have "infinite ((UNIV::'x set)  A)" 

662 
by (simp add: Diff_infinite_finite) 

663 
hence "((UNIV::'x set)  A) \<noteq> ({}::'x set)" by (force simp only:) 

664 
hence "\<exists>c::'x. c\<in>((UNIV::'x set)  A)" by force 

665 
thus "\<exists>c::'x. c\<notin>A" by force 

666 
qed 

667 

668 
"there always exists a fresh name for an object with finite support" 

669 
lemma at_exists_fresh: 

670 
fixes x :: "'a" 

671 
assumes at: "at TYPE('x)" 

672 
and fs: "finite ((supp x)::'x set)" 

673 
shows "\<exists>c::'x. c\<sharp>x" 

674 
by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs]) 

675 

18657  676 
lemma at_finite_select: "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S" 
677 
apply (drule Diff_infinite_finite) 

678 
apply (simp add: at_def) 

679 
apply blast 

680 
apply (subgoal_tac "UNIV  S \<noteq> {}") 

681 
apply (simp only: ex_in_conv [symmetric]) 

682 
apply blast 

683 
apply (rule notI) 

684 
apply simp 

685 
done 

686 

19140  687 
lemma at_different: 
19132  688 
assumes at: "at TYPE('x)" 
19140  689 
shows "\<exists>(b::'x). a\<noteq>b" 
19132  690 
proof  
19140  691 
have "infinite (UNIV::'x set)" by (rule at4[OF at]) 
692 
hence inf2: "infinite (UNIV{a})" by (rule infinite_remove) 

19132  693 
have "(UNIV{a}) \<noteq> ({}::'x set)" 
694 
proof (rule_tac ccontr, drule_tac notnotD) 

695 
assume "UNIV{a} = ({}::'x set)" 

696 
with inf2 have "infinite ({}::'x set)" by simp 

697 
then show "False" by (auto intro: infinite_nonempty) 

698 
qed 

699 
hence "\<exists>(b::'x). b\<in>(UNIV{a})" by blast 

700 
then obtain b::"'x" where mem2: "b\<in>(UNIV{a})" by blast 

19140  701 
from mem2 have "a\<noteq>b" by blast 
702 
then show "\<exists>(b::'x). a\<noteq>b" by blast 

19132  703 
qed 
704 

17870  705 
"the atprops imply the ptprops" 
706 
lemma at_pt_inst: 

707 
assumes at: "at TYPE('x)" 

708 
shows "pt TYPE('x) TYPE('x)" 

709 
apply(auto simp only: pt_def) 

710 
apply(simp only: at1[OF at]) 

711 
apply(simp only: at_append[OF at]) 

18053
2719a6b7d95e
some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents:
18048
diff
changeset

712 
apply(simp only: prm_eq_def) 
17870  713 
done 
714 

715 
section {* finite support properties *} 

716 
(*===================================*) 

717 

718 
lemma fs1: 

719 
fixes x :: "'a" 

720 
assumes a: "fs TYPE('a) TYPE('x)" 

721 
shows "finite ((supp x)::'x set)" 

722 
using a by (simp add: fs_def) 

723 

724 
lemma fs_at_inst: 

725 
fixes a :: "'x" 

726 
assumes at: "at TYPE('x)" 

727 
shows "fs TYPE('x) TYPE('x)" 

728 
apply(simp add: fs_def) 

729 
apply(simp add: at_supp[OF at]) 

730 
done 

731 

732 
lemma fs_unit_inst: 

733 
shows "fs TYPE(unit) TYPE('x)" 

734 
apply(simp add: fs_def) 

735 
apply(simp add: supp_unit) 

736 
done 

737 

738 
lemma fs_prod_inst: 

739 
assumes fsa: "fs TYPE('a) TYPE('x)" 

740 
and fsb: "fs TYPE('b) TYPE('x)" 

741 
shows "fs TYPE('a\<times>'b) TYPE('x)" 

742 
apply(unfold fs_def) 

743 
apply(auto simp add: supp_prod) 

744 
apply(rule fs1[OF fsa]) 

745 
apply(rule fs1[OF fsb]) 

746 
done 

747 

18600  748 
lemma fs_nprod_inst: 
749 
assumes fsa: "fs TYPE('a) TYPE('x)" 

750 
and fsb: "fs TYPE('b) TYPE('x)" 

751 
shows "fs TYPE(('a,'b) nprod) TYPE('x)" 

752 
apply(unfold fs_def, rule allI) 

753 
apply(case_tac x) 

754 
apply(auto simp add: supp_nprod) 

755 
apply(rule fs1[OF fsa]) 

756 
apply(rule fs1[OF fsb]) 

757 
done 

758 

17870  759 
lemma fs_list_inst: 
760 
assumes fs: "fs TYPE('a) TYPE('x)" 

761 
shows "fs TYPE('a list) TYPE('x)" 

762 
apply(simp add: fs_def, rule allI) 

763 
apply(induct_tac x) 

764 
apply(simp add: supp_list_nil) 

765 
apply(simp add: supp_list_cons) 

766 
apply(rule fs1[OF fs]) 

767 
done 

768 

18431  769 
lemma fs_option_inst: 
770 
assumes fs: "fs TYPE('a) TYPE('x)" 

771 
shows "fs TYPE('a option) TYPE('x)" 

17870  772 
apply(simp add: fs_def, rule allI) 
18431  773 
apply(case_tac x) 
774 
apply(simp add: supp_none) 

775 
apply(simp add: supp_some) 

776 
apply(rule fs1[OF fs]) 

17870  777 
done 
778 

779 
section {* Lemmas about the permutation properties *} 

780 
(*=================================================*) 

781 

782 
lemma pt1: 

783 
fixes x::"'a" 

784 
assumes a: "pt TYPE('a) TYPE('x)" 

785 
shows "([]::'x prm)\<bullet>x = x" 

786 
using a by (simp add: pt_def) 

787 

788 
lemma pt2: 

789 
fixes pi1::"'x prm" 

790 
and pi2::"'x prm" 

791 
and x ::"'a" 

792 
assumes a: "pt TYPE('a) TYPE('x)" 

793 
shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)" 

794 
using a by (simp add: pt_def) 

795 

796 
lemma pt3: 

797 
fixes pi1::"'x prm" 

798 
and pi2::"'x prm" 

799 
and x ::"'a" 

800 
assumes a: "pt TYPE('a) TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

801 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x" 
17870  802 
using a by (simp add: pt_def) 
803 

804 
lemma pt3_rev: 

805 
fixes pi1::"'x prm" 

806 
and pi2::"'x prm" 

807 
and x ::"'a" 

808 
assumes pt: "pt TYPE('a) TYPE('x)" 

809 
and at: "at TYPE('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

810 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x" 
17870  811 
by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at]) 
812 

813 
section {* composition properties *} 

814 
(* ============================== *) 

815 
lemma cp1: 

816 
fixes pi1::"'x prm" 

817 
and pi2::"'y prm" 

818 
and x ::"'a" 

819 
assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" 

820 
shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)" 

821 
using cp by (simp add: cp_def) 

822 

823 
lemma cp_pt_inst: 

824 
assumes pt: "pt TYPE('a) TYPE('x)" 

825 
and at: "at TYPE('x)" 

826 
shows "cp TYPE('a) TYPE('x) TYPE('x)" 

827 
apply(auto simp add: cp_def pt2[OF pt,symmetric]) 

828 
apply(rule pt3[OF pt]) 

829 
apply(rule at_ds8[OF at]) 

830 
done 

831 

19638
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

832 
section {* disjointness properties *} 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

833 
(*=================================*) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

834 
lemma dj_perm_forget: 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

835 
fixes pi::"'y prm" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

836 
and x ::"'x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

837 
assumes dj: "disjoint TYPE('x) TYPE('y)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

838 
shows "pi\<bullet>x=x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

839 
using dj by (simp_all add: disjoint_def) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

840 

4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

841 
lemma dj_perm_perm_forget: 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

842 
fixes pi1::"'x prm" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

843 
and pi2::"'y prm" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

844 
assumes dj: "disjoint TYPE('x) TYPE('y)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

845 
shows "pi2\<bullet>pi1=pi1" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

846 
using dj by (induct pi1, auto simp add: disjoint_def) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

847 

4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

848 
lemma dj_cp: 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

849 
fixes pi1::"'x prm" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

850 
and pi2::"'y prm" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

851 
and x ::"'a" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

852 
assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

853 
and dj: "disjoint TYPE('y) TYPE('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

854 
shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

855 
by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj]) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

856 

4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

857 
lemma dj_supp: 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

858 
fixes a::"'x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

859 
assumes dj: "disjoint TYPE('x) TYPE('y)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

860 
shows "(supp a) = ({}::'y set)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

861 
apply(simp add: supp_def dj_perm_forget[OF dj]) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

862 
done 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

863 

17870  864 
section {* permutation type instances *} 
865 
(* ===================================*) 

866 

867 
lemma pt_set_inst: 

868 
assumes pt: "pt TYPE('a) TYPE('x)" 

869 
shows "pt TYPE('a set) TYPE('x)" 

870 
apply(simp add: pt_def) 

871 
apply(simp_all add: perm_set_def) 

872 
apply(simp add: pt1[OF pt]) 

873 
apply(force simp add: pt2[OF pt] pt3[OF pt]) 

874 
done 

875 

876 
lemma pt_list_nil: 

877 
fixes xs :: "'a list" 

878 
assumes pt: "pt TYPE('a) TYPE ('x)" 

879 
shows "([]::'x prm)\<bullet>xs = xs" 

880 
apply(induct_tac xs) 

881 
apply(simp_all add: pt1[OF pt]) 

882 
done 

883 

884 
lemma pt_list_append: 

885 
fixes pi1 :: "'x prm" 

886 
and pi2 :: "'x prm" 

887 
and xs :: "'a list" 

888 
assumes pt: "pt TYPE('a) TYPE ('x)" 

889 
shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)" 

890 
apply(induct_tac xs) 

891 
apply(simp_all add: pt2[OF pt]) 

892 
done 

893 

894 
lemma pt_list_prm_eq: 

895 
fixes pi1 :: "'x prm" 

896 
and pi2 :: "'x prm" 

897 
and xs :: "'a list" 

898 
assumes pt: "pt TYPE('a) TYPE ('x)" 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

899 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs" 
17870  900 
apply(induct_tac xs) 
901 
apply(simp_all add: prm_eq_def pt3[OF pt]) 

902 
done 

903 

904 
lemma pt_list_inst: 

905 
assumes pt: "pt TYPE('a) TYPE('x)" 

906 
shows "pt TYPE('a list) TYPE('x)" 

907 
apply(auto simp only: pt_def) 

908 
apply(rule pt_list_nil[OF pt]) 

909 
apply(rule pt_list_append[OF pt]) 

910 
apply(rule pt_list_prm_eq[OF pt],assumption) 

911 
done 

912 

913 
lemma pt_unit_inst: 

914 
shows "pt TYPE(unit) TYPE('x)" 

915 
by (simp add: pt_def) 

916 

917 
lemma pt_prod_inst: 

918 
assumes pta: "pt TYPE('a) TYPE('x)" 

919 
and ptb: "pt TYPE('b) TYPE('x)" 

920 
shows "pt TYPE('a \<times> 'b) TYPE('x)" 

921 
apply(auto simp add: pt_def) 

922 
apply(rule pt1[OF pta]) 

923 
apply(rule pt1[OF ptb]) 

924 
apply(rule pt2[OF pta]) 

925 
apply(rule pt2[OF ptb]) 

926 
apply(rule pt3[OF pta],assumption) 

927 
apply(rule pt3[OF ptb],assumption) 

928 
done 

929 

18600  930 
lemma pt_nprod_inst: 
931 
assumes pta: "pt TYPE('a) TYPE('x)" 

932 
and ptb: "pt TYPE('b) TYPE('x)" 

933 
shows "pt TYPE(('a,'b) nprod) TYPE('x)" 

934 
apply(auto simp add: pt_def) 

935 
apply(case_tac x) 

936 
apply(simp add: pt1[OF pta] pt1[OF ptb]) 

937 
apply(case_tac x) 

938 
apply(simp add: pt2[OF pta] pt2[OF ptb]) 

939 
apply(case_tac x) 

940 
apply(simp add: pt3[OF pta] pt3[OF ptb]) 

941 
done 

942 

17870  943 
lemma pt_fun_inst: 
944 
assumes pta: "pt TYPE('a) TYPE('x)" 

945 
and ptb: "pt TYPE('b) TYPE('x)" 

946 
and at: "at TYPE('x)" 

947 
shows "pt TYPE('a\<Rightarrow>'b) TYPE('x)" 

948 
apply(auto simp only: pt_def) 

949 
apply(simp_all add: perm_fun_def) 

950 
apply(simp add: pt1[OF pta] pt1[OF ptb]) 

951 
apply(simp add: pt2[OF pta] pt2[OF ptb]) 

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

952 
apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*) 
17870  953 
apply(simp add: pt3[OF pta] pt3[OF ptb]) 
954 
(*A*) 

955 
apply(simp add: at_prm_rev_eq[OF at]) 

956 
done 

957 

958 
lemma pt_option_inst: 

959 
assumes pta: "pt TYPE('a) TYPE('x)" 

960 
shows "pt TYPE('a option) TYPE('x)" 

961 
apply(auto simp only: pt_def) 

962 
apply(case_tac "x") 

963 
apply(simp_all add: pt1[OF pta]) 

964 
apply(case_tac "x") 

965 
apply(simp_all add: pt2[OF pta]) 

966 
apply(case_tac "x") 

967 
apply(simp_all add: pt3[OF pta]) 

968 
done 

969 

970 
lemma pt_noption_inst: 

971 
assumes pta: "pt TYPE('a) TYPE('x)" 

18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18578
diff
changeset

972 
shows "pt TYPE('a noption) TYPE('x)" 
17870  973 
apply(auto simp only: pt_def) 
974 
apply(case_tac "x") 

975 
apply(simp_all add: pt1[OF pta]) 

976 
apply(case_tac "x") 

977 
apply(simp_all add: pt2[OF pta]) 

978 
apply(case_tac "x") 

979 
apply(simp_all add: pt3[OF pta]) 

980 
done 

981 

982 
section {* further lemmas for permutation types *} 

983 
(*==============================================*) 

984 

985 
lemma pt_rev_pi: 

986 
fixes pi :: "'x prm" 

987 
and x :: "'a" 

988 
assumes pt: "pt TYPE('a) TYPE('x)" 

989 
and at: "at TYPE('x)" 

990 
shows "(rev pi)\<bullet>(pi\<bullet>x) = x" 

991 
proof  

18295
dd50de393330
changed \<sim> of permutation equality to \<triangleq>
urbanc
parents:
18294
diff
changeset

992 
have "((rev pi)@pi) \<triangleq> ([]::'x prm)" by (simp add: at_ds7[OF at]) 
17870  993 
hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
994 
thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt]) 

995 
qed 

996 

997 
lemma pt_pi_rev: 

998 
fixes pi :: "'x prm" 

999 
and x :: "'a" 

1000 
assumes pt: "pt TYPE('a) TYPE('x)" 

1001 
and at: "at TYPE('x)" 

1002 
shows "pi\<bullet>((rev pi)\<bullet>x) = x" 

1003 
by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified]) 

1004 

1005 
lemma pt_bij1: 

1006 
fixes pi :: "'x prm" 

1007 
and x :: "'a" 

1008 
and y :: "'a" 

1009 
assumes pt: "pt TYPE('a) TYPE('x)" 

1010 
and at: "at TYPE('x)" 

1011 
and a: "(pi\<bullet>x) = y" 

1012 
shows "x=(rev pi)\<bullet>y" 

1013 
proof  

1014 
from a have "y=(pi\<bullet>x)" by (rule sym) 

1015 
thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at]) 

1016 
qed 

1017 

1018 
lemma pt_bij2: 

1019 
fixes pi :: "'x prm" 

1020 
and x :: "'a" 

1021 
and y :: "'a" 

1022 
assumes pt: "pt TYPE('a) TYPE('x)" 

1023 
and at: "at TYPE('x)" 

1024 
and a: "x = (rev pi)\<bullet>y" 

1025 
shows "(pi\<bullet>x)=y" 

1026 
using a by (simp add: pt_pi_rev[OF pt, OF at]) 

1027 

1028 
lemma pt_bij: 

1029 
fixes pi :: "'x prm" 

1030 
and x :: "'a" 

1031 
and y :: "'a" 

1032 
assumes pt: "pt TYPE('a) TYPE('x)" 

1033 
and at: "at TYPE('x)" 

1034 
shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)" 

1035 
proof 

1036 
assume "pi\<bullet>x = pi\<bullet>y" 

1037 
hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 

1038 
thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at]) 

1039 
next 

1040 
assume "x=y" 

1041 
thus "pi\<bullet>x = pi\<bullet>y" by simp 

1042 
qed 

1043 

1044 
lemma pt_bij3: 

1045 
fixes pi :: "'x prm" 

1046 
and x :: "'a" 

1047 
and y :: "'a" 

1048 
assumes a: "x=y" 

1049 
shows "(pi\<bullet>x = pi\<bullet>y)" 

1050 
using a by simp 

1051 

1052 
lemma pt_bij4: 

1053 
fixes pi :: "'x prm" 

1054 
and x :: "'a" 

1055 
and y :: "'a" 

1056 
assumes pt: "pt TYPE('a) TYPE('x)" 

1057 
and at: "at TYPE('x)" 

1058 
and a: "pi\<bullet>x = pi\<bullet>y" 

1059 
shows "x = y" 

1060 
using a by (simp add: pt_bij[OF pt, OF at]) 

1061 

1062 
lemma pt_swap_bij: 

1063 
fixes a :: "'x" 

1064 
and b :: "'x" 

1065 
and x :: "'a" 

1066 
assumes pt: "pt TYPE('a) TYPE('x)" 

1067 
and at: "at TYPE('x)" 

1068 
shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x" 

1069 
by (rule pt_bij2[OF pt, OF at], simp) 

1070 

19164  1071 
lemma pt_swap_bij': 
1072 
fixes a :: "'x" 

1073 
and b :: "'x" 

1074 
and x :: "'a" 

1075 
assumes pt: "pt TYPE('a) TYPE('x)" 

1076 
and at: "at TYPE('x)" 

1077 
shows "[(a,b)]\<bullet>([(b,a)]\<bullet>x) = x" 

1078 
apply(simp add: pt2[OF pt,symmetric]) 

1079 
apply(rule trans) 

1080 
apply(rule pt3[OF pt]) 

1081 
apply(rule at_ds5'[OF at]) 

1082 
apply(rule pt1[OF pt]) 

1083 
done 

1084 

17870  1085 
lemma pt_set_bij1: 
1086 
fixes pi :: "'x prm" 

1087 
and x :: "'a" 

1088 
and X :: "'a set" 

1089 
assumes pt: "pt TYPE('a) TYPE('x)" 

1090 
and at: "at TYPE('x)" 

1091 
shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))" 

1092 
by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) 

1093 

1094 
lemma pt_set_bij1a: 

1095 
fixes pi :: "'x prm" 

1096 
and x :: "'a" 

1097 
and X :: "'a set" 

1098 
assumes pt: "pt TYPE('a) TYPE('x)" 

1099 
and at: "at TYPE('x)" 

1100 
shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)" 

1101 
by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) 

1102 

1103 
lemma pt_set_bij: 

1104 
fixes pi :: "'x prm" 

1105 
and x :: "'a" 

1106 
and X :: "'a set" 

1107 
assumes pt: "pt TYPE('a) TYPE('x)" 

1108 
and at: "at TYPE('x)" 

1109 
shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)" 

18053
2719a6b7d95e
some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents:
18048
diff
changeset

1110 
by (simp add: perm_set_def pt_bij[OF pt, OF at]) 
17870  1111 

1112 
lemma pt_set_bij2: 

1113 
fixes pi :: "'x prm" 

1114 
and x :: "'a" 

1115 
and X :: "'a set" 

1116 
assumes pt: "pt TYPE('a) TYPE('x)" 

1117 
and at: "at TYPE('x)" 

1118 
and a: "x\<in>X" 

1119 
shows "(pi\<bullet>x)\<in>(pi\<bullet>X)" 

1120 
using a by (simp add: pt_set_bij[OF pt, OF at]) 

1121 

18264  1122 
lemma pt_set_bij2a: 
1123 
fixes pi :: "'x prm" 

1124 
and x :: "'a" 

1125 
and X :: "'a set" 

1126 
assumes pt: "pt TYPE('a) TYPE('x)" 

1127 
and at: "at TYPE('x)" 

1128 
and a: "x\<in>((rev pi)\<bullet>X)" 

1129 
shows "(pi\<bullet>x)\<in>X" 

1130 
using a by (simp add: pt_set_bij1[OF pt, OF at]) 

1131 

17870  1132 
lemma pt_set_bij3: 
1133 
fixes pi :: "'x prm" 

1134 
and x :: "'a" 

1135 
and X :: "'a set" 

1136 
shows "pi\<bullet>(x\<in>X) = (x\<in>X)" 

1137 
apply(case_tac "x\<in>X = True") 

1138 
apply(auto) 

1139 
done 

1140 

18159
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1141 
lemma pt_subseteq_eqvt: 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1142 
fixes pi :: "'x prm" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1143 
and Y :: "'a set" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1144 
and X :: "'a set" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1145 
assumes pt: "pt TYPE('a) TYPE('x)" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1146 
and at: "at TYPE('x)" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1147 
shows "((pi\<bullet>X)\<subseteq>(pi\<bullet>Y)) = (X\<subseteq>Y)" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1148 
proof (auto) 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1149 
fix x::"'a" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1150 
assume a: "(pi\<bullet>X)\<subseteq>(pi\<bullet>Y)" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1151 
and "x\<in>X" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1152 
hence "(pi\<bullet>x)\<in>(pi\<bullet>X)" by (simp add: pt_set_bij[OF pt, OF at]) 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1153 
with a have "(pi\<bullet>x)\<in>(pi\<bullet>Y)" by force 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1154 
thus "x\<in>Y" by (simp add: pt_set_bij[OF pt, OF at]) 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1155 
next 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1156 
fix x::"'a" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1157 
assume a: "X\<subseteq>Y" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1158 
and "x\<in>(pi\<bullet>X)" 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1159 
thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at]) 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1160 
qed 
08282ca0402e
added a few equivariance lemmas (they need to be automated
urbanc
parents:
18068
diff
changeset

1161 

19772
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1162 
lemma pt_set_diff_eqvt: 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1163 
fixes X::"'a set" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1164 
and Y::"'a set" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1165 
and pi::"'x prm" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1166 
assumes pt: "pt TYPE('a) TYPE('x)" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1167 
and at: "at TYPE('x)" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1168 
shows "pi \<bullet> (X  Y) = (pi \<bullet> X)  (pi \<bullet> Y)" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1169 
by (auto simp add: perm_set_def pt_bij[OF pt, OF at]) 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1170 

45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1171 

17870  1172 
 "some helper lemmas for the pt_perm_supp_ineq lemma" 
1173 
lemma Collect_permI: 

1174 
fixes pi :: "'x prm" 

1175 
and x :: "'a" 

1176 
assumes a: "\<forall>x. (P1 x = P2 x)" 

1177 
shows "{pi\<bullet>x x. P1 x} = {pi\<bullet>x x. P2 x}" 

1178 
using a by force 

1179 

1180 
lemma Infinite_cong: 

1181 
assumes a: "X = Y" 

1182 
shows "infinite X = infinite Y" 

1183 
using a by (simp) 

1184 

1185 
lemma pt_set_eq_ineq: 

1186 
fixes pi :: "'y prm" 

1187 
assumes pt: "pt TYPE('x) TYPE('y)" 

1188 
and at: "at TYPE('y)" 

1189 
shows "{pi\<bullet>x x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}" 

1190 
by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) 

1191 

1192 
lemma pt_inject_on_ineq: 

1193 
fixes X :: "'y set" 

1194 
and pi :: "'x prm" 

1195 
assumes pt: "pt TYPE('y) TYPE('x)" 

1196 
and at: "at TYPE('x)" 

1197 
shows "inj_on (perm pi) X" 

1198 
proof (unfold inj_on_def, intro strip) 

1199 
fix x::"'y" and y::"'y" 

1200 
assume "pi\<bullet>x = pi\<bullet>y" 

1201 
thus "x=y" by (simp add: pt_bij[OF pt, OF at]) 

1202 
qed 

1203 

1204 
lemma pt_set_finite_ineq: 

1205 
fixes X :: "'x set" 

1206 
and pi :: "'y prm" 

1207 
assumes pt: "pt TYPE('x) TYPE('y)" 

1208 
and at: "at TYPE('y)" 

1209 
shows "finite (pi\<bullet>X) = finite X" 

1210 
proof  

1211 
have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def) 

1212 
show ?thesis 

1213 
proof (rule iffI) 

1214 
assume "finite (pi\<bullet>X)" 

1215 
hence "finite (perm pi ` X)" using image by (simp) 

1216 
thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD) 

1217 
next 

1218 
assume "finite X" 

1219 
hence "finite (perm pi ` X)" by (rule finite_imageI) 

1220 
thus "finite (pi\<bullet>X)" using image by (simp) 

1221 
qed 

1222 
qed 

1223 

1224 
lemma pt_set_infinite_ineq: 

1225 
fixes X :: "'x set" 

1226 
and pi :: "'y prm" 

1227 
assumes pt: "pt TYPE('x) TYPE('y)" 

1228 
and at: "at TYPE('y)" 

1229 
shows "infinite (pi\<bullet>X) = infinite X" 

1230 
using pt at by (simp add: pt_set_finite_ineq) 

1231 

1232 
lemma pt_perm_supp_ineq: 

1233 
fixes pi :: "'x prm" 

1234 
and x :: "'a" 

1235 
assumes pta: "pt TYPE('a) TYPE('x)" 

1236 
and ptb: "pt TYPE('y) TYPE('x)" 

1237 
and at: "at TYPE('x)" 

1238 
and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 

1239 
shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS") 

1240 
proof  

1241 
have "?LHS = {pi\<bullet>a  a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def) 

1242 
also have "\<dots> = {pi\<bullet>a  a. infinite {pi\<bullet>b  b. [(a,b)]\<bullet>x \<noteq> x}}" 

1243 
proof (rule Collect_permI, rule allI, rule iffI) 

1244 
fix a 

1245 
assume "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}" 

1246 
hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at]) 

1247 
thus "infinite {pi\<bullet>b b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_def) 

1248 
next 

1249 
fix a 

1250 
assume "infinite {pi\<bullet>b b::'y. [(a,b)]\<bullet>x \<noteq> x}" 

1251 
hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def) 

1252 
thus "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}" 

1253 
by (simp add: pt_set_infinite_ineq[OF ptb, OF at]) 

1254 
qed 

1255 
also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 

1256 
by (simp add: pt_set_eq_ineq[OF ptb, OF at]) 

1257 
also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}" 

1258 
by (simp add: pt_bij[OF pta, OF at]) 

1259 
also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}" 

1260 
proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong) 

1261 
fix a::"'y" and b::"'y" 

1262 
have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)" 

1263 
by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at]) 

1264 
thus "(pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> pi\<bullet>x) = ([(a,b)]\<bullet>(pi\<bullet>x) \<noteq> pi\<bullet>x)" by simp 

1265 
qed 

1266 
finally show "?LHS = ?RHS" by (simp add: supp_def) 

1267 
qed 

1268 

1269 
lemma pt_perm_supp: 

1270 
fixes pi :: "'x prm" 

1271 
and x :: "'a" 

1272 
assumes pt: "pt TYPE('a) TYPE('x)" 

1273 
and at: "at TYPE('x)" 

1274 
shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)" 

1275 
apply(rule pt_perm_supp_ineq) 

1276 
apply(rule pt) 

1277 
apply(rule at_pt_inst) 

1278 
apply(rule at)+ 

1279 
apply(rule cp_pt_inst) 

1280 
apply(rule pt) 

1281 
apply(rule at) 

1282 
done 

1283 

1284 
lemma pt_supp_finite_pi: 

1285 
fixes pi :: "'x prm" 

1286 
and x :: "'a" 

1287 
assumes pt: "pt TYPE('a) TYPE('x)" 

1288 
and at: "at TYPE('x)" 

1289 
and f: "finite ((supp x)::'x set)" 

1290 
shows "finite ((supp (pi\<bullet>x))::'x set)" 

1291 
apply(simp add: pt_perm_supp[OF pt, OF at, symmetric]) 

1292 
apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at]) 

1293 
apply(rule f) 

1294 
done 

1295 

1296 
lemma pt_fresh_left_ineq: 

1297 
fixes pi :: "'x prm" 

1298 
and x :: "'a" 

1299 
and a :: "'y" 

1300 
assumes pta: "pt TYPE('a) TYPE('x)" 

1301 
and ptb: "pt TYPE('y) TYPE('x)" 

1302 
and at: "at TYPE('x)" 

1303 
and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 

1304 
shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x" 

1305 
apply(simp add: fresh_def) 

1306 
apply(simp add: pt_set_bij1[OF ptb, OF at]) 

1307 
apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp]) 

1308 
done 

1309 

1310 
lemma pt_fresh_right_ineq: 

1311 
fixes pi :: "'x prm" 

1312 
and x :: "'a" 

1313 
and a :: "'y" 

1314 
assumes pta: "pt TYPE('a) TYPE('x)" 

1315 
and ptb: "pt TYPE('y) TYPE('x)" 

1316 
and at: "at TYPE('x)" 

1317 
and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 

1318 
shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)" 

1319 
apply(simp add: fresh_def) 

1320 
apply(simp add: pt_set_bij1[OF ptb, OF at]) 

1321 
apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp]) 

1322 
done 

1323 

1324 
lemma pt_fresh_bij_ineq: 

1325 
fixes pi :: "'x prm" 

1326 
and x :: "'a" 

1327 
and a :: "'y" 

1328 
assumes pta: "pt TYPE('a) TYPE('x)" 

1329 
and ptb: "pt TYPE('y) TYPE('x)" 

1330 
and at: "at TYPE('x)" 

1331 
and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 

1332 
shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x" 

1333 
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) 

1334 
apply(simp add: pt_rev_pi[OF ptb, OF at]) 

1335 
done 

1336 

1337 
lemma pt_fresh_left: 

1338 
fixes pi :: "'x prm" 

1339 
and x :: "'a" 

1340 
and a :: "'x" 

1341 
assumes pt: "pt TYPE('a) TYPE('x)" 

1342 
and at: "at TYPE('x)" 

1343 
shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x" 

1344 
apply(rule pt_fresh_left_ineq) 

1345 
apply(rule pt) 

1346 
apply(rule at_pt_inst) 

1347 
apply(rule at)+ 

1348 
apply(rule cp_pt_inst) 

1349 
apply(rule pt) 

1350 
apply(rule at) 

1351 
done 

1352 

1353 
lemma pt_fresh_right: 

1354 
fixes pi :: "'x prm" 

1355 
and x :: "'a" 

1356 
and a :: "'x" 

1357 
assumes pt: "pt TYPE('a) TYPE('x)" 

1358 
and at: "at TYPE('x)" 

1359 
shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)" 

1360 
apply(rule pt_fresh_right_ineq) 

1361 
apply(rule pt) 

1362 
apply(rule at_pt_inst) 

1363 
apply(rule at)+ 

1364 
apply(rule cp_pt_inst) 

1365 
apply(rule pt) 

1366 
apply(rule at) 

1367 
done 

1368 

1369 
lemma pt_fresh_bij: 

1370 
fixes pi :: "'x prm" 

1371 
and x :: "'a" 

1372 
and a :: "'x" 

1373 
assumes pt: "pt TYPE('a) TYPE('x)" 

1374 
and at: "at TYPE('x)" 

1375 
shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x" 

1376 
apply(rule pt_fresh_bij_ineq) 

1377 
apply(rule pt) 

1378 
apply(rule at_pt_inst) 

1379 
apply(rule at)+ 

1380 
apply(rule cp_pt_inst) 

1381 
apply(rule pt) 

1382 
apply(rule at) 

1383 
done 

1384 

1385 
lemma pt_fresh_bij1: 

1386 
fixes pi :: "'x prm" 

1387 
and x :: "'a" 

1388 
and a :: "'x" 

1389 
assumes pt: "pt TYPE('a) TYPE('x)" 

1390 
and at: "at TYPE('x)" 

1391 
and a: "a\<sharp>x" 

1392 
shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)" 

1393 
using a by (simp add: pt_fresh_bij[OF pt, OF at]) 

1394 

19566  1395 
lemma pt_fresh_bij2: 
1396 
fixes pi :: "'x prm" 

1397 
and x :: "'a" 

1398 
and a :: "'x" 

1399 
assumes pt: "pt TYPE('a) TYPE('x)" 

1400 
and at: "at TYPE('x)" 

1401 
and a: "(pi\<bullet>a)\<sharp>(pi\<bullet>x)" 

1402 
shows "a\<sharp>x" 

1403 
using a by (simp add: pt_fresh_bij[OF pt, OF at]) 

1404 

17870  1405 
lemma pt_perm_fresh1: 
1406 
fixes a :: "'x" 

1407 
and b :: "'x" 

1408 
and x :: "'a" 

1409 
assumes pt: "pt TYPE('a) TYPE('x)" 

1410 
and at: "at TYPE ('x)" 

1411 
and a1: "\<not>(a\<sharp>x)" 

1412 
and a2: "b\<sharp>x" 

1413 
shows "[(a,b)]\<bullet>x \<noteq> x" 

1414 
proof 

1415 
assume neg: "[(a,b)]\<bullet>x = x" 

1416 
from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 

1417 
from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 

1418 
from a1' a2' have a3: "a\<noteq>b" by force 

1419 
from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 

1420 
by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at]) 

19325  1421 
hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_calc[OF at]) 
17870  1422 
hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at]) 
1423 
with a2' neg show False by simp 

1424 
qed 

1425 

19638
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1426 
(* the next two lemmas are needed in the proof *) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1427 
(* of the structural induction principle *) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1428 
lemma pt_fresh_aux: 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1429 
fixes a::"'x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1430 
and b::"'x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1431 
and c::"'x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1432 
and x::"'a" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1433 
assumes pt: "pt TYPE('a) TYPE('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1434 
and at: "at TYPE ('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1435 
assumes a1: "c\<noteq>a" and a2: "a\<sharp>x" and a3: "c\<sharp>x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1436 
shows "c\<sharp>([(a,b)]\<bullet>x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1437 
using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at]) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1438 

4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1439 
lemma pt_fresh_aux_ineq: 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1440 
fixes pi::"'x prm" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1441 
and c::"'y" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1442 
and x::"'a" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1443 
assumes pta: "pt TYPE('a) TYPE('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1444 
and ptb: "pt TYPE('y) TYPE('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1445 
and at: "at TYPE('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1446 
and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1447 
and dj: "disjoint TYPE('y) TYPE('x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1448 
assumes a: "c\<sharp>x" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1449 
shows "c\<sharp>(pi\<bullet>x)" 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1450 
using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj]) 
4358b88a9d12
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents:
19634
diff
changeset

1451 

17870  1452 
 "three helper lemmas for the perm_fresh_freshlemma" 
1453 
lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV  {b. P b}" 

1454 
by (auto) 

1455 

c35381811d5c
Initial revision.
bergho 