# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295344977 -3600
# Node ID 1d1772a89026d33f28effe3b6c19f319704aa3f2
# Parent  92c001d932258402bdd0b8cb3f9853a02407ab43
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

diff -r 92c001d93225 -r 1d1772a89026 Nominal/Ex/Lambda.thy
--- 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))"
diff -r 92c001d93225 -r 1d1772a89026 Nominal/Nominal2_Abs.thy
--- 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 *}
diff -r 92c001d93225 -r 1d1772a89026 Nominal/Nominal2_Base.thy
--- 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)"