equal
deleted
inserted
replaced
365 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
365 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
366 apply(simp add: fresh_def) |
366 apply(simp add: fresh_def) |
367 apply(simp add: var_supp1) |
367 apply(simp add: var_supp1) |
368 done |
368 done |
369 |
369 |
|
370 (* TODO: make a proper definition of substitution *) |
|
371 definition |
|
372 subs :: "rlam \<Rightarrow> (name \<times> rlam) \<Rightarrow> rlam" ("_ \<guillemotleft>\<guillemotright> _" [70, 71] 70) |
|
373 where |
|
374 "x \<guillemotleft>\<guillemotright> S \<equiv> x" |
|
375 |
|
376 lemma " |
|
377 \<exists>hom\<in>Respects(alpha ===> op =). ( |
|
378 (\<forall>x. hom (rVar x) = var x) \<and> |
|
379 (\<forall>l r. hom (rApp l r) = app (hom l) (hom r)) \<and> |
|
380 (\<forall>x a. hom (rLam a x) = lam (\<lambda>y. hom (a \<guillemotleft>\<guillemotright> (x, rVar y)) (\<lambda>y. a \<guillemotleft>\<guillemotright> (x, rVar y)))) |
|
381 )" |
|
382 |
370 end |
383 end |