# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274195874 -7200
# Node ID ce00205e07abeedaabcf5af7c4286faabdbf825e
# Parent  1785a111c2b674b0b6a6fca984d5641b81a530e0
Single variable substitution

diff -r 1785a111c2b6 -r ce00205e07ab Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 18 17:06:21 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 18 17:17:54 2010 +0200
@@ -473,6 +473,33 @@
 *)
 
 (* Substitution *)
+
+fun
+  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))"
+
+(* 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
+    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)
+      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 simp
+      sorry
+    qed
+
 fun
   subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw"
 where