equal
deleted
inserted
replaced
359 apply(simp add: fresh_def) |
359 apply(simp add: fresh_def) |
360 apply(simp add: var_supp1) |
360 apply(simp add: var_supp1) |
361 done |
361 done |
362 |
362 |
363 |
363 |
364 lemma " |
364 lemma hom: " |
|
365 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
|
366 \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
365 \<exists>hom \<in> Respects(alpha ===> op =). ( |
367 \<exists>hom \<in> Respects(alpha ===> op =). ( |
366 (\<forall>x. hom (rVar x) = f_var x) \<and> |
368 (\<forall>x. hom (rVar x) = f_var x) \<and> |
367 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
369 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
368 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
370 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
369 )" |
371 )" |
|
372 sorry |
|
373 |
|
374 lemma hom': |
|
375 "\<forall>f_lam. \<forall>f_app. \<exists>hom. ( |
|
376 (\<forall>x. hom (Var x) = f_var x) \<and> |
|
377 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
|
378 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
|
379 )" |
|
380 apply (lifting hom) |
370 |
381 |
371 end |
382 end |