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