72 fixes pi |
72 fixes pi |
73 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
73 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
74 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
74 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
75 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
75 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
76 using b apply - |
76 using b apply - |
77 apply(simp add: alpha_gen.simps) |
77 apply(simp add: alpha_gen) |
78 apply(erule conjE)+ |
78 apply(erule conjE)+ |
79 apply(rule conjI) |
79 apply(rule conjI) |
80 apply(simp add: fresh_star_def fresh_minus_perm) |
80 apply(simp add: fresh_star_def fresh_minus_perm) |
81 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
81 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
82 apply simp |
82 apply simp |
83 apply(clarify) |
83 apply(clarify) |
84 apply(simp) |
84 apply(simp) |
85 apply(rule a) |
85 apply(rule a) |
86 apply assumption |
86 apply assumption |
87 done |
87 done |
|
88 |
|
89 lemma alpha_gen_compose_sym2: |
|
90 assumes a: "(aa, (t1, t2)) \<approx>gen (\<lambda>(x11, x12) (x21, x22). R1 x11 x21 \<and> R1 x21 x11 \<and> R2 x12 x22 \<and> R2 x22 x12) |
|
91 (\<lambda>(b, a). fb b \<union> fa a) pi (ab, (s1, s2))" |
|
92 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
93 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
94 shows "(ab, (s1, s2)) \<approx>gen |
|
95 (\<lambda>x1 x2. (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x1 x2 \<and> (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x2 x1) |
|
96 (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, (t1, t2))" |
|
97 using a |
|
98 apply(simp add: alpha_gen) |
|
99 apply clarify |
|
100 apply (rule conjI) |
|
101 apply(simp add: fresh_star_def fresh_minus_perm) |
|
102 apply (rule conjI) |
|
103 apply (rotate_tac 3) |
|
104 apply (drule_tac pi="- pi" in r1) |
|
105 apply simp |
|
106 apply (rule conjI) |
|
107 apply (rotate_tac -1) |
|
108 apply (drule_tac pi="- pi" in r2) |
|
109 apply simp |
|
110 apply (rule conjI) |
|
111 apply (drule_tac pi="- pi" in r1) |
|
112 apply simp |
|
113 apply (rule conjI) |
|
114 apply (drule_tac pi="- pi" in r2) |
|
115 apply simp_all |
|
116 done |
88 |
117 |
89 lemma alpha_gen_compose_trans: |
118 lemma alpha_gen_compose_trans: |
90 fixes pi pia |
119 fixes pi pia |
91 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)" |
120 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)" |
92 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
121 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |