--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Lambda_F_T.thy	Fri Jun 03 18:32:22 2011 +0900
@@ -0,0 +1,139 @@
+theory Lambda
+imports "../Nominal2" 
+begin
+
+atom_decl name
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
+
+lemma Abs1_eq_fdest:
+  fixes x y :: "'a :: at_base"
+    and S T :: "'b :: fs"
+  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
+  and "sort_of (atom x) = sort_of (atom y)"
+  shows "f x T = f y S"
+using assms apply -
+apply (subst (asm) Abs1_eq_iff')
+apply simp_all
+apply (elim conjE disjE)
+apply simp
+apply(rule trans)
+apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(simp add: supp_swap fresh_star_def)
+apply(simp add: swap_commute)
+done
+
+lemma fresh_fun_eqvt_app3:
+  assumes a: "eqvt f"
+  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
+  shows "a \<sharp> f x y z"
+  using fresh_fun_eqvt_app[OF a b(1)] a b
+  by (metis fresh_fun_app)
+
+lemma fresh_fun_eqvt_app4:
+  assumes a: "eqvt f"
+  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
+  shows "a \<sharp> f x y z w"
+  using fresh_fun_eqvt_app[OF a b(1)] a b
+  by (metis fresh_fun_app)
+
+nominal_primrec
+  f
+where
+  "f f1 f2 f3 (Var x) l = f1 x l"
+| "f f1 f2 f3 (App t1 t2) l = f2 t1 t2 (f f1 f2 f3 t1 l) (f f1 f2 f3 t2 l) l"
+| "(\<And>t l r. atom x \<sharp> r \<Longrightarrow> atom x \<sharp> f3 x t r l) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3,l) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t) l) = f3 x t (f f1 f2 f3 t (x # l)) l"
+  apply (simp add: eqvt_def f_graph_def)
+  apply (rule, perm_simp, rule)
+  apply(case_tac x)
+  apply(rule_tac y="d" and c="z" in lam.strong_exhaust)
+  apply(auto simp add: fresh_star_def)
+  apply(blast)
+  apply blast
+  defer
+  apply(simp add: fresh_Pair_elim)
+  apply(erule Abs1_eq_fdest)
+  defer
+  apply simp_all
+  apply (rule_tac f="f3a" in fresh_fun_eqvt_app4)
+  apply assumption
+  apply (simp add: fresh_at_base)
+  apply assumption
+  apply (erule fresh_eqvt_at)
+  apply (simp add: supp_Pair supp_fun_eqvt finite_supp)
+  apply (simp add: fresh_Pair)
+  apply (simp add: fresh_Cons)
+  apply (simp add: fresh_Cons fresh_at_base)
+  apply (assumption)
+  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3a x y r l) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
+  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
+  apply (simp add: eqvt_at_def eqvt_def)
+  apply (simp add: swap_fresh_fresh)
+  apply (simp add: permute_fun_app_eq)
+  apply (simp add: eqvt_def)
+  prefer 2
+  apply (subgoal_tac "atom x \<sharp> f_sumC (f1a, f2a, f3a, t, x # la)")
+  apply simp
+--"I believe this holds by induction on the graph..."
+  unfolding f_sumC_def
+  apply (rule_tac y="t" in lam.exhaust)
+  apply (subgoal_tac "THE_default undefined (f_graph (f1a, f2a, f3a, t, x # la)) = f1a name (x # la)")
+  apply simp
+  defer
+  apply (rule THE_default1_equality)
+  apply simp
+  defer
+  apply simp
+  apply (rule_tac ?f1.0="f1a" in f_graph.intros(1))
+  sorry (*this could be defined? *)
+
+termination
+  by (relation "measure (\<lambda>(_,_,_,x,_). size x)") (auto simp add: lam.size)
+
+section {* Locally Nameless Terms *}
+
+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)"
+  by (induct xs arbitrary: n) (simp_all add: permute_pure)
+
+definition
+  trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
+where
+  "trans t l = f (%x l. lookup l 0 x) (%t1 t2 r1 r2 l. LNApp r1 r2) (%n t r l. LNLam r) t l"
+
+lemma
+ "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 (simp_all add: trans_def)
+apply (subst f.simps)
+apply (simp add: ln.fresh)
+apply (simp add: eqvt_def)
+apply auto
+apply (perm_simp, rule)
+apply (perm_simp, rule)
+apply (perm_simp, rule)
+apply (auto simp add: fresh_Pair)[1]
+apply (simp_all add: fresh_def supp_def permute_fun_def)[3]
+apply (simp add: eqvts permute_pure)
+done
+