equal
deleted
inserted
replaced
23 apply(simp add: eqvt_at_def) |
23 apply(simp add: eqvt_at_def) |
24 apply(simp add: swap_fresh_fresh) |
24 apply(simp add: swap_fresh_fresh) |
25 apply(rule fin) |
25 apply(rule fin) |
26 done |
26 done |
27 |
27 |
|
28 lemma finite_supp_eqvt_at: |
|
29 assumes asm: "eqvt_at f x" |
|
30 and fin: "finite (supp x)" |
|
31 shows "finite (supp (f x))" |
|
32 apply(rule finite_subset) |
|
33 apply(rule supp_eqvt_at[OF asm fin]) |
|
34 apply(rule fin) |
|
35 done |
28 |
36 |
29 definition |
37 definition |
30 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
38 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
31 |
39 |
32 lemma eqvtI: |
40 lemma eqvtI: |
1700 done |
1708 done |
1701 |
1709 |
1702 thm depth.psimps |
1710 thm depth.psimps |
1703 thm depth.simps |
1711 thm depth.simps |
1704 |
1712 |
|
1713 |
|
1714 lemma swap_set_not_in_at: |
|
1715 fixes a b::"'a::at" |
|
1716 and S::"'a::at set" |
|
1717 assumes a: "a \<notin> S" "b \<notin> S" |
|
1718 shows "(a \<leftrightarrow> b) \<bullet> S = S" |
|
1719 unfolding permute_set_eq |
|
1720 using a by (auto simp add: permute_flip_at) |
|
1721 |
|
1722 |
1705 nominal_primrec |
1723 nominal_primrec |
1706 frees :: "lam \<Rightarrow> name set" |
1724 frees :: "lam \<Rightarrow> name set" |
1707 where |
1725 where |
1708 "frees (Var x) = {x}" |
1726 "frees (Var x) = {x}" |
1709 | "frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
1727 | "frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
1722 apply(simp add: Abs_fresh_iff) |
1740 apply(simp add: Abs_fresh_iff) |
1723 apply(simp add: Abs_fresh_iff) |
1741 apply(simp add: Abs_fresh_iff) |
1724 apply(simp add: Abs_fresh_iff) |
1742 apply(simp add: Abs_fresh_iff) |
1725 apply(simp) |
1743 apply(simp) |
1726 apply(drule test) |
1744 apply(drule test) |
|
1745 apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst) |
1727 oops |
1746 oops |
1728 |
1747 |
1729 nominal_primrec |
1748 nominal_primrec |
1730 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1749 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
1731 where |
1750 where |