author  berghofe 
Thu, 13 Sep 2007 18:06:50 +0200  
changeset 24568  9a4cce088aec 
parent 24544  da7de38392df 
child 24571  a6d0428dea8e 
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 

24544  27 
(* an auxiliary constant for the decision procedure involving *) 
28 
(* permutations (to avoid loops when using permcomposition) *) 

19477  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) 
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

34 
perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>x  x. x\<in>X}" 
17870  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) 

22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

53 
"pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)" 
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) 
23050  153 
perm_char_def: "pi\<bullet>(c::char) \<equiv> c" 
154 

155 
lemma perm_string: 

156 
fixes s::"string" 

157 
shows "pi\<bullet>s = s" 

158 
by (induct s)(auto simp add: perm_char_def) 

17870  159 

160 
(* permutation on ints *) 

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

161 
defs (unchecked overloaded) 
17870  162 
perm_int_def: "pi\<bullet>(i::int) \<equiv> i" 
163 

164 
(* permutation on nats *) 

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

165 
defs (unchecked overloaded) 
17870  166 
perm_nat_def: "pi\<bullet>(i::nat) \<equiv> i" 
167 

168 
section {* permutation equality *} 

169 
(*==============================*) 

170 

171 
constdefs 

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

172 
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

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

175 
section {* Support, Freshness and Supports*} 

176 
(*========================================*) 

177 
constdefs 

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

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

180 

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

22808  184 
supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) 
17870  185 
"S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)" 
186 

187 
lemma supp_fresh_iff: 

188 
fixes x :: "'a" 

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

190 
apply(simp add: fresh_def) 

191 
done 

192 

193 
lemma supp_unit: 

194 
shows "supp () = {}" 

195 
by (simp add: supp_def) 

196 

18264  197 
lemma supp_set_empty: 
198 
shows "supp {} = {}" 

199 
by (force simp add: supp_def perm_set_def) 

200 

201 
lemma supp_singleton: 

202 
shows "supp {x} = supp x" 

203 
by (force simp add: supp_def perm_set_def) 

204 

17870  205 
lemma supp_prod: 
206 
fixes x :: "'a" 

207 
and y :: "'b" 

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

209 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

210 

18600  211 
lemma supp_nprod: 
212 
fixes x :: "'a" 

213 
and y :: "'b" 

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

215 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

216 

17870  217 
lemma supp_list_nil: 
218 
shows "supp [] = {}" 

219 
apply(simp add: supp_def) 

220 
done 

221 

222 
lemma supp_list_cons: 

223 
fixes x :: "'a" 

224 
and xs :: "'a list" 

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

226 
apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq) 

227 
done 

228 

229 
lemma supp_list_append: 

230 
fixes xs :: "'a list" 

231 
and ys :: "'a list" 

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

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

234 

235 
lemma supp_list_rev: 

236 
fixes xs :: "'a list" 

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

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

239 

240 
lemma supp_bool: 

241 
fixes x :: "bool" 

242 
shows "supp (x) = {}" 

243 
apply(case_tac "x") 

244 
apply(simp_all add: supp_def) 

245 
done 

246 

247 
lemma supp_some: 

248 
fixes x :: "'a" 

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

250 
apply(simp add: supp_def) 

251 
done 

252 

253 
lemma supp_none: 

254 
fixes x :: "'a" 

255 
shows "supp (None) = {}" 

256 
apply(simp add: supp_def) 

257 
done 

258 

259 
lemma supp_int: 

260 
fixes i::"int" 

261 
shows "supp (i) = {}" 

262 
apply(simp add: supp_def perm_int_def) 

263 
done 

264 

20388  265 
lemma supp_nat: 
266 
fixes n::"nat" 

267 
shows "supp (n) = {}" 

268 
apply(simp add: supp_def perm_nat_def) 

269 
done 

270 

18627  271 
lemma supp_char: 
272 
fixes c::"char" 

273 
shows "supp (c) = {}" 

274 
apply(simp add: supp_def perm_char_def) 

275 
done 

276 

277 
lemma supp_string: 

278 
fixes s::"string" 

279 
shows "supp (s) = {}" 

23050  280 
apply(simp add: supp_def perm_string) 
18627  281 
done 
282 

18264  283 
lemma fresh_set_empty: 
284 
shows "a\<sharp>{}" 

285 
by (simp add: fresh_def supp_set_empty) 

286 

18578  287 
lemma fresh_singleton: 
288 
shows "a\<sharp>{x} = a\<sharp>x" 

289 
by (simp add: fresh_def supp_singleton) 

290 

19858  291 
lemma fresh_unit: 
292 
shows "a\<sharp>()" 

293 
by (simp add: fresh_def supp_unit) 

294 

17870  295 
lemma fresh_prod: 
296 
fixes a :: "'x" 

297 
and x :: "'a" 

298 
and y :: "'b" 

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

300 
by (simp add: fresh_def supp_prod) 

301 

302 
lemma fresh_list_nil: 

303 
fixes a :: "'x" 

18264  304 
shows "a\<sharp>[]" 
17870  305 
by (simp add: fresh_def supp_list_nil) 
306 

307 
lemma fresh_list_cons: 

308 
fixes a :: "'x" 

309 
and x :: "'a" 

310 
and xs :: "'a list" 

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

312 
by (simp add: fresh_def supp_list_cons) 

313 

314 
lemma fresh_list_append: 

315 
fixes a :: "'x" 

316 
and xs :: "'a list" 

317 
and ys :: "'a list" 

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

319 
by (simp add: fresh_def supp_list_append) 

320 

321 
lemma fresh_list_rev: 

322 
fixes a :: "'x" 

323 
and xs :: "'a list" 

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

325 
by (simp add: fresh_def supp_list_rev) 

326 

327 
lemma fresh_none: 

328 
fixes a :: "'x" 

329 
shows "a\<sharp>None" 

22831
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

330 
by (simp add: fresh_def supp_none) 
17870  331 

332 
lemma fresh_some: 

333 
fixes a :: "'x" 

334 
and x :: "'a" 

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

22831
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

336 
by (simp add: fresh_def supp_some) 
17870  337 

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

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

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

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

341 
shows "a\<sharp>i" 
22831
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

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

343 

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

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

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

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

347 
shows "a\<sharp>n" 
22831
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

348 
by (simp add: fresh_def supp_nat) 
21010
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" 
22831
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

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

355 

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

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

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

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

359 
shows "a\<sharp>s" 
22831
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

360 
by (simp add: fresh_def supp_string) 
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

361 

18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

362 
lemma fresh_bool: 
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

363 
fixes a :: "'x" 
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

364 
and b :: "bool" 
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

365 
shows "a\<sharp>b" 
18f4014e1259
tuned some of the proofs and added the lemma fresh_bool
urbanc
parents:
22829
diff
changeset

366 
by (simp add: fresh_def supp_bool) 
21010
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

367 

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

368 
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

369 

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

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

371 
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

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

373 

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

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

375 
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

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

377 

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

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

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

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

381 
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

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

383 

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

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

385 
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

386 
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

387 
by (simp_all add: fresh_prod) 
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 
ML_setup {* 
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21318
diff
changeset

390 
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

391 
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

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

393 

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

394 

17870  395 
section {* Abstract Properties for Permutations and Atoms *} 
396 
(*=========================================================*) 

397 

398 
(* properties for being a permutation type *) 

399 
constdefs 

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

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

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

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

405 
(* properties for being an atom type *) 

406 
constdefs 

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

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

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

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

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

412 

413 
(* property of two atomtypes being disjoint *) 

414 
constdefs 

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

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

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

418 

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

420 
constdefs 

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

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

423 

424 
(* property of having finite support *) 

425 
constdefs 

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

427 

428 
section {* Lemmas about the atomtype properties*} 

429 
(*==============================================*) 

430 

431 
lemma at1: 

432 
fixes x::"'x" 

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

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

435 
using a by (simp add: at_def) 

436 

437 
lemma at2: 

438 
fixes a ::"'x" 

439 
and b ::"'x" 

440 
and x ::"'x" 

441 
and pi::"'x prm" 

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

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

444 
using a by (simp only: at_def) 

445 

446 
lemma at3: 

447 
fixes a ::"'x" 

448 
and b ::"'x" 

449 
and c ::"'x" 

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

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

452 
using a by (simp only: at_def) 

453 

454 
(* rules to calculate simple premutations *) 

455 
lemmas at_calc = at2 at1 at3 

456 

22610  457 
lemma at_swap_simps: 
458 
fixes a ::"'x" 

459 
and b ::"'x" 

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

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

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

463 
using a by (simp_all add: at_calc) 

464 

17870  465 
lemma at4: 
466 
assumes a: "at TYPE('x)" 

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

468 
using a by (simp add: at_def) 

469 

470 
lemma at_append: 

471 
fixes pi1 :: "'x prm" 

472 
and pi2 :: "'x prm" 

473 
and c :: "'x" 

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

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

476 
proof (induct pi1) 

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

478 
next 

479 
case (Cons x xs) 

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

480 
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

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

482 
ultimately show ?case by (cases "x", simp add: at2[OF at]) 
17870  483 
qed 
484 

485 
lemma at_swap: 

486 
fixes a :: "'x" 

487 
and b :: "'x" 

488 
and c :: "'x" 

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

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

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

492 

493 
lemma at_rev_pi: 

494 
fixes pi :: "'x prm" 

495 
and c :: "'x" 

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

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

498 
proof(induct pi) 

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

500 
next 

501 
case (Cons x xs) thus ?case 

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

503 
qed 

504 

505 
lemma at_pi_rev: 

506 
fixes pi :: "'x prm" 

507 
and x :: "'x" 

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

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

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

511 

512 
lemma at_bij1: 

513 
fixes pi :: "'x prm" 

514 
and x :: "'x" 

515 
and y :: "'x" 

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

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

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

519 
proof  

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

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

522 
qed 

523 

524 
lemma at_bij2: 

525 
fixes pi :: "'x prm" 

526 
and x :: "'x" 

527 
and y :: "'x" 

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

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

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

531 
proof  

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

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

534 
qed 

535 

536 
lemma at_bij: 

537 
fixes pi :: "'x prm" 

538 
and x :: "'x" 

539 
and y :: "'x" 

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

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

542 
proof 

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

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

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

546 
next 

547 
assume "x=y" 

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

549 
qed 

550 

551 
lemma at_supp: 

552 
fixes x :: "'x" 

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

554 
shows "supp x = {x}" 

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

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

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

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

559 
from f a1 a2 show False by force 

560 
qed 

561 

562 
lemma at_fresh: 

563 
fixes a :: "'x" 

564 
and b :: "'x" 

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

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

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

568 

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

569 
lemma at_prm_fresh: 
17870  570 
fixes c :: "'x" 
571 
and pi:: "'x prm" 

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

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

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

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

575 
using a 
17870  576 
apply(induct pi) 
577 
apply(simp add: at1[OF at]) 

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

579 
done 

580 

581 
lemma at_prm_rev_eq: 

582 
fixes pi1 :: "'x prm" 

583 
and pi2 :: "'x prm" 

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

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

585 
shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)" 
17870  586 
proof (simp add: prm_eq_def, auto) 
587 
fix x 

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

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

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

591 
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

592 
thus "pi1\<bullet>x = pi2\<bullet>x" by simp 
17870  593 
next 
594 
fix x 

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

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

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

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

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

600 
qed 

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

601 

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

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

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

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

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

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

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

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

609 
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

610 

19325  611 
lemma at_prm_eq_append': 
612 
fixes pi1 :: "'x prm" 

613 
and pi2 :: "'x prm" 

614 
and pi3 :: "'x prm" 

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

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

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

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

619 

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

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

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

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

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

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

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

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

627 
using a1 a2 by (auto simp add: prm_eq_def) 
17870  628 

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

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

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

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

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

633 

17870  634 
lemma at_prm_rev_eq1: 
635 
fixes pi1 :: "'x prm" 

636 
and pi2 :: "'x prm" 

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

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

638 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)" 
17870  639 
by (simp add: at_prm_rev_eq[OF at]) 
640 

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

641 

17870  642 
lemma at_ds1: 
643 
fixes a :: "'x" 

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

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

645 
shows "[(a,a)] \<triangleq> []" 
17870  646 
by (force simp add: prm_eq_def at_calc[OF at]) 
647 

648 
lemma at_ds2: 

649 
fixes pi :: "'x prm" 

650 
and a :: "'x" 

651 
and b :: "'x" 

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

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

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

656 

657 
lemma at_ds3: 

658 
fixes a :: "'x" 

659 
and b :: "'x" 

660 
and c :: "'x" 

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

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

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

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

666 
lemma at_ds4: 

667 
fixes a :: "'x" 

668 
and b :: "'x" 

669 
and pi :: "'x prm" 

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

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

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

674 

675 
lemma at_ds5: 

676 
fixes a :: "'x" 

677 
and b :: "'x" 

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

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

679 
shows "[(a,b)] \<triangleq> [(b,a)]" 
17870  680 
by (force simp add: prm_eq_def at_calc[OF at]) 
681 

19164  682 
lemma at_ds5': 
683 
fixes a :: "'x" 

684 
and b :: "'x" 

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

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

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

688 

17870  689 
lemma at_ds6: 
690 
fixes a :: "'x" 

691 
and b :: "'x" 

692 
and c :: "'x" 

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

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

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

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

698 
lemma at_ds7: 

699 
fixes pi :: "'x prm" 

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

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

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

704 
lemma at_ds8_aux: 

705 
fixes pi :: "'x prm" 

706 
and a :: "'x" 

707 
and b :: "'x" 

708 
and c :: "'x" 

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

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

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

712 

713 
lemma at_ds8: 

714 
fixes pi1 :: "'x prm" 

715 
and pi2 :: "'x prm" 

716 
and a :: "'x" 

717 
and b :: "'x" 

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

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

719 
shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)" 
17870  720 
apply(induct_tac pi2) 
721 
apply(simp add: prm_eq_def) 

722 
apply(auto simp add: prm_eq_def) 

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

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

725 
apply(drule sym) 

726 
apply(simp) 

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

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

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

730 
done 

731 

732 
lemma at_ds9: 

733 
fixes pi1 :: "'x prm" 

734 
and pi2 :: "'x prm" 

735 
and a :: "'x" 

736 
and b :: "'x" 

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

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

738 
shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" 
17870  739 
apply(induct_tac pi2) 
740 
apply(simp add: prm_eq_def) 

741 
apply(auto simp add: prm_eq_def) 

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

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

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

745 
apply(drule sym) 

746 
apply(simp) 

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

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

749 
done 

750 

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

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

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

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

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

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

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

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

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

762 
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

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

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

765 

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

766 
"there always exists an atom that is not being in a finite set" 
17870  767 
lemma ex_in_inf: 
768 
fixes A::"'x set" 

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

770 
and fs: "finite A" 

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

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

774 
by (simp add: Diff_infinite_finite) 

775 
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

776 
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

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

778 
then show ?thesis using prems by simp 
17870  779 
qed 
780 

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

781 
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

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

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

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

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

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

787 
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

788 

17870  789 
lemma at_exists_fresh: 
790 
fixes x :: "'a" 

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

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

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

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

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

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

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

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

800 
apply blast 

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

802 
apply (simp only: ex_in_conv [symmetric]) 

803 
apply blast 

804 
apply (rule notI) 

805 
apply simp 

806 
done 

807 

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

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

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

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

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

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

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

19132  824 
qed 
825 

17870  826 
"the atprops imply the ptprops" 
827 
lemma at_pt_inst: 

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

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

830 
apply(auto simp only: pt_def) 

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

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

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

833 
apply(simp only: prm_eq_def) 
17870  834 
done 
835 

836 
section {* finite support properties *} 

837 
(*===================================*) 

838 

839 
lemma fs1: 

840 
fixes x :: "'a" 

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

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

843 
using a by (simp add: fs_def) 

844 

845 
lemma fs_at_inst: 

846 
fixes a :: "'x" 

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

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

849 
apply(simp add: fs_def) 

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

851 
done 

852 

853 
lemma fs_unit_inst: 

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

855 
apply(simp add: fs_def) 

856 
apply(simp add: supp_unit) 

857 
done 

858 

859 
lemma fs_prod_inst: 

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

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

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

863 
apply(unfold fs_def) 

864 
apply(auto simp add: supp_prod) 

865 
apply(rule fs1[OF fsa]) 

866 
apply(rule fs1[OF fsb]) 

867 
done 

868 

18600  869 
lemma fs_nprod_inst: 
870 
assumes fsa: "fs TYPE('a) TYPE('x)" 

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

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

873 
apply(unfold fs_def, rule allI) 

874 
apply(case_tac x) 

875 
apply(auto simp add: supp_nprod) 

876 
apply(rule fs1[OF fsa]) 

877 
apply(rule fs1[OF fsb]) 

878 
done 

879 

17870  880 
lemma fs_list_inst: 
881 
assumes fs: "fs TYPE('a) TYPE('x)" 

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

883 
apply(simp add: fs_def, rule allI) 

884 
apply(induct_tac x) 

885 
apply(simp add: supp_list_nil) 

886 
apply(simp add: supp_list_cons) 

887 
apply(rule fs1[OF fs]) 

888 
done 

889 

18431  890 
lemma fs_option_inst: 
891 
assumes fs: "fs TYPE('a) TYPE('x)" 

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

17870  893 
apply(simp add: fs_def, rule allI) 
18431  894 
apply(case_tac x) 
895 
apply(simp add: supp_none) 

896 
apply(simp add: supp_some) 

897 
apply(rule fs1[OF fs]) 

17870  898 
done 
899 

900 
section {* Lemmas about the permutation properties *} 

901 
(*=================================================*) 

902 

903 
lemma pt1: 

904 
fixes x::"'a" 

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

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

907 
using a by (simp add: pt_def) 

908 

909 
lemma pt2: 

910 
fixes pi1::"'x prm" 

911 
and pi2::"'x prm" 

912 
and x ::"'a" 

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

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

915 
using a by (simp add: pt_def) 

916 

917 
lemma pt3: 

918 
fixes pi1::"'x prm" 

919 
and pi2::"'x prm" 

920 
and x ::"'a" 

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

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

922 
shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x" 
17870  923 
using a by (simp add: pt_def) 
924 

925 
lemma pt3_rev: 

926 
fixes pi1::"'x prm" 

927 
and pi2::"'x prm" 

928 
and x ::"'a" 

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

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

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

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

934 
section {* composition properties *} 

935 
(* ============================== *) 

936 
lemma cp1: 

937 
fixes pi1::"'x prm" 

938 
and pi2::"'y prm" 

939 
and x ::"'a" 

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

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

942 
using cp by (simp add: cp_def) 

943 

944 
lemma cp_pt_inst: 

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

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

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

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

949 
apply(rule pt3[OF pt]) 

950 
apply(rule at_ds8[OF at]) 

951 
done 

952 

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

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

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

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

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

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

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

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

960 
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

961 

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

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

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

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

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

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

967 
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

968 

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

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

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

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

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

973 
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

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

975 
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

976 
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

977 

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

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

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

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

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

982 
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

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

984 

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

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

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

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

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

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

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

991 

17870  992 
section {* permutation type instances *} 
993 
(* ===================================*) 

994 

995 
lemma pt_set_inst: 

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

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

998 
apply(simp add: pt_def) 

999 
apply(simp_all add: perm_set_def) 

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

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

1002 
done 

1003 

1004 
lemma pt_list_nil: 

1005 
fixes xs :: "'a list" 

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

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

1008 
apply(induct_tac xs) 

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

1010 
done 

1011 

1012 
lemma pt_list_append: 

1013 
fixes pi1 :: "'x prm" 

1014 
and pi2 :: "'x prm" 

1015 
and xs :: "'a list" 

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

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

1018 
apply(induct_tac xs) 

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

1020 
done 

1021 

1022 
lemma pt_list_prm_eq: 

1023 
fixes pi1 :: "'x prm" 

1024 
and pi2 :: "'x prm" 

1025 
and xs :: "'a list" 

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

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

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

1030 
done 

1031 

1032 
lemma pt_list_inst: 

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

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

1035 
apply(auto simp only: pt_def) 

1036 
apply(rule pt_list_nil[OF pt]) 

1037 
apply(rule pt_list_append[OF pt]) 

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

1039 
done 

1040 

1041 
lemma pt_unit_inst: 

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

1043 
by (simp add: pt_def) 

1044 

1045 
lemma pt_prod_inst: 

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

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

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

1049 
apply(auto simp add: pt_def) 

1050 
apply(rule pt1[OF pta]) 

1051 
apply(rule pt1[OF ptb]) 

1052 
apply(rule pt2[OF pta]) 

1053 
apply(rule pt2[OF ptb]) 

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

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

1056 
done 

1057 

18600  1058 
lemma pt_nprod_inst: 
1059 
assumes pta: "pt TYPE('a) TYPE('x)" 

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

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

1062 
apply(auto simp add: pt_def) 

1063 
apply(case_tac x) 

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

1065 
apply(case_tac x) 

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

1067 
apply(case_tac x) 

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

1069 
done 

1070 

17870  1071 
lemma pt_fun_inst: 
1072 
assumes pta: "pt TYPE('a) TYPE('x)" 

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

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

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

1076 
apply(auto simp only: pt_def) 

1077 
apply(simp_all add: perm_fun_def) 

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

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

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

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

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

1084 
done 

1085 

1086 
lemma pt_option_inst: 

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

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

1089 
apply(auto simp only: pt_def) 

1090 
apply(case_tac "x") 

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

1092 
apply(case_tac "x") 

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

1094 
apply(case_tac "x") 

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

1096 
done 

1097 

1098 
lemma pt_noption_inst: 

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

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

1100 
shows "pt TYPE('a noption) TYPE('x)" 
17870  1101 
apply(auto simp only: pt_def) 
1102 
apply(case_tac "x") 

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

1104 
apply(case_tac "x") 

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

1106 
apply(case_tac "x") 

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

1108 
done 

1109 

24544  1110 
lemma pt_bool_inst: 
1111 
shows "pt TYPE(bool) TYPE('x)" 

1112 
by (simp add: pt_def perm_bool) 

1113 

17870  1114 
section {* further lemmas for permutation types *} 
1115 
(*==============================================*) 

1116 

1117 
lemma pt_rev_pi: 

1118 
fixes pi :: "'x prm" 

1119 
and x :: "'a" 

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

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

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

1123 
proof  

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

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

1127 
qed 

1128 

1129 
lemma pt_pi_rev: 

1130 
fixes pi :: "'x prm" 

1131 
and x :: "'a" 

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

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

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

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

1136 

1137 
lemma pt_bij1: 

1138 
fixes pi :: "'x prm" 

1139 
and x :: "'a" 

1140 
and y :: "'a" 

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

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

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

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

1145 
proof  

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

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

1148 
qed 

1149 

1150 
lemma pt_bij2: 

1151 
fixes pi :: "'x prm" 

1152 
and x :: "'a" 

1153 
and y :: "'a" 

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

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

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

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

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

1159 

1160 
lemma pt_bij: 

1161 
fixes pi :: "'x prm" 

1162 
and x :: "'a" 

1163 
and y :: "'a" 

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

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

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

1167 
proof 

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

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

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

1171 
next 

1172 
assume "x=y" 

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

1174 
qed 

1175 

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

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

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

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

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

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

1181 
and at: "at TYPE('x)" 
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

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

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

1184 
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

1185 

17870  1186 
lemma pt_bij3: 
1187 
fixes pi :: "'x prm" 

1188 
and x :: "'a" 

1189 
and y :: "'a" 

1190 
assumes a: "x=y" 

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

1192 
using a by simp 

1193 

1194 
lemma pt_bij4: 

1195 
fixes pi :: "'x prm" 

1196 
and x :: "'a" 

1197 
and y :: "'a" 

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

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

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

1201 
shows "x = y" 

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

1203 

1204 
lemma pt_swap_bij: 

1205 
fixes a :: "'x" 

1206 
and b :: "'x" 

1207 
and x :: "'a" 

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

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

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

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

1212 

19164  1213 
lemma pt_swap_bij': 
1214 
fixes a :: "'x" 

1215 
and b :: "'x" 

1216 
and x :: "'a" 

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

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

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

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

1221 
apply(rule trans) 

1222 
apply(rule pt3[OF pt]) 

1223 
apply(rule at_ds5'[OF at]) 

1224 
apply(rule pt1[OF pt]) 

1225 
done 

1226 

17870  1227 
lemma pt_set_bij1: 
1228 
fixes pi :: "'x prm" 

1229 
and x :: "'a" 

1230 
and X :: "'a set" 

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

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

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

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

1235 

1236 
lemma pt_set_bij1a: 

1237 
fixes pi :: "'x prm" 

1238 
and x :: "'a" 

1239 
and X :: "'a set" 

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

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

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

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

1244 

1245 
lemma pt_set_bij: 

1246 
fixes pi :: "'x prm" 

1247 
and x :: "'a" 

1248 
and X :: "'a set" 

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

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

1251 
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

1252 
by (simp add: perm_set_def pt_bij[OF pt, OF at]) 
17870  1253 

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

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

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

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

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

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

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

1260 
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

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

1262 
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

1263 

17870  1264 
lemma pt_set_bij2: 
1265 
fixes pi :: "'x prm" 

1266 
and x :: "'a" 

1267 
and X :: "'a set" 

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

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

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

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

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

1273 

18264  1274 
lemma pt_set_bij2a: 
1275 
fixes pi :: "'x prm" 

1276 
and x :: "'a" 

1277 
and X :: "'a set" 

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

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

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

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

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

1283 

17870  1284 
lemma pt_set_bij3: 
1285 
fixes pi :: "'x prm" 

1286 
and x :: "'a" 

1287 
and X :: "'a set" 

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

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

1290 
apply(auto) 

1291 
done 

1292 

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

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

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

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

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

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

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

1299 
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

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

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

1302 
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

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

1304 
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

1305 
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

1306 
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

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

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

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

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

1311 
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

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

1313 

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

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

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

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

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

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

1319 
and at: "at TYPE('x)" 
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

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

1321 
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

1322 

22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1323 
lemma pt_Collect_eqvt: 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1324 
fixes pi::"'x prm" 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1325 
assumes pt: "pt TYPE('a) TYPE('x)" 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1326 
and at: "at TYPE('x)" 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1327 
shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}" 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1328 
apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at]) 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1329 
apply(rule_tac x="(rev pi)\<bullet>x" in exI) 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

1330 
apply(simp add: pt_pi_rev[OF pt, OF at]) 
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22808
diff
changeset

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

1332 

17870  1333 
 "some helper lemmas for the pt_perm_supp_ineq lemma" 
1334 
lemma Collect_permI: 

1335 
fixes pi :: "'x prm" 

1336 
and x :: "'a" 

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

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

1339 
using a by force 

1340 

1341 
lemma Infinite_cong: 

1342 
assumes a: "X = Y" 

1343 
shows "infinite X = infinite Y" 

1344 
using a by (simp) 

1345 

1346 
lemma pt_set_eq_ineq: 

1347 
fixes pi :: "'y prm" 

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

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

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

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

1352 

1353 
lemma pt_inject_on_ineq: 

1354 
fixes X :: "'y set" 

1355 
and pi :: "'x prm" 

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

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

1358 
shows "inj_on (perm pi) X" 

1359 
proof (unfold inj_on_def, intro strip) 

1360 
fix x::"'y" and y::"'y" 

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

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

1363 
qed 

1364 

1365 
lemma pt_set_finite_ineq: 

1366 
fixes X :: "'x set" 

1367 
and pi :: "'y prm" 

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

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

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

1371 
proof  

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

1373 
show ?thesis 

1374 
proof (rule iffI) 

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

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

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

1378 
next 

1379 
assume "finite X" 

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

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

1382 
qed 

1383 
qed 

1384 

1385 
lemma pt_set_infinite_ineq: 

1386 
fixes X :: "'x set" 

1387 
and pi :: "'y prm" 

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

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

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

1391 
using pt at by (simp add: pt_set_finite_ineq) 

1392 

1393 
lemma pt_perm_supp_ineq: 

1394 
fixes pi :: "'x prm" 

1395 
and x :: "'a" 

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

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

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

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

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

1401 
proof  

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

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

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

1405 
fix a 

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

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

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

1409 
next 

1410 
fix a 

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

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

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

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

1415 
qed 

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

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

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

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

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

1421 
proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong) 

