86 lemma alpha_gen_sym_eqvt: |
86 lemma alpha_gen_sym_eqvt: |
87 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" |
87 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" |
88 and b: "p \<bullet> R = R" |
88 and b: "p \<bullet> R = R" |
89 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
89 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
90 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
90 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
91 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
91 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
92 proof - |
92 apply(auto intro!: alpha_gen_sym) |
93 { assume "R (p \<bullet> x) y" |
93 apply(drule_tac [!] a) |
94 then have "R y (p \<bullet> x)" using a by simp |
94 apply(rule_tac [!] p="p" in permute_boolE) |
95 then have "R (- p \<bullet> y) x" |
95 apply(perm_simp add: permute_minus_cancel b) |
96 apply(rule_tac p="p" in permute_boolE) |
96 apply(assumption) |
97 apply(perm_simp add: permute_minus_cancel b) |
97 apply(perm_simp add: permute_minus_cancel b) |
98 apply(assumption) |
98 apply(assumption) |
99 done |
99 apply(perm_simp add: permute_minus_cancel b) |
100 } |
100 apply(assumption) |
101 then show "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
101 done |
102 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
|
103 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
|
104 unfolding alphas fresh_star_def |
|
105 by (auto simp add: fresh_minus_perm) |
|
106 qed |
|
107 |
102 |
108 lemma alpha_gen_trans: |
103 lemma alpha_gen_trans: |
109 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
104 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
110 shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)" |
105 shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)" |
111 and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)" |
106 and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)" |
112 and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)" |
107 and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)" |
113 using a |
108 using a |
114 unfolding alphas fresh_star_def |
109 unfolding alphas fresh_star_def |
115 by (simp_all add: fresh_plus_perm) |
110 by (simp_all add: fresh_plus_perm) |
116 |
111 |
|
112 |
|
113 lemma alpha_gen_trans_eqvt: |
|
114 assumes b: "(cs, y) \<approx>gen R f q (ds, z)" |
|
115 and a: "(bs, x) \<approx>gen R f p (cs, y)" |
|
116 and d: "q \<bullet> R = R" |
|
117 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
|
118 shows "(bs, x) \<approx>gen R f (q + p) (ds, z)" |
|
119 apply(rule alpha_gen_trans) |
|
120 defer |
|
121 apply(rule a) |
|
122 apply(rule b) |
|
123 apply(drule c) |
|
124 apply(rule_tac p="q" in permute_boolE) |
|
125 apply(perm_simp add: permute_minus_cancel d) |
|
126 apply(assumption) |
|
127 apply(rotate_tac -1) |
|
128 apply(drule_tac p="q" in permute_boolI) |
|
129 apply(perm_simp add: permute_minus_cancel d) |
|
130 apply(simp add: permute_eqvt[symmetric]) |
|
131 done |
|
132 |
|
133 lemma alpha_res_trans_eqvt: |
|
134 assumes b: "(cs, y) \<approx>res R f q (ds, z)" |
|
135 and a: "(bs, x) \<approx>res R f p (cs, y)" |
|
136 and d: "q \<bullet> R = R" |
|
137 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
|
138 shows "(bs, x) \<approx>res R f (q + p) (ds, z)" |
|
139 apply(rule alpha_gen_trans) |
|
140 defer |
|
141 apply(rule a) |
|
142 apply(rule b) |
|
143 apply(drule c) |
|
144 apply(rule_tac p="q" in permute_boolE) |
|
145 apply(perm_simp add: permute_minus_cancel d) |
|
146 apply(assumption) |
|
147 apply(rotate_tac -1) |
|
148 apply(drule_tac p="q" in permute_boolI) |
|
149 apply(perm_simp add: permute_minus_cancel d) |
|
150 apply(simp add: permute_eqvt[symmetric]) |
|
151 done |
|
152 |
|
153 lemma alpha_lst_trans_eqvt: |
|
154 assumes b: "(cs, y) \<approx>lst R f q (ds, z)" |
|
155 and a: "(bs, x) \<approx>lst R f p (cs, y)" |
|
156 and d: "q \<bullet> R = R" |
|
157 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
|
158 shows "(bs, x) \<approx>lst R f (q + p) (ds, z)" |
|
159 apply(rule alpha_gen_trans) |
|
160 defer |
|
161 apply(rule a) |
|
162 apply(rule b) |
|
163 apply(drule c) |
|
164 apply(rule_tac p="q" in permute_boolE) |
|
165 apply(perm_simp add: permute_minus_cancel d) |
|
166 apply(assumption) |
|
167 apply(rotate_tac -1) |
|
168 apply(drule_tac p="q" in permute_boolI) |
|
169 apply(perm_simp add: permute_minus_cancel d) |
|
170 apply(simp add: permute_eqvt[symmetric]) |
|
171 done |
|
172 |
|
173 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt |
|
174 |
|
175 lemma test: |
|
176 shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s" |
|
177 and "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s" |
|
178 and "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s" |
|
179 by (simp_all add: alphas) |
117 |
180 |
118 |
181 |
119 section {* General Abstractions *} |
182 section {* General Abstractions *} |
120 |
183 |
121 fun |
184 fun |