96 apply(simp only: foo.eq_iff) |
96 apply(simp only: foo.eq_iff) |
97 apply(simp only: eqvts) |
97 apply(simp only: eqvts) |
98 apply simp |
98 apply simp |
99 by (metis assms(2) atom_eqvt fresh_perm) |
99 by (metis assms(2) atom_eqvt fresh_perm) |
100 |
100 |
|
101 lemma Let2_rename3: |
|
102 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" |
|
103 and "(supp ([[atom y]]lst. t2)) \<sharp>* p" |
|
104 and "(atom x) \<sharp> p" |
|
105 shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)" |
|
106 using assms |
|
107 apply - |
|
108 apply(drule supp_perm_eq[symmetric]) |
|
109 apply(drule supp_perm_eq[symmetric]) |
|
110 apply(simp only: foo.eq_iff) |
|
111 apply(simp only: eqvts) |
|
112 apply simp |
|
113 by (metis assms(2) atom_eqvt fresh_perm) |
|
114 |
101 lemma strong_exhaust1: |
115 lemma strong_exhaust1: |
102 fixes c::"'a::fs" |
116 fixes c::"'a::fs" |
103 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
117 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
104 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
118 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
105 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
119 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
193 apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2) |
207 apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2) |
194 apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs) |
208 apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs) |
195 apply (simp add: fresh_star_def supp_atom) |
209 apply (simp add: fresh_star_def supp_atom) |
196 done |
210 done |
197 |
211 |
|
212 lemma strong_exhaust2: |
|
213 fixes c::"'a::fs" |
|
214 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
215 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
216 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
217 and "\<And>assn1 trm1 assn2 trm2. |
|
218 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
219 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
220 shows "P" |
|
221 apply (rule strong_exhaust1) |
|
222 apply (erule assms) |
|
223 apply (erule assms) |
|
224 apply (erule assms) apply assumption |
|
225 apply (erule assms) apply assumption |
|
226 apply(case_tac "x1 = x2") |
|
227 apply(subgoal_tac |
|
228 "\<exists>q. (q \<bullet> {atom x1, atom x2}) \<sharp>* c \<and> (supp (([[atom x1, atom x2]]lst. trm1), ([[atom x2]]lst. trm2))) \<sharp>* q") |
|
229 apply(erule exE)+ |
|
230 apply(erule conjE)+ |
|
231 apply(perm_simp) |
|
232 apply(rule assms(5)) |
|
233 apply assumption |
|
234 apply simp |
|
235 apply (rule Let2_rename) |
|
236 apply (simp only: supp_Pair) |
|
237 apply (simp only: fresh_star_Un_elim) |
|
238 apply (simp only: supp_Pair) |
|
239 apply (simp only: fresh_star_Un_elim) |
|
240 apply(rule at_set_avoiding2) |
|
241 apply(simp add: finite_supp) |
|
242 apply(simp add: finite_supp) |
|
243 apply(simp add: finite_supp) |
|
244 apply clarify |
|
245 apply (simp add: fresh_star_def) |
|
246 apply (simp add: fresh_def supp_Pair supp_Abs) |
|
247 |
|
248 apply(subgoal_tac |
|
249 "\<exists>q. (q \<bullet> {atom x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<sharp>* q") |
|
250 apply(erule exE)+ |
|
251 apply(erule conjE)+ |
|
252 apply(rule assms(5)) |
|
253 apply(perm_simp) |
|
254 apply(simp (no_asm) add: fresh_star_insert) |
|
255 apply(rule conjI) |
|
256 apply (simp add: fresh_star_def) |
|
257 apply(rotate_tac 2) |
|
258 apply(simp add: fresh_star_def) |
|
259 apply(simp) |
|
260 apply (rule Let2_rename3) |
|
261 apply (simp add: supp_Pair fresh_star_union) |
|
262 apply (simp add: supp_Pair fresh_star_union) |
|
263 apply (simp add: supp_Pair fresh_star_union) |
|
264 apply clarify |
|
265 apply (simp add: fresh_star_def supp_atom) |
|
266 apply(rule at_set_avoiding2) |
|
267 apply(simp add: finite_supp) |
|
268 apply(simp add: finite_supp) |
|
269 apply(simp add: finite_supp) |
|
270 apply(simp add: fresh_star_def) |
|
271 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
|
272 done |
198 |
273 |
199 end |
274 end |
200 |
275 |
201 |
276 |
202 |
277 |