85 apply(rule a) |
85 apply(rule a) |
86 apply assumption |
86 apply assumption |
87 done |
87 done |
88 |
88 |
89 lemma alpha_gen_compose_sym2: |
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) |
90 assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22). |
91 (\<lambda>(b, a). fb b \<union> fa a) pi (ab, (s1, s2))" |
91 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<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)" |
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)" |
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 |
94 shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
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) |
95 using a |
96 (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, (t1, t2))" |
96 apply(simp add: alpha_gen) |
97 using a |
97 apply clarify |
98 apply(simp add: alpha_gen) |
98 apply (rule conjI) |
99 apply clarify |
|
100 apply (rule conjI) |
|
101 apply(simp add: fresh_star_def fresh_minus_perm) |
99 apply(simp add: fresh_star_def fresh_minus_perm) |
102 apply (rule conjI) |
100 apply (rule conjI) |
103 apply (rotate_tac 3) |
101 apply (rotate_tac 3) |
104 apply (drule_tac pi="- pi" in r1) |
102 apply (drule_tac pi="- pi" in r1) |
105 apply simp |
103 apply simp |
106 apply (rule conjI) |
104 apply (rule conjI) |
107 apply (rotate_tac -1) |
105 apply (rotate_tac -1) |
108 apply (drule_tac pi="- pi" in r2) |
106 apply (drule_tac pi="- pi" in r2) |
109 apply simp |
107 apply simp_all |
110 apply (rule conjI) |
108 done |
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 |
|
117 |
109 |
118 lemma alpha_gen_compose_trans: |
110 lemma alpha_gen_compose_trans: |
119 fixes pi pia |
111 fixes pi pia |
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)" |
112 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)" |
121 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
113 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |