1 theory Abs_res |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
|
3 begin |
|
4 |
|
5 fun |
|
6 alpha_gen |
|
7 where |
|
8 alpha_gen[simp del]: |
|
9 "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y" |
|
10 |
|
11 notation |
|
12 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
|
13 |
|
14 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
|
15 by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps) |
|
16 |
|
17 lemma alpha_gen_refl: |
|
18 assumes a: "R x x" |
|
19 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
|
20 using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm) |
|
21 |
|
22 lemma alpha_gen_sym: |
|
23 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
|
24 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
|
25 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
|
26 using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
|
27 |
|
28 lemma alpha_gen_trans: |
|
29 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
|
30 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
|
31 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
|
32 shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)" |
|
33 using a b c using supp_plus_perm |
|
34 apply(simp add: alpha_gen fresh_star_def fresh_def) |
|
35 apply(blast) |
|
36 done |
|
37 |
|
38 lemma alpha_gen_eqvt: |
|
39 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
|
40 and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
|
41 and c: "p \<bullet> (f x) = f (p \<bullet> x)" |
|
42 and d: "p \<bullet> (f y) = f (p \<bullet> y)" |
|
43 shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
|
44 using a b |
|
45 apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric]) |
|
46 apply(simp add: permute_eqvt[symmetric]) |
|
47 apply(simp add: fresh_star_permute_iff) |
|
48 apply(clarsimp) |
|
49 done |
|
50 |
|
51 lemma alpha_gen_compose_sym: |
|
52 fixes pi |
|
53 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
54 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
55 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
|
56 using b apply - |
|
57 apply(simp add: alpha_gen.simps) |
|
58 apply(erule conjE)+ |
|
59 apply(rule conjI) |
|
60 apply(simp add: fresh_star_def fresh_minus_perm) |
|
61 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
62 apply simp |
|
63 apply(rule a) |
|
64 apply assumption |
|
65 done |
|
66 |
|
67 lemma alpha_gen_compose_trans: |
|
68 fixes pi pia |
|
69 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
70 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
|
71 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
72 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
|
73 using b c apply - |
|
74 apply(simp add: alpha_gen.simps) |
|
75 apply(erule conjE)+ |
|
76 apply(simp add: fresh_star_plus) |
|
77 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
78 apply(drule mp) |
|
79 apply(rotate_tac 4) |
|
80 apply(drule_tac pi="- pia" in a) |
|
81 apply(simp) |
|
82 apply(rotate_tac 6) |
|
83 apply(drule_tac pi="pia" in a) |
|
84 apply(simp) |
|
85 done |
|
86 |
|
87 lemma alpha_gen_compose_eqvt: |
|
88 fixes pia |
|
89 assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)" |
|
90 and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)" |
|
91 and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
|
92 shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)" |
|
93 using b |
|
94 apply - |
|
95 apply(simp add: alpha_gen.simps) |
|
96 apply(erule conjE)+ |
|
97 apply(rule conjI) |
|
98 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
99 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
|
100 apply(rule conjI) |
|
101 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
102 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
|
103 apply(subst permute_eqvt[symmetric]) |
|
104 apply(simp) |
|
105 done |
|
106 |
|
107 fun |
|
108 alpha_abs |
|
109 where |
|
110 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
|
111 |
|
112 notation |
|
113 alpha_abs ("_ \<approx>abs _") |
|
114 |
|
115 lemma alpha_abs_swap: |
|
116 assumes a1: "a \<notin> (supp x) - bs" |
|
117 and a2: "b \<notin> (supp x) - bs" |
|
118 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
|
119 apply(simp) |
|
120 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
121 apply(simp add: alpha_gen) |
|
122 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
123 apply(simp add: swap_set_not_in[OF a1 a2]) |
|
124 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
125 using a1 a2 |
|
126 apply(simp add: fresh_star_def fresh_def) |
|
127 apply(blast) |
|
128 apply(simp add: supp_swap) |
|
129 done |
|
130 |
|
131 lemma alpha_gen_swap_fun: |
|
132 assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)" |
|
133 assumes a1: "a \<notin> (f x) - bs" |
|
134 and a2: "b \<notin> (f x) - bs" |
|
135 shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
|
136 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
137 apply(simp add: alpha_gen) |
|
138 apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
139 apply(simp add: swap_set_not_in[OF a1 a2]) |
|
140 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
141 using a1 a2 |
|
142 apply(simp add: fresh_star_def fresh_def) |
|
143 apply(blast) |
|
144 apply(simp add: supp_swap) |
|
145 done |
|
146 |
|
147 |
|
148 fun |
|
149 supp_abs_fun |
|
150 where |
|
151 "supp_abs_fun (bs, x) = (supp x) - bs" |
|
152 |
|
153 lemma supp_abs_fun_lemma: |
|
154 assumes a: "x \<approx>abs y" |
|
155 shows "supp_abs_fun x = supp_abs_fun y" |
|
156 using a |
|
157 apply(induct rule: alpha_abs.induct) |
|
158 apply(simp add: alpha_gen) |
|
159 done |
|
160 |
|
161 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
|
162 apply(rule equivpI) |
|
163 unfolding reflp_def symp_def transp_def |
|
164 apply(simp_all) |
|
165 (* refl *) |
|
166 apply(clarify) |
|
167 apply(rule exI) |
|
168 apply(rule alpha_gen_refl) |
|
169 apply(simp) |
|
170 (* symm *) |
|
171 apply(clarify) |
|
172 apply(rule exI) |
|
173 apply(rule alpha_gen_sym) |
|
174 apply(assumption) |
|
175 apply(clarsimp) |
|
176 (* trans *) |
|
177 apply(clarify) |
|
178 apply(rule exI) |
|
179 apply(rule alpha_gen_trans) |
|
180 apply(assumption) |
|
181 apply(assumption) |
|
182 apply(simp) |
|
183 done |
|
184 |
|
185 quotient_definition |
|
186 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
|
187 is |
|
188 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
|
189 |
|
190 lemma [quot_respect]: |
|
191 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
|
192 apply(clarsimp) |
|
193 apply(rule exI) |
|
194 apply(rule alpha_gen_refl) |
|
195 apply(simp) |
|
196 done |
|
197 |
|
198 lemma [quot_respect]: |
|
199 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
|
200 apply(clarsimp) |
|
201 apply(rule exI) |
|
202 apply(rule alpha_gen_eqvt) |
|
203 apply(assumption) |
|
204 apply(simp_all add: supp_eqvt) |
|
205 done |
|
206 |
|
207 lemma [quot_respect]: |
|
208 shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun" |
|
209 apply(simp add: supp_abs_fun_lemma) |
|
210 done |
|
211 |
|
212 lemma abs_induct: |
|
213 "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t" |
|
214 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) |
|
215 done |
|
216 |
|
217 (* TEST case *) |
|
218 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted] |
|
219 thm abs_induct abs_induct2 |
|
220 |
|
221 instantiation abs :: (pt) pt |
|
222 begin |
|
223 |
|
224 quotient_definition |
|
225 "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs" |
|
226 is |
|
227 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
|
228 |
|
229 lemma permute_ABS [simp]: |
|
230 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
|
231 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
|
232 by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) |
|
233 |
|
234 instance |
|
235 apply(default) |
|
236 apply(induct_tac [!] x rule: abs_induct) |
|
237 apply(simp_all) |
|
238 done |
|
239 |
|
240 end |
|
241 |
|
242 quotient_definition |
|
243 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
|
244 is |
|
245 "supp_abs_fun" |
|
246 |
|
247 lemma supp_Abs_fun_simp: |
|
248 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
|
249 by (lifting supp_abs_fun.simps(1)) |
|
250 |
|
251 lemma supp_Abs_fun_eqvt [eqvt]: |
|
252 shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)" |
|
253 apply(induct_tac x rule: abs_induct) |
|
254 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
|
255 done |
|
256 |
|
257 lemma supp_Abs_fun_fresh: |
|
258 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
|
259 apply(rule fresh_fun_eqvt_app) |
|
260 apply(simp add: eqvts_raw) |
|
261 apply(simp) |
|
262 done |
|
263 |
|
264 lemma Abs_swap: |
|
265 assumes a1: "a \<notin> (supp x) - bs" |
|
266 and a2: "b \<notin> (supp x) - bs" |
|
267 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
|
268 using a1 a2 by (lifting alpha_abs_swap) |
|
269 |
|
270 lemma Abs_supports: |
|
271 shows "((supp x) - as) supports (Abs as x)" |
|
272 unfolding supports_def |
|
273 apply(clarify) |
|
274 apply(simp (no_asm)) |
|
275 apply(subst Abs_swap[symmetric]) |
|
276 apply(simp_all) |
|
277 done |
|
278 |
|
279 lemma supp_Abs_subset1: |
|
280 fixes x::"'a::fs" |
|
281 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
|
282 apply(simp add: supp_conv_fresh) |
|
283 apply(auto) |
|
284 apply(drule_tac supp_Abs_fun_fresh) |
|
285 apply(simp only: supp_Abs_fun_simp) |
|
286 apply(simp add: fresh_def) |
|
287 apply(simp add: supp_finite_atom_set finite_supp) |
|
288 done |
|
289 |
|
290 lemma supp_Abs_subset2: |
|
291 fixes x::"'a::fs" |
|
292 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
|
293 apply(rule supp_is_subset) |
|
294 apply(rule Abs_supports) |
|
295 apply(simp add: finite_supp) |
|
296 done |
|
297 |
|
298 lemma supp_Abs: |
|
299 fixes x::"'a::fs" |
|
300 shows "supp (Abs as x) = (supp x) - as" |
|
301 apply(rule_tac subset_antisym) |
|
302 apply(rule supp_Abs_subset2) |
|
303 apply(rule supp_Abs_subset1) |
|
304 done |
|
305 |
|
306 instance abs :: (fs) fs |
|
307 apply(default) |
|
308 apply(induct_tac x rule: abs_induct) |
|
309 apply(simp add: supp_Abs) |
|
310 apply(simp add: finite_supp) |
|
311 done |
|
312 |
|
313 lemma Abs_fresh_iff: |
|
314 fixes x::"'a::fs" |
|
315 shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
|
316 apply(simp add: fresh_def) |
|
317 apply(simp add: supp_Abs) |
|
318 apply(auto) |
|
319 done |
|
320 |
|
321 lemma Abs_eq_iff: |
|
322 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
|
323 by (lifting alpha_abs.simps(1)) |
|
324 |
|
325 |
|
326 |
|
327 (* |
|
328 below is a construction site for showing that in the |
|
329 single-binder case, the old and new alpha equivalence |
|
330 coincide |
|
331 *) |
|
332 |
|
333 fun |
|
334 alpha1 |
|
335 where |
|
336 "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
|
337 |
|
338 notation |
|
339 alpha1 ("_ \<approx>abs1 _") |
|
340 |
|
341 fun |
|
342 alpha2 |
|
343 where |
|
344 "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))" |
|
345 |
|
346 notation |
|
347 alpha2 ("_ \<approx>abs2 _") |
|
348 |
|
349 lemma qq: |
|
350 fixes S::"atom set" |
|
351 assumes a: "supp p \<inter> S = {}" |
|
352 shows "p \<bullet> S = S" |
|
353 using a |
|
354 apply(simp add: supp_perm permute_set_eq) |
|
355 apply(auto) |
|
356 apply(simp only: disjoint_iff_not_equal) |
|
357 apply(simp) |
|
358 apply (metis permute_atom_def_raw) |
|
359 apply(rule_tac x="(- p) \<bullet> x" in exI) |
|
360 apply(simp) |
|
361 apply(simp only: disjoint_iff_not_equal) |
|
362 apply(simp) |
|
363 apply(metis permute_minus_cancel) |
|
364 done |
|
365 |
|
366 lemma alpha_old_new: |
|
367 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
|
368 shows "({a}, x) \<approx>abs ({b}, y)" |
|
369 using a |
|
370 apply(simp) |
|
371 apply(erule disjE) |
|
372 apply(simp) |
|
373 apply(rule exI) |
|
374 apply(rule alpha_gen_refl) |
|
375 apply(simp) |
|
376 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
377 apply(simp add: alpha_gen) |
|
378 apply(simp add: fresh_def) |
|
379 apply(rule conjI) |
|
380 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1]) |
|
381 apply(rule trans) |
|
382 apply(simp add: Diff_eqvt supp_eqvt) |
|
383 apply(subst swap_set_not_in) |
|
384 back |
|
385 apply(simp) |
|
386 apply(simp) |
|
387 apply(simp add: permute_set_eq) |
|
388 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
|
389 apply(simp add: permute_self) |
|
390 apply(simp add: Diff_eqvt supp_eqvt) |
|
391 apply(simp add: permute_set_eq) |
|
392 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
393 apply(simp add: fresh_star_def fresh_def) |
|
394 apply(blast) |
|
395 apply(simp add: supp_swap) |
|
396 done |
|
397 |
|
398 lemma perm_zero: |
|
399 assumes a: "\<forall>x::atom. p \<bullet> x = x" |
|
400 shows "p = 0" |
|
401 using a |
|
402 by (simp add: expand_perm_eq) |
|
403 |
|
404 fun |
|
405 add_perm |
|
406 where |
|
407 "add_perm [] = 0" |
|
408 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs" |
|
409 |
|
410 fun |
|
411 elem_perm |
|
412 where |
|
413 "elem_perm [] = {}" |
|
414 | "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs" |
|
415 |
|
416 |
|
417 lemma add_perm_apend: |
|
418 shows "add_perm (xs @ ys) = add_perm xs + add_perm ys" |
|
419 apply(induct xs arbitrary: ys) |
|
420 apply(auto simp add: add_assoc) |
|
421 done |
|
422 |
|
423 lemma perm_list_exists: |
|
424 fixes p::perm |
|
425 shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" |
|
426 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct) |
|
427 apply(rename_tac p) |
|
428 apply(case_tac "supp p = {}") |
|
429 apply(simp) |
|
430 apply(simp add: supp_perm) |
|
431 apply(drule perm_zero) |
|
432 apply(simp) |
|
433 apply(rule_tac x="[]" in exI) |
|
434 apply(simp add: supp_Nil) |
|
435 apply(subgoal_tac "\<exists>x. x \<in> supp p") |
|
436 defer |
|
437 apply(auto)[1] |
|
438 apply(erule exE) |
|
439 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec) |
|
440 apply(drule mp) |
|
441 defer |
|
442 apply(erule exE) |
|
443 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI) |
|
444 apply(simp add: add_perm_apend) |
|
445 apply(erule conjE) |
|
446 apply(drule sym) |
|
447 apply(simp) |
|
448 apply(simp add: expand_perm_eq) |
|
449 apply(simp add: supp_append) |
|
450 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom) |
|
451 apply(rule conjI) |
|
452 prefer 2 |
|
453 apply(auto)[1] |
|
454 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2)) |
|
455 defer |
|
456 apply(rule psubset_card_mono) |
|
457 apply(simp add: finite_supp) |
|
458 apply(rule psubsetI) |
|
459 defer |
|
460 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))") |
|
461 apply(blast) |
|
462 apply(simp add: supp_perm) |
|
463 defer |
|
464 apply(auto simp add: supp_perm)[1] |
|
465 apply(case_tac "x = xa") |
|
466 apply(simp) |
|
467 apply(case_tac "((- p) \<bullet> x) = xa") |
|
468 apply(simp) |
|
469 apply(case_tac "sort_of xa = sort_of x") |
|
470 apply(simp) |
|
471 apply(auto)[1] |
|
472 apply(simp) |
|
473 apply(simp) |
|
474 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}") |
|
475 apply(blast) |
|
476 apply(auto simp add: supp_perm)[1] |
|
477 apply(case_tac "x = xa") |
|
478 apply(simp) |
|
479 apply(case_tac "((- p) \<bullet> x) = xa") |
|
480 apply(simp) |
|
481 apply(case_tac "sort_of xa = sort_of x") |
|
482 apply(simp) |
|
483 apply(auto)[1] |
|
484 apply(simp) |
|
485 apply(simp) |
|
486 done |
|
487 |
|
488 lemma tt0: |
|
489 fixes p::perm |
|
490 shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x" |
|
491 apply(auto simp add: fresh_star_def supp_perm fresh_def) |
|
492 done |
|
493 |
|
494 lemma uu0: |
|
495 shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x" |
|
496 apply(induct xs rule: add_perm.induct) |
|
497 apply(simp) |
|
498 apply(simp add: swap_fresh_fresh) |
|
499 done |
|
500 |
|
501 lemma yy0: |
|
502 fixes xs::"(atom \<times> atom) list" |
|
503 shows "supp xs = elem_perm xs" |
|
504 apply(induct xs rule: elem_perm.induct) |
|
505 apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom) |
|
506 done |
|
507 |
|
508 lemma tt1: |
|
509 shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
|
510 apply(drule tt0) |
|
511 apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p") |
|
512 prefer 2 |
|
513 apply(rule perm_list_exists) |
|
514 apply(erule exE) |
|
515 apply(simp only: yy0) |
|
516 apply(rule uu0) |
|
517 apply(auto) |
|
518 done |
|
519 |
|
520 |
|
521 lemma perm_induct_test: |
|
522 fixes P :: "perm => bool" |
|
523 assumes fin: "finite (supp p)" |
|
524 assumes zero: "P 0" |
|
525 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
|
526 assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
|
527 shows "P p" |
|
528 using fin |
|
529 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct) |
|
530 apply(simp add: supp_perm) |
|
531 apply(drule perm_zero) |
|
532 apply(simp add: zero) |
|
533 apply(rotate_tac 3) |
|
534 oops |
|
535 lemma tt: |
|
536 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
|
537 oops |
|
538 |
|
539 lemma yy: |
|
540 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
|
541 shows "S1 = S2" |
|
542 using assms |
|
543 apply (metis insert_Diff_single insert_absorb) |
|
544 done |
|
545 |
|
546 lemma permute_boolI: |
|
547 fixes P::"bool" |
|
548 shows "p \<bullet> P \<Longrightarrow> P" |
|
549 apply(simp add: permute_bool_def) |
|
550 done |
|
551 |
|
552 lemma permute_boolE: |
|
553 fixes P::"bool" |
|
554 shows "P \<Longrightarrow> p \<bullet> P" |
|
555 apply(simp add: permute_bool_def) |
|
556 done |
|
557 |
|
558 lemma kk: |
|
559 assumes a: "p \<bullet> x = y" |
|
560 shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y" |
|
561 using a |
|
562 apply(auto) |
|
563 apply(rule_tac p="- p" in permute_boolI) |
|
564 apply(simp add: mem_eqvt supp_eqvt) |
|
565 done |
|
566 |
|
567 lemma ww: |
|
568 assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b" |
|
569 shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x" |
|
570 apply(subgoal_tac "(supp x) supports x") |
|
571 apply(simp add: supports_def) |
|
572 using assms |
|
573 apply - |
|
574 apply(drule_tac x="a" in spec) |
|
575 defer |
|
576 apply(rule supp_supports) |
|
577 apply(auto) |
|
578 apply(rotate_tac 1) |
|
579 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE) |
|
580 apply(simp add: mem_eqvt supp_eqvt) |
|
581 done |
|
582 |
|
583 lemma alpha_abs_sym: |
|
584 assumes a: "({a}, x) \<approx>abs ({b}, y)" |
|
585 shows "({b}, y) \<approx>abs ({a}, x)" |
|
586 using a |
|
587 apply(simp) |
|
588 apply(erule exE) |
|
589 apply(rule_tac x="- p" in exI) |
|
590 apply(simp add: alpha_gen) |
|
591 apply(simp add: fresh_star_def fresh_minus_perm) |
|
592 apply (metis permute_minus_cancel(2)) |
|
593 done |
|
594 |
|
595 lemma alpha_abs_trans: |
|
596 assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)" |
|
597 assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)" |
|
598 shows "({a1}, x1) \<approx>abs ({a3}, x3)" |
|
599 using a b |
|
600 apply(simp) |
|
601 apply(erule exE)+ |
|
602 apply(rule_tac x="pa + p" in exI) |
|
603 apply(simp add: alpha_gen) |
|
604 apply(simp add: fresh_star_def fresh_plus_perm) |
|
605 done |
|
606 |
|
607 lemma alpha_equal: |
|
608 assumes a: "({a}, x) \<approx>abs ({a}, y)" |
|
609 shows "(a, x) \<approx>abs1 (a, y)" |
|
610 using a |
|
611 apply(simp) |
|
612 apply(erule exE) |
|
613 apply(simp add: alpha_gen) |
|
614 apply(erule conjE)+ |
|
615 apply(case_tac "a \<notin> supp x") |
|
616 apply(simp) |
|
617 apply(subgoal_tac "supp x \<sharp>* p") |
|
618 apply(drule tt1) |
|
619 apply(simp) |
|
620 apply(simp) |
|
621 apply(simp) |
|
622 apply(case_tac "a \<notin> supp y") |
|
623 apply(simp) |
|
624 apply(drule tt1) |
|
625 apply(clarify) |
|
626 apply(simp (no_asm_use)) |
|
627 apply(simp) |
|
628 apply(simp) |
|
629 apply(drule yy) |
|
630 apply(simp) |
|
631 apply(simp) |
|
632 apply(simp) |
|
633 apply(case_tac "a \<sharp> p") |
|
634 apply(subgoal_tac "supp y \<sharp>* p") |
|
635 apply(drule tt1) |
|
636 apply(clarify) |
|
637 apply(simp (no_asm_use)) |
|
638 apply(metis) |
|
639 apply(auto simp add: fresh_star_def)[1] |
|
640 apply(frule_tac kk) |
|
641 apply(drule_tac x="a" in bspec) |
|
642 apply(simp) |
|
643 apply(simp add: fresh_def) |
|
644 apply(simp add: supp_perm) |
|
645 apply(subgoal_tac "((p \<bullet> a) \<sharp> p)") |
|
646 apply(simp add: fresh_def supp_perm) |
|
647 apply(simp add: fresh_star_def) |
|
648 done |
|
649 |
|
650 lemma alpha_unequal: |
|
651 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b" |
|
652 shows "(a, x) \<approx>abs1 (b, y)" |
|
653 using a |
|
654 apply - |
|
655 apply(subgoal_tac "a \<notin> supp x - {a}") |
|
656 apply(subgoal_tac "b \<notin> supp x - {a}") |
|
657 defer |
|
658 apply(simp add: alpha_gen) |
|
659 apply(simp) |
|
660 apply(drule_tac alpha_abs_swap) |
|
661 apply(assumption) |
|
662 apply(simp only: insert_eqvt empty_eqvt swap_atom_simps) |
|
663 apply(drule alpha_abs_sym) |
|
664 apply(rotate_tac 4) |
|
665 apply(drule_tac alpha_abs_trans) |
|
666 apply(assumption) |
|
667 apply(drule alpha_equal) |
|
668 apply(simp) |
|
669 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI) |
|
670 apply(simp add: fresh_eqvt) |
|
671 apply(simp add: fresh_def) |
|
672 done |
|
673 |
|
674 lemma alpha_new_old: |
|
675 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
|
676 shows "(a, x) \<approx>abs1 (b, y)" |
|
677 using a |
|
678 apply(case_tac "a=b") |
|
679 apply(simp only: alpha_equal) |
|
680 apply(drule alpha_unequal) |
|
681 apply(simp) |
|
682 apply(simp) |
|
683 apply(simp) |
|
684 done |
|
685 |
|
686 fun |
|
687 distinct_perms |
|
688 where |
|
689 "distinct_perms [] = True" |
|
690 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
|
691 |
|
692 (* support of concrete atom sets *) |
|
693 |
|
694 lemma atom_eqvt_raw: |
|
695 fixes p::"perm" |
|
696 shows "(p \<bullet> atom) = atom" |
|
697 by (simp add: expand_fun_eq permute_fun_def atom_eqvt) |
|
698 |
|
699 lemma atom_image_cong: |
|
700 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
701 apply(rule inj_image_eq_iff) |
|
702 apply(simp add: inj_on_def) |
|
703 done |
|
704 |
|
705 lemma supp_atom_image: |
|
706 fixes as::"'a::at_base set" |
|
707 shows "supp (atom ` as) = supp as" |
|
708 apply(simp add: supp_def) |
|
709 apply(simp add: image_eqvt) |
|
710 apply(simp add: atom_eqvt_raw) |
|
711 apply(simp add: atom_image_cong) |
|
712 done |
|
713 |
|
714 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
|
715 apply (simp add: fresh_def) |
|
716 apply (simp add: supp_atom_image) |
|
717 apply (fold fresh_def) |
|
718 apply (simp add: swap_fresh_fresh) |
|
719 done |
|
720 |
|
721 |
|
722 end |
|
723 |
|