475 (* Substitution *)

   476 fun

   477   subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw"

   478 where

   479   "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))"

   480 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)"

   481 | "subst_raw (Lam_raw x t) y s =

   482      (if x = y then t else

   483        (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))"

   484 

   485 quotient_definition

   486   subst ("_ [ _ ::= _ ]" [100,100,100] 100)

   487 where

   488   "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw"

   489 

   490 lemmas fv_rsp = quot_respect(10)[simplified,rulify]

   491 

   492 lemma subst_rsp_pre1:

   493   assumes a: "alpha_lam_raw a b"

   494   shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)"

   495   using a

   496   apply (induct a b arbitrary: c y rule: alpha_lam_raw.induct)

   497   apply (simp add: equivp_reflp[OF lam_equivp])

   498   apply (simp add: alpha_lam_raw.intros)

   499   apply (simp only: alphas)

   500   apply clarify

   501   apply (simp only: subst_raw.simps)

   502   sorry

   503 

   504 lemma subst_rsp_pre2:

   505   assumes a: "alpha_lam_raw a b"

   506   shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)"

   507   sorry

   508 

   509 (* The below is definitely not true... *)

   510 lemma [quot_respect]:

   511   "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw"

   512   proof (intro fun_relI, simp)

   513     fix a b c d :: lam_raw

   514     fix y :: name

   515     assume a: "alpha_lam_raw a b"

   516     assume b: "alpha_lam_raw c d"

   517     have c: "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" using subst_rsp_pre1 a by simp

   518     then have d: "alpha_lam_raw (subst_raw b y c) (subst_raw b y d)" using subst_rsp_pre2 b by simp

   519     show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)"

   520       using c d equivp_transp[OF lam_equivp] by blast

   521   qed

   522 

   523 lemma simp3:

   524   "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> Lam_raw x (subst_raw t y s) = Lam_raw x (subst_raw t y s)"

   525   by simp

   526 

   527 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars]

   528   simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars]