253 apply rule |
253 apply rule |
254 apply(simp (no_asm) only: Abs_fresh_iff) |
254 apply(simp (no_asm) only: Abs_fresh_iff) |
255 apply(clarify) |
255 apply(clarify) |
256 apply auto[1] |
256 apply auto[1] |
257 apply (simp add: fresh_star_def fresh_def) |
257 apply (simp add: fresh_star_def fresh_def) |
258 --"HERE" |
258 |
259 apply (simp (no_asm) add: fresh_star_def) |
259 apply (simp (no_asm) add: fresh_star_def) |
260 apply rule |
260 apply rule |
261 apply auto[1] |
261 apply auto[1] |
262 apply(simp (no_asm) only: Abs_fresh_iff) |
262 apply(simp (no_asm) only: Abs_fresh_iff) |
263 apply(clarify) |
263 apply(clarify) |
264 apply auto[1] |
264 apply auto[1] |
265 prefer 2 |
|
266 apply (simp add: fresh_def) |
|
267 apply(drule_tac a="atom x" in fresh_eqvt_at) |
265 apply(drule_tac a="atom x" in fresh_eqvt_at) |
268 apply (simp add: supp_Pair finite_supp) |
266 apply (simp add: supp_Pair finite_supp) |
269 apply (simp add: fresh_Pair) |
267 apply (simp add: fresh_Pair) |
270 apply(auto simp add: Abs_fresh_iff fresh_star_def)[1] |
268 apply(auto simp add: Abs_fresh_iff fresh_star_def)[2] |
271 apply auto[1] |
269 apply (simp add: fresh_def) |
272 |
|
273 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
270 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
274 prefer 2 |
271 prefer 2 |
275 apply (rule perm_supp_eq) |
272 apply (rule perm_supp_eq) |
276 apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'") |
273 apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'") |
277 apply (auto simp add: fresh_star_def)[1] |
274 apply (auto simp add: fresh_star_def)[1] |
289 apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)") |
286 apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)") |
290 apply simp |
287 apply simp |
291 apply (subst supp_Pair[symmetric]) |
288 apply (subst supp_Pair[symmetric]) |
292 apply (rule supp_eqvt_at) |
289 apply (rule supp_eqvt_at) |
293 apply (simp add: eqvt_at_def) |
290 apply (simp add: eqvt_at_def) |
294 defer --"because eqvt_at Ta" |
291 apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)") |
|
292 apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)") |
|
293 apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)") |
|
294 apply (thin_tac "(atom ` fset xsa \<inter> supp (p \<bullet> T) - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)") |
|
295 apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'") |
|
296 apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'") |
|
297 apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p") |
|
298 apply (rule) |
|
299 apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)") |
|
300 apply (erule_tac x="p" in allE) |
|
301 apply (erule_tac x="pa + p" in allE) |
|
302 apply (metis permute_plus) |
|
303 apply assumption |
295 apply (simp add: supp_Pair finite_supp) |
304 apply (simp add: supp_Pair finite_supp) |
296 prefer 2 apply blast |
305 prefer 2 apply blast |
297 prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI) |
306 prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI) |
298 --"p and xs and xsa are fresh for theta" |
307 apply (rule_tac s="supp \<theta>'" in trans) |
|
308 apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'") |
|
309 apply (auto simp add: fresh_star_def fresh_def)[1] |
|
310 apply (subgoal_tac "supp p \<sharp>* \<theta>'") |
|
311 apply (metis fresh_star_permute_iff) |
|
312 apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'") |
|
313 apply (auto simp add: fresh_star_def)[1] |
|
314 apply (simp add: fresh_star_Un) |
|
315 apply (auto simp add: fresh_star_def fresh_def)[1] |
299 oops |
316 oops |
300 |
317 |
301 section {* defined as two separate nominal datatypes *} |
318 section {* defined as two separate nominal datatypes *} |
302 |
319 |
303 nominal_datatype ty2 = |
320 nominal_datatype ty2 = |