--- a/Nominal/Ex/Lambda.thy	Tue May 18 17:56:41 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed May 19 11:29:42 2010 +0200
@@ -474,29 +474,80 @@
 
 (* Substitution *)
 
-fun
+definition new where
+  "new s = (THE x. \<forall>a \<in> s. x \<noteq> a)"
+
+term "let n = new {s, x} in b"
+
+lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t"
+  by (induct t) simp_all
+
+function
   subst_var_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> name \<Rightarrow> lam_raw"
 where
   "subst_var_raw (Var_raw x) y s = (if x=y then (Var_raw s) else (Var_raw x))"
 | "subst_var_raw (App_raw l r) y s = App_raw (subst_var_raw l y s) (subst_var_raw r y s)"
 | "subst_var_raw (Lam_raw x t) y s =
-     (if x = y then Lam_raw x t else Lam_raw x (subst_var_raw t y s))"
+    Lam_raw (new {s, y, x}) (subst_var_raw ((x \<leftrightarrow> new {s, y, x}) \<bullet> t) y s)"
+by (pat_completeness, auto)
+termination
+  apply (relation "measure (\<lambda>(t, y, s). (size t))")
+  apply (auto simp add: size_no_change)
+  done
+
+lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)"
+  sorry
+
+lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_var_raw t y s) = subst_var_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)"
+  apply (induct t arbitrary: p y s)
+  apply simp_all
+  apply(perm_simp)
+  apply simp
+  sorry
+
+lemma subst_id: "alpha_lam_raw (subst_var_raw x d d) x"
+  apply (induct x arbitrary: d)
+  apply (simp_all add: alpha_lam_raw.intros)
+  apply (rule alpha_lam_raw.intros)
+  apply (rule_tac x="((new {d, name}) \<leftrightarrow> name)" in exI)
+  
+  apply (rule_tac s="subst_var_raw ((name \<leftrightarrow> n) \<bullet> x) d d" and
+                  t="(name \<leftrightarrow> n) \<bullet> (subst_var_raw x ((name \<leftrightarrow> n) \<bullet> d) ((name \<leftrightarrow> n) \<bullet> d))" in subst)
+  sorry
 
 (* Should be true? *)
 lemma "(alpha_lam_raw ===> op = ===> op = ===> alpha_lam_raw) subst_var_raw subst_var_raw"
   proof (intro fun_relI, (simp, clarify))
-    fix a b ba bb
+    fix a b c d
     assume a: "alpha_lam_raw a b"
-    show "alpha_lam_raw (subst_var_raw a ba bb) (subst_var_raw b ba bb)" using a
-      apply (induct a b rule: alpha_lam_raw.induct)
+    show "alpha_lam_raw (subst_var_raw a c d) (subst_var_raw b c d)" using a
+      apply (induct a b arbitrary: c d rule: alpha_lam_raw.induct)
       apply (simp add: equivp_reflp[OF lam_equivp])
       apply (simp add: alpha_lam_raw.intros)
-      apply auto
-      apply (rule_tac[!] alpha_lam_raw.intros)
-      apply (rule_tac[!] x="p" in exI) (* Need to do better *)
-      apply (simp_all add: alphas)
+      apply clarify
+(*      apply (case_tac "c = d")
+      apply clarify
+      apply (simp only: subst_id)
+      apply (rule alpha_lam_raw.intros)
+      apply (rule_tac x="p" in exI)
+      apply (simp add: alphas)
+      apply clarify
+      apply simp*)
+      apply (rename_tac x l y r c d p)
+      apply simp
+      unfolding Let_def
+      apply (rule alpha_lam_raw.intros)
+      apply (simp add: alphas)
       apply clarify
       apply simp
+      apply (rule conjI)
+      defer (* The fv one looks ok *)
+      apply (rule_tac x="p + (x \<leftrightarrow> new {d, c, x}) + (y \<leftrightarrow> new {d, c, y})" in exI)
+      apply (rule conjI)
+      defer (* should do sth like subst fresh_star_permute_iff[symmetric] *)
+      apply (simp only: eqvts)
+      apply simp
+      apply clarify
       sorry
     qed