author  narboux 
Tue, 24 Apr 2007 14:02:16 +0200  
changeset 22775  d08efe73b27f 
parent 22774  8c64803fae48 
child 22785  fab155c8ce46 
permissions  rwrr 
17870  1 
(* $Id$ *) 
2 

19494  3 
theory Nominal 
20809  4 
imports Main Infinite_Set 
18068  5 
uses 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22231
diff
changeset

6 
("nominal_thmdecls.ML") 
18068  7 
("nominal_atoms.ML") 
8 
("nominal_package.ML") 

18264  9 
("nominal_induct.ML") 
18068  10 
("nominal_permeq.ML") 
22762  11 
("nominal_fresh_fun.ML") 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
21405
diff
changeset

12 
("nominal_primrec.ML") 
22312  13 
("nominal_inductive.ML") 
17870  14 
begin 
15 

16 
section {* Permutations *} 

17 
(*======================*) 

18 

19 
types 

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

21 

19477  22 
(* polymorphic operations for permutation and swapping *) 
17870  23 
consts 
18491  24 
perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) 
17870  25 
swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" 
26 

19477  27 
(* for the decision procedure involving permutations *) 
28 
(* (to make the permcomposition to be terminating *) 

29 
constdefs 

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

31 

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

33 
defs (unchecked overloaded) 
17870  34 
perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a  a. a\<in>X}" 
35 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

36 
lemma empty_eqvt: 
18656  37 
shows "pi\<bullet>{} = {}" 
38 
by (simp add: perm_set_def) 

39 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

40 
lemma union_eqvt: 
18264  41 
shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)" 
42 
by (auto simp add: perm_set_def) 

43 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

44 
lemma insert_eqvt: 
18656  45 
shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)" 
46 
by (auto simp add: perm_set_def) 

47 

17870  48 
(* permutation on units and products *) 
19687  49 
primrec (unchecked perm_unit) 
50 
"pi\<bullet>() = ()" 

51 

52 
primrec (unchecked perm_prod) 

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

17870  54 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

55 
lemma fst_eqvt: 
17870  56 
"pi\<bullet>(fst x) = fst (pi\<bullet>x)" 
19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

57 
by (cases x) simp 
17870  58 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

59 
lemma snd_eqvt: 
17870  60 
"pi\<bullet>(snd x) = snd (pi\<bullet>x)" 
19634
c78cf8981c5d
defs (unchecked overloaded), including former primrec;
wenzelm
parents:
19566
diff
changeset

61 
by (cases x) simp 
17870  62 

63 
(* permutation on lists *) 

19687  64 
primrec (unchecked perm_list) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

65 
nil_eqvt: "pi\<bullet>[] = []" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

66 
cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

67 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

68 
lemma append_eqvt: 
17870  69 
fixes pi :: "'x prm" 
70 
and l1 :: "'a list" 

71 
and l2 :: "'a list" 

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

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

73 
by (induct l1) auto 
17870  74 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

75 
lemma rev_eqvt: 
17870  76 
fixes pi :: "'x prm" 
77 
and l :: "'a list" 

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

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

79 
by (induct l) (simp_all add: append_eqvt) 
17870  80 

22768
d41fe3416f52
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
urbanc
parents:
22762
diff
changeset

81 
lemma set_eqvt: 
d41fe3416f52
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
urbanc
parents:
22762
diff
changeset

82 
fixes pi :: "'x prm" 
d41fe3416f52
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
urbanc
parents:
22762
diff
changeset

83 
and xs :: "'a list" 
d41fe3416f52
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
urbanc
parents:
22762
diff
changeset

84 
shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)" 
d41fe3416f52
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
urbanc
parents:
22762
diff
changeset

85 
by (induct xs, auto simp add: empty_eqvt insert_eqvt) 
d41fe3416f52
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
urbanc
parents:
22762
diff
changeset

86 

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

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

91 
(* permutation on bools *) 

19687  92 
primrec (unchecked perm_bool) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

93 
true_eqvt: "pi\<bullet>True = True" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

94 
false_eqvt: "pi\<bullet>False = False" 
17870  95 

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

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

98 
by (cases b) auto 
18264  99 

19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

100 
lemma perm_boolI: 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

101 
assumes a: "P" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

102 
shows "pi\<bullet>P" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

103 
using a by (simp add: perm_bool) 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

104 

89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

105 
lemma perm_boolE: 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

106 
assumes a: "pi\<bullet>P" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

107 
shows "P" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

108 
using a by (simp add: perm_bool) 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

109 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

110 
lemma if_eqvt: 
21010
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

111 
fixes pi::"'a prm" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

112 
shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

113 
apply(simp add: perm_fun_def) 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

114 
done 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

115 

22514  116 
lemma imp_eqvt: 
117 
shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))" 

118 
by (simp add: perm_bool) 

119 

120 
lemma conj_eqvt: 

121 
shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))" 

122 
by (simp add: perm_bool) 

123 

124 
lemma disj_eqvt: 

125 
shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))" 

126 
by (simp add: perm_bool) 

127 

128 
lemma neg_eqvt: 

129 
shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))" 

130 
by (simp add: perm_bool) 

131 

17870  132 
(* permutation on options *) 
21010
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

133 

19687  134 
primrec (unchecked perm_option) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

135 
some_eqvt: "pi\<bullet>Some(x) = Some(pi\<bullet>x)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

136 
none_eqvt: "pi\<bullet>None = None" 
17870  137 

138 
(* 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

139 
datatype 'a noption = nSome 'a  nNone 
17870  140 

19687  141 
primrec (unchecked perm_noption) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

142 
nSome_eqvt: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

143 
nNone_eqvt: "pi\<bullet>nNone = nNone" 
18600  144 

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

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

147 

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

17870  150 

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

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

152 
defs (unchecked overloaded) 
17870  153 
perm_char_def: "pi\<bullet>(s::char) \<equiv> s" 
154 

155 
(* permutation on ints *) 

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

156 
defs (unchecked overloaded) 
17870  157 
perm_int_def: "pi\<bullet>(i::int) \<equiv> i" 
158 

159 
(* permutation on nats *) 

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

160 
defs (unchecked overloaded) 
17870  161 
perm_nat_def: "pi\<bullet>(i::nat) \<equiv> i" 
162 

163 
section {* permutation equality *} 

164 
(*==============================*) 

165 

166 
constdefs 

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

167 
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

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

170 
section {* Support, Freshness and Supports*} 

171 
(*========================================*) 

172 
constdefs 

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

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

175 

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

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

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

181 

182 
lemma supp_fresh_iff: 

183 
fixes x :: "'a" 

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

185 
apply(simp add: fresh_def) 

186 
done 

187 

188 
lemma supp_unit: 

189 
shows "supp () = {}" 

190 
by (simp add: supp_def) 

191 

18264  192 
lemma supp_set_empty: 
193 
shows "supp {} = {}" 

194 
by (force simp add: supp_def perm_set_def) 

195 

196 
lemma supp_singleton: 

197 
shows "supp {x} = supp x" 

198 
by (force simp add: supp_def perm_set_def) 

199 

17870  200 
lemma supp_prod: 
201 
fixes x :: "'a" 

202 
and y :: "'b" 

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

204 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

205 

18600  206 
lemma supp_nprod: 
207 
fixes x :: "'a" 

208 
and y :: "'b" 

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

210 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

211 

17870  212 
lemma supp_list_nil: 
213 
shows "supp [] = {}" 

214 
apply(simp add: supp_def) 

215 
done 

216 

217 
lemma supp_list_cons: 

218 
fixes x :: "'a" 

219 
and xs :: "'a list" 

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

221 
apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq) 

222 
done 

223 

224 
lemma supp_list_append: 

225 
fixes xs :: "'a list" 

226 
and ys :: "'a list" 

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

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

229 

230 
lemma supp_list_rev: 

231 
fixes xs :: "'a list" 

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

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

234 

235 
lemma supp_bool: 

236 
fixes x :: "bool" 

237 
shows "supp (x) = {}" 

238 
apply(case_tac "x") 

239 
apply(simp_all add: supp_def) 

240 
done 

241 

242 
lemma supp_some: 

243 
fixes x :: "'a" 

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

245 
apply(simp add: supp_def) 

246 
done 

247 

248 
lemma supp_none: 

249 
fixes x :: "'a" 

250 
shows "supp (None) = {}" 

251 
apply(simp add: supp_def) 

252 
done 

253 

254 
lemma supp_int: 

255 
fixes i::"int" 

256 
shows "supp (i) = {}" 

257 
apply(simp add: supp_def perm_int_def) 

258 
done 

259 

20388  260 
lemma supp_nat: 
261 
fixes n::"nat" 

262 
shows "supp (n) = {}" 

263 
apply(simp add: supp_def perm_nat_def) 

264 
done 

265 

18627  266 
lemma supp_char: 
267 
fixes c::"char" 

268 
shows "supp (c) = {}" 

269 
apply(simp add: supp_def perm_char_def) 

270 
done 

271 

272 
lemma supp_string: 

273 
fixes s::"string" 

274 
shows "supp (s) = {}" 

275 
apply(induct s) 

276 
apply(auto simp add: supp_char supp_list_nil supp_list_cons) 

277 
done 

278 

18264  279 
lemma fresh_set_empty: 
280 
shows "a\<sharp>{}" 

281 
by (simp add: fresh_def supp_set_empty) 

282 

18578  283 
lemma fresh_singleton: 
284 
shows "a\<sharp>{x} = a\<sharp>x" 

285 
by (simp add: fresh_def supp_singleton) 

286 

19858  287 
lemma fresh_unit: 
288 
shows "a\<sharp>()" 

289 
by (simp add: fresh_def supp_unit) 

290 

17870  291 
lemma fresh_prod: 
292 
fixes a :: "'x" 

293 
and x :: "'a" 

294 
and y :: "'b" 

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

296 
by (simp add: fresh_def supp_prod) 

297 

298 
lemma fresh_list_nil: 

299 
fixes a :: "'x" 

18264  300 
shows "a\<sharp>[]" 
17870  301 
by (simp add: fresh_def supp_list_nil) 
302 

303 
lemma fresh_list_cons: 

304 
fixes a :: "'x" 

305 
and x :: "'a" 

306 
and xs :: "'a list" 

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

308 
by (simp add: fresh_def supp_list_cons) 

309 

310 
lemma fresh_list_append: 

311 
fixes a :: "'x" 

312 
and xs :: "'a list" 

313 
and ys :: "'a list" 

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

315 
by (simp add: fresh_def supp_list_append) 

316 

317 
lemma fresh_list_rev: 

318 
fixes a :: "'x" 

319 
and xs :: "'a list" 

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

321 
by (simp add: fresh_def supp_list_rev) 

322 

323 
lemma fresh_none: 

324 
fixes a :: "'x" 

325 
shows "a\<sharp>None" 

326 
apply(simp add: fresh_def supp_none) 

327 
done 

328 

329 
lemma fresh_some: 

330 
fixes a :: "'x" 

331 
and x :: "'a" 

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

333 
apply(simp add: fresh_def supp_some) 

334 
done 

335 

21010
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

336 
lemma fresh_int: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

337 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

338 
and i :: "int" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

339 
shows "a\<sharp>i" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

340 
apply(simp add: fresh_def supp_int) 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

341 
done 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

342 

7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

343 
lemma fresh_nat: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

344 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

345 
and n :: "nat" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

346 
shows "a\<sharp>n" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

347 
apply(simp add: fresh_def supp_nat) 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

348 
done 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

349 

7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

350 
lemma fresh_char: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

351 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

352 
and c :: "char" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

353 
shows "a\<sharp>c" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

354 
apply(simp add: fresh_def supp_char) 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

355 
done 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

356 

7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

357 
lemma fresh_string: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

358 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

359 
and s :: "string" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

360 
shows "a\<sharp>s" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

361 
apply(simp add: fresh_def supp_string) 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

362 
done 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

363 

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

364 
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

365 

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

366 
lemma fresh_unit_elim: 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

367 
shows "(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

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

369 

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

370 
lemma fresh_prod_elim: 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

371 
shows "(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

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

373 

21405
26b51f724fe6
added an intro lemma for freshness of products; set up
urbanc
parents:
21377
diff
changeset

374 
(* this rule needs to be added before the fresh_prodD is *) 
26b51f724fe6
added an intro lemma for freshness of products; set up
urbanc
parents:
21377
diff
changeset

375 
(* added to the simplifier with mksimps *) 
26b51f724fe6
added an intro lemma for freshness of products; set up
urbanc
parents:
21377
diff
changeset

376 
lemma [simp]: 
26b51f724fe6
added an intro lemma for freshness of products; set up
urbanc
parents:
21377
diff
changeset

377 
shows "a\<sharp>x1 \<Longrightarrow> a\<sharp>x2 \<Longrightarrow> a\<sharp>(x1,x2)" 
26b51f724fe6
added an intro lemma for freshness of products; set up
urbanc
parents:
21377
diff
changeset

378 
by (simp add: fresh_prod) 
26b51f724fe6
added an intro lemma for freshness of products; set up
urbanc
parents:
21377
diff
changeset

379 

21318
edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

380 
lemma fresh_prodD: 
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

381 
shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x" 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

382 
and "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y" 
21318
edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

383 
by (simp_all add: fresh_prod) 
edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

384 

edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

385 
ML_setup {* 
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

386 
val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD")::mksimps_pairs; 
21318
edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

387 
change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs)); 
edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

388 
*} 
edb595802d22
added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents:
21010
diff
changeset

389 

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

390 

17870  391 
section {* Abstract Properties for Permutations and Atoms *} 
392 
(*=========================================================*) 

393 

394 
(* properties for being a permutation type *) 

395 
constdefs 

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

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

398 
(\<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

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

401 
(* properties for being an atom type *) 

402 
constdefs 

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

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

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

406 
(\<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> 

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

408 

409 
(* property of two atomtypes being disjoint *) 

410 
constdefs 

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

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

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

414 

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

416 
constdefs 

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

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

419 

420 
(* property of having finite support *) 

421 
constdefs 

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

423 

424 
section {* Lemmas about the atomtype properties*} 

425 
(*==============================================*) 

426 

427 
lemma at1: 

428 
fixes x::"'x" 

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

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

431 
using a by (simp add: at_def) 

432 

433 
lemma at2: 

434 
fixes a ::"'x" 

435 
and b ::"'x" 

436 
and x ::"'x" 

437 
and pi::"'x prm" 

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

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

440 
using a by (simp only: at_def) 

441 

442 
lemma at3: 

443 
fixes a ::"'x" 

444 
and b ::"'x" 

445 
and c ::"'x" 

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

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

448 
using a by (simp only: at_def) 

449 

450 
(* rules to calculate simple premutations *) 

451 
lemmas at_calc = at2 at1 at3 

452 

22610  453 
lemma at_swap_simps: 
454 
fixes a ::"'x" 

455 
and b ::"'x" 

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

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

458 
and "[(a,b)]\<bullet>b = a" 

459 
using a by (simp_all add: at_calc) 

460 

17870  461 
lemma at4: 
462 
assumes a: "at TYPE('x)" 

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

464 
using a by (simp add: at_def) 

465 

466 
lemma at_append: 

467 
fixes pi1 :: "'x prm" 

468 
and pi2 :: "'x prm" 

469 
and c :: "'x" 

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

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

472 
proof (induct pi1) 

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

474 
next 

475 
case (Cons x xs) 

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

476 
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

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

478 
ultimately show ?case by (cases "x", simp add: at2[OF at]) 
17870  479 
qed 
480 

481 
lemma at_swap: 

482 
fixes a :: "'x" 

483 
and b :: "'x" 

484 
and c :: "'x" 

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

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

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

488 

489 
lemma at_rev_pi: 

490 
fixes pi :: "'x prm" 

491 
and c :: "'x" 

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

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

494 
proof(induct pi) 

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

496 
next 

497 
case (Cons x xs) thus ?case 

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

499 
qed 

500 

501 
lemma at_pi_rev: 

502 
fixes pi :: "'x prm" 

503 
and x :: "'x" 

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

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

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

507 

508 
lemma at_bij1: 

509 
fixes pi :: "'x prm" 

510 
and x :: "'x" 

511 
and y :: "'x" 

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

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

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

515 
proof  

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

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

518 
qed 

519 

520 
lemma at_bij2: 

521 
fixes pi :: "'x prm" 

522 
and x :: "'x" 

523 
and y :: "'x" 

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

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

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

527 
proof  

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

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

530 
qed 

531 

532 
lemma at_bij: 

533 
fixes pi :: "'x prm" 

534 
and x :: "'x" 

535 
and y :: "'x" 

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

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

538 
proof 

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

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

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

542 
next 

543 
assume "x=y" 

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

545 
qed 

546 

547 
lemma at_supp: 

548 
fixes x :: "'x" 

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

550 
shows "supp x = {x}" 

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

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

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

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

555 
from f a1 a2 show False by force 

556 
qed 

557 

558 
lemma at_fresh: 

559 
fixes a :: "'x" 

560 
and b :: "'x" 

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

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

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

564 

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

565 
lemma at_prm_fresh: 
17870  566 
fixes c :: "'x" 
567 
and pi:: "'x prm" 

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

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

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

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

571 
using a 
17870  572 
apply(induct pi) 
573 
apply(simp add: at1[OF at]) 

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

575 
done 

576 

577 
lemma at_prm_rev_eq: 

578 
fixes pi1 :: "'x prm" 

579 
and pi2 :: "'x prm" 

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

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

581 
shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)" 
17870  582 
proof (simp add: prm_eq_def, auto) 
583 
fix x 

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

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

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

587 
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

588 
thus "pi1\<bullet>x = pi2\<bullet>x" by simp 
17870  589 
next 
590 
fix x 

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

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

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

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

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

596 
qed 

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

597 

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

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

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

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

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

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

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

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

605 
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

606 

19325  607 
lemma at_prm_eq_append': 
608 
fixes pi1 :: "'x prm" 

609 
and pi2 :: "'x prm" 

610 
and pi3 :: "'x prm" 

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

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

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

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

615 

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

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

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

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

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

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

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

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

623 
using a1 a2 by (auto simp add: prm_eq_def) 
17870  624 

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

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

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

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

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

629 

17870  630 
lemma at_prm_rev_eq1: 
631 
fixes pi1 :: "'x prm" 

632 
and pi2 :: "'x prm" 

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

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

634 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)" 
17870  635 
by (simp add: at_prm_rev_eq[OF at]) 
636 

22774
8c64803fae48
adds op in front of an infix to fix SML compilation
narboux
parents:
22768
diff
changeset

637 

17870  638 
lemma at_ds1: 
639 
fixes a :: "'x" 

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

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

641 
shows "[(a,a)] \<triangleq> []" 
17870  642 
by (force simp add: prm_eq_def at_calc[OF at]) 
643 

644 
lemma at_ds2: 

645 
fixes pi :: "'x prm" 

646 
and a :: "'x" 

647 
and b :: "'x" 

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

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

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

652 

653 
lemma at_ds3: 

654 
fixes a :: "'x" 

655 
and b :: "'x" 

656 
and c :: "'x" 

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

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

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

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

662 
lemma at_ds4: 

663 
fixes a :: "'x" 

664 
and b :: "'x" 

665 
and pi :: "'x prm" 

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

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

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

670 

671 
lemma at_ds5: 

672 
fixes a :: "'x" 

673 
and b :: "'x" 

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

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

675 
shows "[(a,b)] \<triangleq> [(b,a)]" 
17870  676 
by (force simp add: prm_eq_def at_calc[OF at]) 
677 

19164  678 
lemma at_ds5': 
679 
fixes a :: "'x" 

680 
and b :: "'x" 

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

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

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

684 

17870  685 
lemma at_ds6: 
686 
fixes a :: "'x" 

687 
and b :: "'x" 

688 
and c :: "'x" 

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

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

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

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

694 
lemma at_ds7: 

695 
fixes pi :: "'x prm" 

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

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

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

700 
lemma at_ds8_aux: 

701 
fixes pi :: "'x prm" 

702 
and a :: "'x" 

703 
and b :: "'x" 

704 
and c :: "'x" 

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

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

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

708 

709 
lemma at_ds8: 

710 
fixes pi1 :: "'x prm" 

711 
and pi2 :: "'x prm" 

712 
and a :: "'x" 

713 
and b :: "'x" 

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

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

715 
shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)" 
17870  716 
apply(induct_tac pi2) 
717 
apply(simp add: prm_eq_def) 

718 
apply(auto simp add: prm_eq_def) 

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

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

721 
apply(drule sym) 

722 
apply(simp) 

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

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

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

726 
done 

727 

728 
lemma at_ds9: 

729 
fixes pi1 :: "'x prm" 

730 
and pi2 :: "'x prm" 

731 
and a :: "'x" 

732 
and b :: "'x" 

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

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

734 
shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" 
17870  735 
apply(induct_tac pi2) 
736 
apply(simp add: prm_eq_def) 

737 
apply(auto simp add: prm_eq_def) 

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

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

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

741 
apply(drule sym) 

742 
apply(simp) 

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

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

745 
done 

746 

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

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

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

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

751 
assumes at: "at TYPE('x)" 
19132  752 
and a: "b\<sharp>(rev pi)" 
753 
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

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

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

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

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

758 
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

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

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

761 

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

762 
"there always exists an atom that is not being in a finite set" 
17870  763 
lemma ex_in_inf: 
764 
fixes A::"'x set" 

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

766 
and fs: "finite A" 

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

767 
obtains c::"'x" where "c\<notin>A" 
17870  768 
proof  
769 
from fs at4[OF at] have "infinite ((UNIV::'x set)  A)" 

770 
by (simp add: Diff_infinite_finite) 

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

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

772 
then obtain c::"'x" where "c\<in>((UNIV::'x set)  A)" by force 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

773 
then have "c\<notin>A" by simp 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

774 
then show ?thesis using prems by simp 
17870  775 
qed 
776 

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

777 
text {* there always exists a fresh name for an object with finite support *} 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

778 
lemma at_exists_fresh': 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

779 
fixes x :: "'a" 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

780 
assumes at: "at TYPE('x)" 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

781 
and fs: "finite ((supp x)::'x set)" 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

782 
shows "\<exists>c::'x. c\<sharp>x" 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

783 
by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs]) 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

784 

17870  785 
lemma at_exists_fresh: 
786 
fixes x :: "'a" 

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

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

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

789 
obtains c::"'x" where "c\<sharp>x" 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

790 
by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def) 
17870  791 

21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

792 
lemma at_finite_select: 
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

793 
shows "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S" 
18657  794 
apply (drule Diff_infinite_finite) 
795 
apply (simp add: at_def) 

796 
apply blast 

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

798 
apply (simp only: ex_in_conv [symmetric]) 

799 
apply blast 

800 
apply (rule notI) 

801 
apply simp 

802 
done 

803 

19140  804 
lemma at_different: 
19132  805 
assumes at: "at TYPE('x)" 
19140  806 
shows "\<exists>(b::'x). a\<noteq>b" 
19132  807 
proof  
19140  808 
have "infinite (UNIV::'x set)" by (rule at4[OF at]) 
809 
hence inf2: "infinite (UNIV{a})" by (rule infinite_remove) 

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

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

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

19869  814 
then show "False" by auto 
19132  815 
qed 
816 
hence "\<exists>(b::'x). b\<in>(UNIV{a})" by blast 

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

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

19132  820 
qed 
821 

17870  822 
"the atprops imply the ptprops" 
823 
lemma at_pt_inst: 

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

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

826 
apply(auto simp only: pt_def) 

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

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

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

829 
apply(simp only: prm_eq_def) 
17870  830 
done 
831 

832 
section {* finite support properties *} 

833 
(*===================================*) 

834 

835 
lemma fs1: 

836 
fixes x :: "'a" 

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

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

839 
using a by (simp add: fs_def) 

840 

841 
lemma fs_at_inst: 

842 
fixes a :: "'x" 

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

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

845 
apply(simp add: fs_def) 

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

847 
done 

848 

849 
lemma fs_unit_inst: 

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

851 
apply(simp add: fs_def) 

852 
apply(simp add: supp_unit) 

853 
done 

854 

855 
lemma fs_prod_inst: 

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

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

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

859 
apply(unfold fs_def) 

860 
apply(auto simp add: supp_prod) 

861 
apply(rule fs1[OF fsa]) 

862 
apply(rule fs1[OF fsb]) 

863 
done 

864 

18600  865 
lemma fs_nprod_inst: 
866 
assumes fsa: "fs TYPE('a) TYPE('x)" 

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

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

869 
apply(unfold fs_def, rule allI) 

870 
apply(case_tac x) 

871 
apply(auto simp add: supp_nprod) 

872 
apply(rule fs1[OF fsa]) 

873 
apply(rule fs1[OF fsb]) 

874 
done 

875 

17870  876 
lemma fs_list_inst: 
877 
assumes fs: "fs TYPE('a) TYPE('x)" 

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

879 
apply(simp add: fs_def, rule allI) 

880 
apply(induct_tac x) 

881 
apply(simp add: supp_list_nil) 

882 
apply(simp add: supp_list_cons) 

883 
apply(rule fs1[OF fs]) 

884 
done 

885 

18431  886 
lemma fs_option_inst: 
887 
assumes fs: "fs TYPE('a) TYPE('x)" 

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

17870  889 
apply(simp add: fs_def, rule allI) 
18431  890 
apply(case_tac x) 
891 
apply(simp add: supp_none) 

892 
apply(simp add: supp_some) 

893 
apply(rule fs1[OF fs]) 

17870  894 
done 
895 

896 
section {* Lemmas about the permutation properties *} 

897 
(*=================================================*) 

898 

899 
lemma pt1: 

900 
fixes x::"'a" 

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

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

903 
using a by (simp add: pt_def) 

904 

905 
lemma pt2: 

906 
fixes pi1::"'x prm" 

907 
and pi2::"'x prm" 

908 
and x ::"'a" 

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

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

911 
using a by (simp add: pt_def) 

912 

913 
lemma pt3: 

914 
fixes pi1::"'x prm" 

915 
and pi2::"'x prm" 

916 
and x ::"'a" 

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

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

918 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x" 
17870  919 
using a by (simp add: pt_def) 
920 

921 
lemma pt3_rev: 

922 
fixes pi1::"'x prm" 

923 
and pi2::"'x prm" 

924 
and x ::"'a" 

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

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

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

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

930 
section {* composition properties *} 

931 
(* ============================== *) 

932 
lemma cp1: 

933 
fixes pi1::"'x prm" 

934 
and pi2::"'y prm" 

935 
and x ::"'a" 

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

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

938 
using cp by (simp add: cp_def) 

939 

940 
lemma cp_pt_inst: 

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

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

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

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

945 
apply(rule pt3[OF pt]) 

946 
apply(rule at_ds8[OF at]) 

947 
done 

948 

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

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

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

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

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

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

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

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

956 
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

957 

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

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

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

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

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

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

963 
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

964 

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

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

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

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

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

969 
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

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

971 
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

972 
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

973 

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

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

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

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

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

978 
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

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

980 

19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

981 
lemma at_fresh_ineq: 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

982 
fixes a :: "'x" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

983 
and b :: "'y" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

984 
assumes dj: "disjoint TYPE('y) TYPE('x)" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

985 
shows "a\<sharp>b" 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

986 
by (simp add: fresh_def dj_supp[OF dj]) 
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19869
diff
changeset

987 

17870  988 
section {* permutation type instances *} 
989 
(* ===================================*) 

990 

991 
lemma pt_set_inst: 

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

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

994 
apply(simp add: pt_def) 

995 
apply(simp_all add: perm_set_def) 

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

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

998 
done 

999 

1000 
lemma pt_list_nil: 

1001 
fixes xs :: "'a list" 

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

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

1004 
apply(induct_tac xs) 

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

1006 
done 

1007 

1008 
lemma pt_list_append: 

1009 
fixes pi1 :: "'x prm" 

1010 
and pi2 :: "'x prm" 

1011 
and xs :: "'a list" 

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

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

1014 
apply(induct_tac xs) 

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

1016 
done 

1017 

1018 
lemma pt_list_prm_eq: 

1019 
fixes pi1 :: "'x prm" 

1020 
and pi2 :: "'x prm" 

1021 
and xs :: "'a list" 

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

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

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

1026 
done 

1027 

1028 
lemma pt_list_inst: 

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

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

1031 
apply(auto simp only: pt_def) 

1032 
apply(rule pt_list_nil[OF pt]) 

1033 
apply(rule pt_list_append[OF pt]) 

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

1035 
done 

1036 

1037 
lemma pt_unit_inst: 

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

1039 
by (simp add: pt_def) 

1040 

1041 
lemma pt_prod_inst: 

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

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

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

1045 
apply(auto simp add: pt_def) 

1046 
apply(rule pt1[OF pta]) 

1047 
apply(rule pt1[OF ptb]) 

1048 
apply(rule pt2[OF pta]) 

1049 
apply(rule pt2[OF ptb]) 

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

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

1052 
done 

1053 

18600  1054 
lemma pt_nprod_inst: 
1055 
assumes pta: "pt TYPE('a) TYPE('x)" 

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

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

1058 
apply(auto simp add: pt_def) 

1059 
apply(case_tac x) 

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

1061 
apply(case_tac x) 

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

1063 
apply(case_tac x) 

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

1065 
done 

1066 

17870  1067 
lemma pt_fun_inst: 
1068 
assumes pta: "pt TYPE('a) TYPE('x)" 

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

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

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

1072 
apply(auto simp only: pt_def) 

1073 
apply(simp_all add: perm_fun_def) 

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

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

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

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

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

1080 
done 

1081 

1082 
lemma pt_option_inst: 

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

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

1085 
apply(auto simp only: pt_def) 

1086 
apply(case_tac "x") 

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

1088 
apply(case_tac "x") 

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

1090 
apply(case_tac "x") 

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

1092 
done 

1093 

1094 
lemma pt_noption_inst: 

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

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

1096 
shows "pt TYPE('a noption) TYPE('x)" 
17870  1097 
apply(auto simp only: pt_def) 
1098 
apply(case_tac "x") 

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

1100 
apply(case_tac "x") 

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

1102 
apply(case_tac "x") 

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

1104 
done 

1105 

1106 
section {* further lemmas for permutation types *} 

1107 
(*==============================================*) 

1108 

1109 
lemma pt_rev_pi: 

1110 
fixes pi :: "'x prm" 

1111 
and x :: "'a" 

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

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

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

1115 
proof  

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

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

1119 
qed 

1120 

1121 
lemma pt_pi_rev: 

1122 
fixes pi :: "'x prm" 

1123 
and x :: "'a" 

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

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

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

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

1128 

1129 
lemma pt_bij1: 

1130 
fixes pi :: "'x prm" 

1131 
and x :: "'a" 

1132 
and y :: "'a" 

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

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

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

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

1137 
proof  

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

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

1140 
qed 

1141 

1142 
lemma pt_bij2: 

1143 
fixes pi :: "'x prm" 

1144 
and x :: "'a" 

1145 
and y :: "'a" 

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

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

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

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

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

1151 

1152 
lemma pt_bij: 

1153 
fixes pi :: "'x prm" 

1154 
and x :: "'a" 

1155 
and y :: "'a" 

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

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

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

1159 
proof 

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

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

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

1163 
next 

1164 
assume "x=y" 

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

1166 
qed 

1167 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1168 
lemma pt_eq_eqvt: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1169 
fixes pi :: "'x prm" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1170 
and x :: "'a" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1171 
and y :: "'a" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1172 
assumes pt: "pt TYPE('a) TYPE('x)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1173 
and at: "at TYPE('x)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1174 
shows "pi \<bullet> (x=y) = (pi\<bullet>x = pi\<bullet>y)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1175 
using assms 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1176 
by (auto simp add: pt_bij perm_bool) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1177 

17870  1178 
lemma pt_bij3: 
1179 
fixes pi :: "'x prm" 

1180 
and x :: "'a" 

1181 
and y :: "'a" 

1182 
assumes a: "x=y" 

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

1184 
using a by simp 

1185 

1186 
lemma pt_bij4: 

1187 
fixes pi :: "'x prm" 

1188 
and x :: "'a" 

1189 
and y :: "'a" 

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

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

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

1193 
shows "x = y" 

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

1195 

1196 
lemma pt_swap_bij: 

1197 
fixes a :: "'x" 

1198 
and b :: "'x" 

1199 
and x :: "'a" 

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

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

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

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

1204 

19164  1205 
lemma pt_swap_bij': 
1206 
fixes a :: "'x" 

1207 
and b :: "'x" 

1208 
and x :: "'a" 

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

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

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

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

1213 
apply(rule trans) 

1214 
apply(rule pt3[OF pt]) 

1215 
apply(rule at_ds5'[OF at]) 

1216 
apply(rule pt1[OF pt]) 

1217 
done 

1218 

17870  1219 
lemma pt_set_bij1: 
1220 
fixes pi :: "'x prm" 

1221 
and x :: "'a" 

1222 
and X :: "'a set" 

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

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

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

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

1227 

1228 
lemma pt_set_bij1a: 

1229 
fixes pi :: "'x prm" 

1230 
and x :: "'a" 

1231 
and X :: "'a set" 

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

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

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

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

1236 

1237 
lemma pt_set_bij: 

1238 
fixes pi :: "'x prm" 

1239 
and x :: "'a" 

1240 
and X :: "'a set" 

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

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

1243 
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

1244 
by (simp add: perm_set_def pt_bij[OF pt, OF at]) 
17870  1245 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1246 
lemma pt_in_eqvt: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1247 
fixes pi :: "'x prm" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1248 
and x :: "'a" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1249 
and X :: "'a set" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1250 
assumes pt: "pt TYPE('a) TYPE('x)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1251 
and at: "at TYPE('x)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1252 
shows "pi\<bullet>(x\<in>X)=((pi\<bullet>x)\<in>(pi\<bullet>X))" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1253 
using assms 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1254 
by (auto simp add: pt_set_bij perm_bool) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22326
diff
changeset

1255 

17870  1256 
lemma pt_set_bij2: 
1257 
fixes pi :: "'x prm" 

1258 
and x :: "'a" 

1259 
and X :: "'a set" 

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

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

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

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

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

1265 

18264  1266 
lemma pt_set_bij2a: 
1267 
fixes pi :: "'x prm" 

1268 
and x :: "'a" 

1269 
and X :: "'a set" 

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

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

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

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

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

1275 

17870  1276 
lemma pt_set_bij3: 
1277 
fixes pi :: "'x prm" 

1278 
and x :: "'a" 

1279 
and X :: "'a set" 

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

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

1282 
apply(auto) 

1283 
done 

1284 

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

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

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

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

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

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

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

1291 
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

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

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

1294 
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

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

1296 
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

1297 
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

1298 
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

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

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

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

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

1303 
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

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

1305 

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

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

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

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

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

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

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

1312 
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

1313 
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

1314 

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

1315 

17870  1316 
 "some helper lemmas for the pt_perm_supp_ineq lemma" 
1317 
lemma Collect_permI: 

1318 
fixes pi :: "'x prm" 

1319 
and x :: "'a" 

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

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

1322 
using a by force 

1323 

1324 
lemma Infinite_cong: 

1325 
assumes a: "X = Y" 

1326 
shows "infinite X = infinite Y" 

1327 
using a by (simp) 

1328 

1329 
lemma pt_set_eq_ineq: 

1330 
fixes pi :: "'y prm" 

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

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

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

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

1335 

1336 
lemma pt_inject_on_ineq: 

1337 
fixes X :: "'y set" 

1338 
and pi :: "'x prm" 

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

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

1341 
shows "inj_on (perm pi) X" 

1342 
proof (unfold inj_on_def, intro strip) 

1343 
fix x::"'y" and y::"'y" 

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

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

1346 
qed 

1347 

1348 
lemma pt_set_finite_ineq: 

1349 
fixes X :: "'x set" 

1350 
and pi :: "'y prm" 

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

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

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

1354 
proof  

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

1356 
show ?thesis 

1357 
proof (rule iffI) 

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

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

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

1361 
next 

1362 
assume "finite X" 

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

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

1365 
qed 

1366 
qed 

1367 

1368 
lemma pt_set_infinite_ineq: 

1369 
fixes X :: "'x set" 

1370 
and pi :: "'y prm" 

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

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

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

1374 
using pt at by (simp add: pt_set_finite_ineq) 

1375 

1376 
lemma pt_perm_supp_ineq: 

1377 
fixes pi :: "'x prm" 

1378 
and x :: "'a" 

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

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

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

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

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

1384 
proof  

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

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

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

1388 
fix a 

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

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

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

1392 
next 

1393 
fix a 

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

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

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

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

1398 
qed 

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

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

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

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

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

1404 
proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong) 

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

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

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

1408 
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 

1409 
qed 

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

1411 
qed 

1412 

1413 
lemma pt_perm_supp: 

1414 
fixes pi :: "'x prm" 

1415 
and x :: "'a" 

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

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

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

1419 
apply(rule pt_perm_supp_ineq) 

1420 
apply(rule pt) 

1421 
apply(rule at_pt_inst) 

1422 
apply(rule at)+ 

1423 
apply(rule cp_pt_inst) 

1424 
apply(rule pt) 

1425 
apply(rule at) 

1426 
done 

1427 

1428 
lemma pt_supp_finite_pi: 

1429 
fi 