the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
--- a/Nominal/Ex/Lambda.thy Tue Jan 18 06:55:18 2011 +0100
+++ b/Nominal/Ex/Lambda.thy Tue Jan 18 11:02:57 2011 +0100
@@ -102,6 +102,58 @@
apply(simp_all add: lam.supp supp_at_base)
done
+nominal_datatype ln =
+ LNBnd nat
+| LNVar name
+| LNApp ln ln
+| LNLam ln
+
+fun
+ lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln"
+where
+ "lookup [] n x = LNVar x"
+| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
+
+lemma [eqvt]:
+ shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
+apply(induct xs arbitrary: n)
+apply(simp_all add: permute_pure)
+done
+
+nominal_primrec
+ trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
+where
+ "trans (Var x) xs = lookup xs 0 x"
+| "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
+| "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+apply(simp_all)[3]
+apply(blast)
+apply(blast)
+apply(simp add: fresh_star_def)
+apply(simp_all add: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.eq_iff)
+apply(simp add: Abs_eq_iff)
+apply(erule conjE)
+apply(erule exE)
+apply(simp add: alphas)
+apply(simp add: atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(simp (no_asm) add: ln.supp)
+apply(drule supp_eqvt_at)
+apply(simp add: finite_supp)
+oops
+
+
+
+
+
nominal_datatype db =
DBVar nat
| DBApp db db
@@ -112,7 +164,6 @@
where
"c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
-
lemma mbind_eqvt:
fixes c::"'a::pt option"
shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
--- a/Nominal/Nominal2_Abs.thy Tue Jan 18 06:55:18 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy Tue Jan 18 11:02:57 2011 +0100
@@ -342,6 +342,41 @@
by (auto dest: disjoint_right_eq)
qed
+lemma alpha_abs_res_stronger1:
+ fixes x::"'a::fs"
+ assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
+ shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')"
+proof -
+ from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas)
+ then have #: "p' \<bullet> (supp x - as) = (supp x - as)"
+ by (simp add: atom_set_perm_eq)
+ have "finite (supp x)" by (simp add: finite_supp)
+ then obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"
+ using set_renaming_perm by blast
+ from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
+ from 0 have 1: "(supp x - as) \<sharp>* p" using *
+ by (auto simp add: fresh_star_def fresh_perm)
+ then have 2: "(supp x - as) \<inter> supp p = {}"
+ by (auto simp add: fresh_star_def fresh_def)
+ have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
+ have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp
+ also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))"
+ using b by simp
+ also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as)))"
+ by (simp add: union_eqvt)
+ also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> (supp x \<inter> as))"
+ using # by auto
+ also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using asm
+ by (simp add: supp_property_res)
+ finally have "supp p \<subseteq> (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" .
+ then
+ have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto
+ moreover
+ have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas)
+ ultimately
+ show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast
+qed
+
section {* Quotient types *}
--- a/Nominal/Nominal2_Base.thy Tue Jan 18 06:55:18 2011 +0100
+++ b/Nominal/Nominal2_Base.thy Tue Jan 18 11:02:57 2011 +0100
@@ -518,6 +518,18 @@
unfolding permute_set_eq
using a by (auto simp add: swap_atom)
+lemma swap_set_in_eq:
+ assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
+ shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
+ unfolding permute_set_eq
+ using a by (auto simp add: swap_atom)
+
+lemma swap_set_both_in:
+ assumes a: "a \<in> S" "b \<in> S"
+ shows "(a \<rightleftharpoons> b) \<bullet> S = S"
+ unfolding permute_set_eq
+ using a by (auto simp add: swap_atom)
+
lemma mem_permute_iff:
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
unfolding mem_def permute_fun_def permute_bool_def
@@ -1717,7 +1729,7 @@
by (rule_tac S="supp p" in perm_struct_induct)
(auto intro: zero swap)
-lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
+lemma perm_struct_induct2[consumes 1, case_names zero swap plus]:
assumes S: "supp p \<subseteq> S"
assumes zero: "P 0"
assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
@@ -1727,6 +1739,14 @@
by (induct p rule: perm_struct_induct)
(auto intro: zero plus swap simp add: supp_swap)
+lemma perm_simple_struct_induct2[case_names zero swap plus]:
+ assumes zero: "P 0"
+ assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+ assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+ shows "P p"
+by (rule_tac S="supp p" in perm_struct_induct2)
+ (auto intro: zero swap plus)
+
lemma supp_perm_eq:
assumes "(supp x) \<sharp>* p"
shows "p \<bullet> x = x"
@@ -1751,7 +1771,7 @@
from assms have "supp p \<subseteq> {a. a \<sharp> x}"
unfolding supp_perm fresh_star_def fresh_def by auto
then show "p \<bullet> x = x"
- proof (induct p rule: perm_subset_induct)
+ proof (induct p rule: perm_struct_induct2)
case zero
show "0 \<bullet> x = x" by simp
next
@@ -1925,7 +1945,6 @@
section {* Renaming permutations *}
-
lemma set_renaming_perm:
assumes b: "finite bs"
shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"