equal
deleted
inserted
replaced
506 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
506 "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" |
507 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
507 | "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" |
508 | "subst_raw (Lam_raw x t) y s = |
508 | "subst_raw (Lam_raw x t) y s = |
509 (if x = y then t else |
509 (if x = y then t else |
510 (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))" |
510 (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))" |
|
511 (* termination/lifting fail with sth like: |
|
512 | "subst_raw (Lam_raw x t) y s = |
|
513 (FRESH v. Lam_raw v (subst_raw (subst_var_raw t x v) y s))" |
|
514 *) |
511 |
515 |
512 quotient_definition |
516 quotient_definition |
513 subst ("_ [ _ ::= _ ]" [100,100,100] 100) |
517 subst ("_ [ _ ::= _ ]" [100,100,100] 100) |
514 where |
518 where |
515 "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw" |
519 "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw" |