441 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)" |
441 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)" |
442 "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) = |
442 "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) = |
443 (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
443 (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
444 \<and> pi \<bullet> bsl = csl)" |
444 \<and> pi \<bullet> bsl = csl)" |
445 by (simp_all add: alphas) |
445 by (simp_all add: alphas) |
|
446 |
|
447 lemma alphas3: |
|
448 "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and> |
|
449 (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and> |
|
450 R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)" |
|
451 by (simp add: alphas) |
446 |
452 |
447 lemma alpha_gen_compose_sym: |
453 lemma alpha_gen_compose_sym: |
448 fixes pi |
454 fixes pi |
449 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
455 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
450 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
456 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |