--- a/Nominal/Ex/Lambda.thy	Wed May 19 11:29:42 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed May 19 12:29:08 2010 +0200
@@ -475,101 +475,61 @@
 (* Substitution *)
 
 definition new where
-  "new s = (THE x. \<forall>a \<in> s. x \<noteq> a)"
-
-term "let n = new {s, x} in b"
+  "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)"
 
 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"
+  subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<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 =
-    Lam_raw (new {s, y, x}) (subst_var_raw ((x \<leftrightarrow> new {s, y, x}) \<bullet> t) y s)"
+  "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))"
+| "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)"
+| "subst_raw (Lam_raw x t) y s =
+      Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))
+       (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom 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 fv_subst[simp]: "fv_lam_raw (subst_raw t y s) =
+  (if (atom y \<in> fv_lam_raw t) then fv_lam_raw s \<union> (fv_lam_raw t - {atom y}) else fv_lam_raw t)"
+  apply (induct t arbitrary: s)
+  apply (auto simp add: supp_at_base)[1]
+  apply (auto simp add: supp_at_base)[1]
+  apply (simp only: fv_lam_raw.simps)
+  apply simp
+  apply (rule conjI)
+  apply clarify
+  sorry
+
+thm supp_at_base
 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)"
+lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_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"
+lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw 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 c d
-    assume a: "alpha_lam_raw a b"
-    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 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
-
-fun
-  subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw"
-where
-  "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))"
-| "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)"
-| "subst_raw (Lam_raw x t) y s =
-     (if x = y then t else
-       (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))"
-(* termination/lifting fail with sth like:
-| "subst_raw (Lam_raw x t) y s =
-     (FRESH v. Lam_raw v (subst_raw (subst_var_raw t x v) y s))"
-*)
+  apply (rule_tac x="(name \<leftrightarrow> new (insert (atom d) (supp d)))" in exI)
+  apply (simp add: alphas)
+  oops
 
 quotient_definition
   subst ("_ [ _ ::= _ ]" [100,100,100] 100)
 where
   "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw"
 
-lemmas fv_rsp = quot_respect(10)[simplified,rulify]
+lemmas fv_rsp = quot_respect(10)[simplified]
 
 lemma subst_rsp_pre1:
   assumes a: "alpha_lam_raw a b"
@@ -581,14 +541,21 @@
   apply (simp only: alphas)
   apply clarify
   apply (simp only: subst_raw.simps)
+  apply (rule alpha_lam_raw.intros)
+  apply (simp only: alphas)
   sorry
 
 lemma subst_rsp_pre2:
   assumes a: "alpha_lam_raw a b"
   shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)"
+  using a
+  apply (induct c arbitrary: a b y)
+  apply (simp add: equivp_reflp[OF lam_equivp])
+  apply (simp add: alpha_lam_raw.intros)
+  apply simp
+  apply (rule alpha_lam_raw.intros)
   sorry
 
-(* The below is definitely not true... *)
 lemma [quot_respect]:
   "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw"
   proof (intro fun_relI, simp)
@@ -603,8 +570,14 @@
   qed
 
 lemma simp3:
-  "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> subst_raw (Lam_raw x t) y s = Lam_raw x (subst_raw t y s)"
-  by simp
+  "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> alpha_lam_raw (subst_raw (Lam_raw x t) y s) (Lam_raw x (subst_raw t y s))"
+  apply simp
+  apply (rule alpha_lam_raw.intros)
+  apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) -
+                    {atom x})))" in exI)
+  apply (simp only: alphas)
+  apply simp
+  sorry
 
 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars]
   simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars]