equal
deleted
inserted
replaced
378 lemma Abs_res_fcb: |
378 lemma Abs_res_fcb: |
379 fixes xs ys :: "('a :: at_base) set" |
379 fixes xs ys :: "('a :: at_base) set" |
380 and S T :: "'b :: fs" |
380 and S T :: "'b :: fs" |
381 assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" |
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" |
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" |
383 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" |
384 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S |
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 |
385 \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S |
386 \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
386 \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
387 shows "f xs T = f ys S" |
387 shows "f xs T = f ys S" |
388 using e apply - |
388 using e apply - |
399 apply (subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T") |
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) |
400 apply (metis Un_absorb2 fresh_star_Un) |
401 apply (subst fresh_star_Un) |
401 apply (subst fresh_star_Un) |
402 apply (rule conjI) |
402 apply (rule conjI) |
403 apply (simp add: fresh_star_def f1) |
403 apply (simp add: fresh_star_def f1) |
|
404 apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys") |
404 apply (simp add: fresh_star_def f2) |
405 apply (simp add: fresh_star_def f2) |
|
406 apply blast |
405 apply (simp add: eqv) |
407 apply (simp add: eqv) |
406 done |
408 done |
407 |
409 |
408 nominal_primrec |
410 nominal_primrec |
409 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
411 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |