--- 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