256 apply metis apply assumption |
256 apply metis apply assumption |
257 apply clarify |
257 apply clarify |
258 --"This is exactly the assumption for the properly defined function" |
258 --"This is exactly the assumption for the properly defined function" |
259 defer |
259 defer |
260 apply (simp add: ty_tys.eq_iff) |
260 apply (simp add: ty_tys.eq_iff) |
|
261 apply (subgoal_tac "(atom ` fset xsa - atom ` fset xs) \<sharp>* ([atom ` fset xs]set. T)") |
261 apply (subst (asm) Abs_eq_iff2) |
262 apply (subst (asm) Abs_eq_iff2) |
262 apply (simp add: alpha_res.simps) |
263 apply (simp add: alphas) |
263 apply (clarify) |
264 apply (clarify) |
264 apply (rule trans) |
265 apply (rule trans) |
265 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
266 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
266 apply(rule fresh_star_supp_conv) |
267 apply(rule fresh_star_supp_conv) |
267 thm fresh_star_perm_set_conv |
268 thm fresh_star_perm_set_conv |
268 apply(drule fresh_star_perm_set_conv) |
269 apply(drule fresh_star_perm_set_conv) |
269 apply (rule finite_Diff) |
270 apply (rule finite_Diff) |
270 apply (rule finite_supp) |
271 apply (rule finite_supp) |
271 apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]res. subst \<theta>' T)") |
272 apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]set. subst \<theta>' T)") |
272 apply (metis Un_absorb2 fresh_star_Un) |
273 apply (metis Un_absorb2 fresh_star_Un) |
273 apply (simp add: fresh_star_Un) |
274 apply (simp add: fresh_star_Un) |
274 apply (rule conjI) |
275 apply (rule conjI) |
275 apply (simp add: fresh_star_def) |
276 apply (simp add: fresh_star_def) |
276 apply rule |
277 apply rule |
277 apply(simp (no_asm) only: Abs_fresh_iff) |
278 apply(simp (no_asm) only: Abs_fresh_iff) |
278 apply(clarify) |
279 apply(clarify) |
279 apply blast |
280 apply simp |
280 defer |
281 apply (simp add: fresh_star_def) |
|
282 apply rule |
|
283 apply(simp (no_asm) only: Abs_fresh_iff) |
|
284 apply(clarify) |
|
285 apply(drule_tac a="atom a" in fresh_eqvt_at) |
|
286 apply (simp add: supp_Pair finite_supp) |
|
287 apply (simp add: fresh_Pair) |
|
288 apply(simp add: Abs_fresh_iff) |
|
289 apply(simp add: Abs_fresh_iff) |
281 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
290 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
282 prefer 2 |
291 prefer 2 |
283 apply (rule perm_supp_eq) |
292 apply (rule perm_supp_eq) |
284 apply (metis Un_absorb2 fresh_star_Un) |
293 apply (metis Un_absorb2 fresh_star_Un) |
285 apply simp |
294 apply (simp add: eqvt_at_def) |
286 --"Would work for 'set' and 'list' bindings, not sure how to do 'set+'." |
295 apply (simp add: fresh_star_def) |
|
296 apply rule |
|
297 apply(simp add: Abs_fresh_iff) |
287 oops |
298 oops |
288 |
299 |
289 |
300 |
290 section {* defined as two separate nominal datatypes *} |
301 section {* defined as two separate nominal datatypes *} |
291 |
302 |