49 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
49 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
50 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
50 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
51 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
51 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
52 using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
52 using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
53 |
53 |
|
54 lemma alpha_gen_trans: |
|
55 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
|
56 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
|
57 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
|
58 shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)" |
|
59 using a b c using supp_plus_perm |
|
60 apply(simp add: alpha_gen fresh_star_def fresh_def) |
|
61 apply(blast) |
|
62 done |
|
63 |
|
64 lemma alpha_gen_eqvt: |
|
65 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
|
66 and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
|
67 and c: "p \<bullet> (f x) = f (p \<bullet> x)" |
|
68 and d: "p \<bullet> (f y) = f (p \<bullet> y)" |
|
69 shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
|
70 using a b |
|
71 apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric]) |
|
72 apply(simp add: permute_eqvt[symmetric]) |
|
73 apply(simp add: fresh_star_permute_iff) |
|
74 apply(clarsimp) |
|
75 done |
|
76 |
|
77 (* introduced for examples *) |
54 lemma alpha_gen_atom_sym: |
78 lemma alpha_gen_atom_sym: |
55 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
79 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
56 shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow> |
80 shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow> |
57 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
81 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
58 apply(erule exE) |
82 apply(erule exE) |
63 apply(simp add: fresh_star_def fresh_minus_perm) |
87 apply(simp add: fresh_star_def fresh_minus_perm) |
64 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
88 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
65 apply simp |
89 apply simp |
66 apply(rule a) |
90 apply(rule a) |
67 apply assumption |
91 apply assumption |
68 done |
|
69 |
|
70 lemma alpha_gen_trans: |
|
71 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
|
72 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
|
73 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
|
74 shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)" |
|
75 using a b c using supp_plus_perm |
|
76 apply(simp add: alpha_gen fresh_star_def fresh_def) |
|
77 apply(blast) |
|
78 done |
92 done |
79 |
93 |
80 lemma alpha_gen_atom_trans: |
94 lemma alpha_gen_atom_trans: |
81 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
95 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
82 shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta); |
96 shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta); |
94 apply(drule_tac pi="- pia" in a) |
108 apply(drule_tac pi="- pia" in a) |
95 apply(simp) |
109 apply(simp) |
96 apply(rotate_tac 6) |
110 apply(rotate_tac 6) |
97 apply(drule_tac pi="pia" in a) |
111 apply(drule_tac pi="pia" in a) |
98 apply(simp) |
112 apply(simp) |
99 done |
|
100 |
|
101 lemma alpha_gen_eqvt: |
|
102 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
|
103 and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
|
104 and c: "p \<bullet> (f x) = f (p \<bullet> x)" |
|
105 and d: "p \<bullet> (f y) = f (p \<bullet> y)" |
|
106 shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
|
107 using a b |
|
108 apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric]) |
|
109 apply(simp add: permute_eqvt[symmetric]) |
|
110 apply(simp add: fresh_star_permute_iff) |
|
111 apply(clarsimp) |
|
112 done |
113 done |
113 |
114 |
114 lemma alpha_gen_atom_eqvt: |
115 lemma alpha_gen_atom_eqvt: |
115 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
116 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
116 and b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)" |
117 and b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)" |
257 |
258 |
258 lemma supp_Abs_fun_simp: |
259 lemma supp_Abs_fun_simp: |
259 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
260 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
260 by (lifting supp_abs_fun.simps(1)) |
261 by (lifting supp_abs_fun.simps(1)) |
261 |
262 |
262 lemma supp_Abs_fun_eqvt: |
263 lemma supp_Abs_fun_eqvt [eqvt]: |
263 shows "(p \<bullet> supp_Abs_fun) = supp_Abs_fun" |
264 shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)" |
264 apply(subst permute_fun_def) |
|
265 apply(subst expand_fun_eq) |
|
266 apply(rule allI) |
|
267 apply(induct_tac x rule: abs_induct) |
265 apply(induct_tac x rule: abs_induct) |
268 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
266 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
269 done |
267 done |
270 |
268 |
271 lemma supp_Abs_fun_fresh: |
269 lemma supp_Abs_fun_fresh: |
272 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
270 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
273 apply(rule fresh_fun_eqvt_app) |
271 apply(rule fresh_fun_eqvt_app) |
274 apply(simp add: supp_Abs_fun_eqvt) |
272 apply(simp add: eqvts_raw) |
275 apply(simp) |
273 apply(simp) |
276 done |
274 done |
277 |
275 |
278 lemma Abs_swap: |
276 lemma Abs_swap: |
279 assumes a1: "a \<notin> (supp x) - bs" |
277 assumes a1: "a \<notin> (supp x) - bs" |
324 apply(simp add: finite_supp) |
322 apply(simp add: finite_supp) |
325 done |
323 done |
326 |
324 |
327 lemma Abs_fresh_iff: |
325 lemma Abs_fresh_iff: |
328 fixes x::"'a::fs" |
326 fixes x::"'a::fs" |
329 shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))" |
327 shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
330 apply(simp add: fresh_def) |
328 apply(simp add: fresh_def) |
331 apply(simp add: supp_Abs) |
329 apply(simp add: supp_Abs) |
332 apply(auto) |
330 apply(auto) |
333 done |
331 done |
334 |
332 |
335 lemma Abs_eq_iff: |
333 lemma Abs_eq_iff: |
336 shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
334 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
337 by (lifting alpha_abs.simps(1)) |
335 by (lifting alpha_abs.simps(1)) |
338 |
336 |
339 |
337 |
340 |
338 |
341 (* |
339 (* |
345 *) |
343 *) |
346 |
344 |
347 fun |
345 fun |
348 alpha1 |
346 alpha1 |
349 where |
347 where |
350 "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))" |
348 "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)" |
351 |
349 |
352 notation |
350 notation |
353 alpha1 ("_ \<approx>abs1 _") |
351 alpha1 ("_ \<approx>abs1 _") |
|
352 |
|
353 thm swap_set_not_in |
|
354 |
|
355 lemma qq: |
|
356 fixes S::"atom set" |
|
357 assumes a: "supp p \<inter> S = {}" |
|
358 shows "p \<bullet> S = S" |
|
359 using a |
|
360 apply(simp add: supp_perm permute_set_eq) |
|
361 apply(auto) |
|
362 apply(simp only: disjoint_iff_not_equal) |
|
363 apply(simp) |
|
364 apply (metis permute_atom_def_raw) |
|
365 apply(rule_tac x="(- p) \<bullet> x" in exI) |
|
366 apply(simp) |
|
367 apply(simp only: disjoint_iff_not_equal) |
|
368 apply(simp) |
|
369 apply(metis permute_minus_cancel) |
|
370 done |
|
371 |
|
372 lemma alpha_abs_swap: |
|
373 assumes a1: "(supp x - bs) \<sharp>* p" |
|
374 and a2: "(supp x - bs) \<sharp>* p" |
|
375 shows "(bs, x) \<approx>abs (p \<bullet> bs, p \<bullet> x)" |
|
376 apply(simp) |
|
377 apply(rule_tac x="p" in exI) |
|
378 apply(simp add: alpha_gen) |
|
379 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
380 apply(rule conjI) |
|
381 apply(rule sym) |
|
382 apply(rule qq) |
|
383 using a1 a2 |
|
384 apply(auto)[1] |
|
385 oops |
|
386 |
|
387 |
354 |
388 |
355 lemma |
389 lemma |
356 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
390 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
357 shows "({a}, x) \<approx>abs ({b}, y)" |
391 shows "({a}, x) \<approx>abs ({b}, y)" |
358 using a |
392 using a |
382 apply(simp add: fresh_star_def fresh_def) |
416 apply(simp add: fresh_star_def fresh_def) |
383 apply(blast) |
417 apply(blast) |
384 apply(simp add: supp_swap) |
418 apply(simp add: supp_swap) |
385 done |
419 done |
386 |
420 |
|
421 thm supp_perm |
|
422 |
|
423 lemma perm_induct_test: |
|
424 fixes P :: "perm => bool" |
|
425 assumes zero: "P 0" |
|
426 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
|
427 assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
|
428 shows "P p" |
|
429 sorry |
|
430 |
|
431 |
|
432 lemma tt: |
|
433 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
|
434 apply(induct p rule: perm_induct_test) |
|
435 apply(simp) |
|
436 apply(rule swap_fresh_fresh) |
|
437 apply(case_tac "a \<in> supp x") |
|
438 apply(simp add: fresh_star_def) |
|
439 apply(drule_tac x="a" in bspec) |
|
440 apply(simp) |
|
441 apply(simp add: fresh_def) |
|
442 apply(simp add: supp_swap) |
|
443 apply(simp add: fresh_def) |
|
444 apply(case_tac "b \<in> supp x") |
|
445 apply(simp add: fresh_star_def) |
|
446 apply(drule_tac x="b" in bspec) |
|
447 apply(simp) |
|
448 apply(simp add: fresh_def) |
|
449 apply(simp add: supp_swap) |
|
450 apply(simp add: fresh_def) |
|
451 apply(simp) |
|
452 apply(drule meta_mp) |
|
453 apply(simp add: fresh_star_def fresh_def) |
|
454 apply(drule meta_mp) |
|
455 apply(simp add: fresh_star_def fresh_def) |
|
456 apply(simp) |
|
457 done |
|
458 |
|
459 lemma yy: |
|
460 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
|
461 shows "S1 = S2" |
|
462 using assms |
|
463 apply (metis insert_Diff_single insert_absorb) |
|
464 done |
|
465 |
|
466 |
|
467 lemma |
|
468 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
|
469 shows "(a, x) \<approx>abs1 (b, y)" |
|
470 using a |
|
471 apply(case_tac "a = b") |
|
472 apply(simp) |
|
473 oops |
|
474 |
387 |
475 |
388 end |
476 end |
389 |
477 |