360 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)" |
360 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)" |
361 unfolding eqvt_def subst_graph_def |
361 unfolding eqvt_def subst_graph_def |
362 apply (rule, perm_simp, rule) |
362 apply (rule, perm_simp, rule) |
363 apply(rule TrueI) |
363 apply(rule TrueI) |
364 apply(case_tac x) |
364 apply(case_tac x) |
365 apply(simp) |
|
366 apply(rule_tac y="b" in ty2.exhaust) |
365 apply(rule_tac y="b" in ty2.exhaust) |
367 apply(blast) |
366 apply(blast) |
368 apply(blast) |
367 apply(blast) |
369 apply(simp_all add: ty2.distinct) |
368 apply(simp_all add: ty2.distinct) |
370 done |
369 done |
371 |
370 |
372 termination |
371 termination |
373 apply(relation "measure (size o snd)") |
372 by (relation "measure (size o snd)") (simp_all add: ty2.size) |
374 apply(simp_all add: ty2.size) |
|
375 done |
|
376 |
373 |
377 lemma subst_eqvt[eqvt]: |
374 lemma subst_eqvt[eqvt]: |
378 shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)" |
375 shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)" |
379 apply(induct \<theta> T rule: subst.induct) |
376 by (induct \<theta> T rule: subst.induct) (simp_all add: lookup2_eqvt) |
380 apply(simp_all add: lookup2_eqvt) |
|
381 done |
|
382 |
377 |
383 lemma supp_fun_app2_eqvt: |
378 lemma supp_fun_app2_eqvt: |
384 assumes e: "eqvt f" |
379 assumes e: "eqvt f" |
385 shows "supp (f a b) \<subseteq> supp a \<union> supp b" |
380 shows "supp (f a b) \<subseteq> supp a \<union> supp b" |
386 using supp_fun_app_eqvt[OF e] supp_fun_app |
381 using supp_fun_app_eqvt[OF e] supp_fun_app |
392 unfolding eqvt_def by (simp add: eqvts_raw) |
387 unfolding eqvt_def by (simp add: eqvts_raw) |
393 |
388 |
394 lemma fresh_star_inter1: |
389 lemma fresh_star_inter1: |
395 "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z" |
390 "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z" |
396 unfolding fresh_star_def by blast |
391 unfolding fresh_star_def by blast |
397 |
392 |
|
393 lemma Abs_res_fcb: |
|
394 fixes xs ys :: "('a :: at_base) set" |
|
395 and S T :: "'b :: fs" |
|
396 assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" |
|
397 and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T" |
|
398 and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T" |
|
399 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S |
|
400 \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
|
401 shows "f xs T = f ys S" |
|
402 using e apply - |
|
403 apply (subst (asm) Abs_eq_res_set) |
|
404 apply (subst (asm) Abs_eq_iff2) |
|
405 apply (simp add: alphas) |
|
406 apply (elim exE conjE) |
|
407 apply(rule trans) |
|
408 apply (rule_tac p="p" in supp_perm_eq[symmetric]) |
|
409 apply(rule fresh_star_supp_conv) |
|
410 apply(drule fresh_star_perm_set_conv) |
|
411 apply (rule finite_Diff) |
|
412 apply (rule finite_supp) |
|
413 apply (subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T") |
|
414 apply (metis Un_absorb2 fresh_star_Un) |
|
415 apply (subst fresh_star_Un) |
|
416 apply (rule conjI) |
|
417 apply (simp add: fresh_star_def f1) |
|
418 apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys") |
|
419 apply (simp add: fresh_star_def f2) |
|
420 apply blast |
|
421 apply (simp add: eqv) |
|
422 done |
|
423 |
398 nominal_primrec |
424 nominal_primrec |
399 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
425 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
400 where |
426 where |
401 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)" |
427 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)" |
402 unfolding eqvt_def substs_graph_def |
428 unfolding eqvt_def substs_graph_def |
403 apply (rule, perm_simp, rule) |
429 apply (rule, perm_simp, rule) |
404 apply auto[2] |
430 apply auto[2] |
405 apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) |
431 apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) |
406 apply auto |
432 apply auto |
407 apply (subst (asm) Abs_eq_res_set) |
433 apply (erule Abs_res_fcb) |
408 apply (subst (asm) Abs_eq_iff2) |
|
409 apply (clarify) |
|
410 apply (simp add: alphas) |
|
411 apply (clarify) |
|
412 apply (rule trans) |
|
413 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
414 apply(rule fresh_star_supp_conv) |
|
415 apply(drule fresh_star_perm_set_conv) |
|
416 apply (rule finite_Diff) |
|
417 apply (rule finite_supp) |
|
418 apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* ([atom ` fset xs]res. subst \<theta>' t)") |
|
419 apply (metis Un_absorb2 fresh_star_Un) |
|
420 apply (subst fresh_star_Un) |
|
421 apply (rule conjI) |
|
422 apply (simp (no_asm) add: fresh_star_def) |
|
423 apply (rule) |
|
424 apply (simp add: Abs_fresh_iff) |
434 apply (simp add: Abs_fresh_iff) |
425 apply (simp add: fresh_star_def) |
435 apply (simp add: Abs_fresh_iff) |
426 apply (rule) |
|
427 apply (simp (no_asm) add: Abs_fresh_iff) |
|
428 apply auto[1] |
436 apply auto[1] |
429 apply (simp add: fresh_def supp_Abs) |
437 apply (simp add: fresh_def fresh_star_def) |
430 apply (rule contra_subsetD) |
438 apply (rule contra_subsetD[OF supp_subst]) |
431 apply (rule supp_subst) |
|
432 apply auto[1] |
|
433 apply simp |
439 apply simp |
|
440 apply blast |
|
441 apply clarify |
|
442 apply (simp add: subst_eqvt) |
434 apply (subst Abs_eq_iff) |
443 apply (subst Abs_eq_iff) |
435 apply (rule_tac x="0::perm" in exI) |
444 apply (rule_tac x="0::perm" in exI) |
436 apply (subgoal_tac "p \<bullet> subst \<theta>' t = subst \<theta>' (p \<bullet> t)") |
445 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
437 prefer 2 |
|
438 apply (subgoal_tac "\<theta>' = p \<bullet> \<theta>'") |
|
439 apply (simp add: subst_eqvt) |
|
440 apply (rule sym) |
|
441 apply (rule perm_supp_eq) |
|
442 apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'") |
|
443 apply (metis Diff_partition fresh_star_Un) |
|
444 apply (simp add: fresh_star_Un fresh_star_inter1) |
|
445 apply (simp add: alphas fresh_star_zero) |
446 apply (simp add: alphas fresh_star_zero) |
446 apply auto[1] |
447 apply auto[1] |
447 apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
448 apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
448 apply (simp add: inter_eqvt) |
449 apply (simp add: inter_eqvt) |
449 apply blast |
450 apply blast |
450 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
451 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
451 apply (simp add: IntI image_eqI) |
452 apply (auto simp add: IntI image_eqI) |
452 apply (drule subsetD[OF supp_subst]) |
453 apply (drule subsetD[OF supp_subst]) |
453 apply (simp add: fresh_star_def fresh_def) |
454 apply (simp add: fresh_star_def fresh_def) |
454 apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
455 apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
455 apply (simp add: ) |
456 apply (simp) |
456 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
457 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
457 apply (metis inf1I inter_eqvt mem_def supp_eqvt ) |
458 apply (metis inf1I inter_eqvt mem_def supp_eqvt) |
458 apply (rotate_tac 6) |
459 apply (subgoal_tac "x \<notin> supp \<theta>'") |
459 apply (drule sym) |
460 apply (metis UnE subsetD supp_subst) |
460 apply (simp add: subst_eqvt) |
461 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>')") |
461 apply (drule subsetD[OF supp_subst]) |
|
462 apply auto[1] |
|
463 apply (rotate_tac 2) |
|
464 apply (subst (asm) fresh_star_permute_iff[symmetric]) |
|
465 apply (simp add: fresh_star_def fresh_def) |
462 apply (simp add: fresh_star_def fresh_def) |
|
463 apply (simp (no_asm) add: fresh_star_permute_iff) |
|
464 apply (rule perm_supp_eq) |
|
465 apply (simp add: fresh_def fresh_star_def) |
466 apply blast |
466 apply blast |
467 done |
467 done |
468 |
468 |
469 |
469 |
470 text {* Some Tests about Alpha-Equality *} |
470 text {* Some Tests about Alpha-Equality *} |