--- a/Nominal/Ex/LamTest.thy Mon Jan 10 08:51:51 2011 +0000
+++ b/Nominal/Ex/LamTest.thy Mon Jan 10 11:36:55 2011 +0000
@@ -25,6 +25,14 @@
apply(rule fin)
done
+lemma finite_supp_eqvt_at:
+ assumes asm: "eqvt_at f x"
+ and fin: "finite (supp x)"
+ shows "finite (supp (f x))"
+apply(rule finite_subset)
+apply(rule supp_eqvt_at[OF asm fin])
+apply(rule fin)
+done
definition
"eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
@@ -1702,6 +1710,16 @@
thm depth.psimps
thm depth.simps
+
+lemma swap_set_not_in_at:
+ fixes a b::"'a::at"
+ and S::"'a::at set"
+ assumes a: "a \<notin> S" "b \<notin> S"
+ shows "(a \<leftrightarrow> b) \<bullet> S = S"
+ unfolding permute_set_eq
+ using a by (auto simp add: permute_flip_at)
+
+
nominal_primrec
frees :: "lam \<Rightarrow> name set"
where
@@ -1724,6 +1742,7 @@
apply(simp add: Abs_fresh_iff)
apply(simp)
apply(drule test)
+apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst)
oops
nominal_primrec
--- a/Nominal/Nominal2_Base.thy Mon Jan 10 08:51:51 2011 +0000
+++ b/Nominal/Nominal2_Base.thy Mon Jan 10 11:36:55 2011 +0000
@@ -952,18 +952,6 @@
instance atom :: fs
by default (simp add: supp_atom)
-section {* Support for finite sets of atoms *}
-
-lemma supp_finite_atom_set:
- fixes S::"atom set"
- assumes "finite S"
- shows "supp S = S"
- apply(rule finite_supp_unique)
- apply(simp add: supports_def)
- apply(simp add: swap_set_not_in)
- apply(rule assms)
- apply(simp add: swap_set_in)
-done
section {* Type @{typ perm} is finitely-supported. *}
@@ -1266,6 +1254,27 @@
section {* Support of Finite Sets of Finitely Supported Elements *}
+text {* support and freshness for atom sets *}
+
+lemma supp_finite_atom_set:
+ fixes S::"atom set"
+ assumes "finite S"
+ shows "supp S = S"
+ apply(rule finite_supp_unique)
+ apply(simp add: supports_def)
+ apply(simp add: swap_set_not_in)
+ apply(rule assms)
+ apply(simp add: swap_set_in)
+done
+
+lemma fresh_finite_atom_set:
+ fixes S::"atom set"
+ assumes "finite S"
+ shows "a \<sharp> S \<longleftrightarrow> a \<notin> S"
+ unfolding fresh_def
+ by (simp add: supp_finite_atom_set[OF assms])
+
+
lemma Union_fresh:
shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
unfolding Union_image_eq[symmetric]
@@ -1977,6 +1986,18 @@
apply(auto)
done
+lemma fresh_finite_set_at_base:
+ fixes a::"'a::at_base"
+ assumes a: "finite S"
+ shows "atom a \<sharp> S \<longleftrightarrow> a \<notin> S"
+ unfolding fresh_def
+ apply(simp add: supp_finite_set_at_base[OF a])
+ apply(subst inj_image_mem_iff)
+ apply(simp add: inj_on_def)
+ apply(simp)
+ done
+
+
section {* Infrastructure for concrete atom types *}
section {* A swapping operation for concrete atoms *}