358 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
358 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
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 (* lemma hom_reg: *) |
363 |
364 |
364 lemma hom: " |
365 lemma hom: " |
365 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
366 \<exists>hom\<in>Respects (alpha ===> op =). ( |
366 \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
|
367 \<exists>hom \<in> Respects(alpha ===> op =). ( |
|
368 (\<forall>x. hom (rVar x) = f_var x) \<and> |
367 (\<forall>x. hom (rVar x) = f_var x) \<and> |
369 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
368 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
370 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
369 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
371 )" |
370 )" |
372 sorry |
371 sorry |
373 |
372 |
|
373 lemma hom_reg:" |
|
374 (\<exists>hom\<in>Respects (alpha ===> op =). |
|
375 (\<forall>x. hom (rVar x) = f_var x) \<and> |
|
376 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
|
377 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa)))) \<longrightarrow> |
|
378 (\<exists>hom. |
|
379 (\<forall>x. hom (rVar x) = f_var x) \<and> |
|
380 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
|
381 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
|
382 by(regularize) |
|
383 |
|
384 thm impE[OF hom_reg] |
|
385 lemma hom_pre:" |
|
386 (\<exists>hom. |
|
387 (\<forall>x. hom (rVar x) = f_var x) \<and> |
|
388 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
|
389 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
|
390 apply (rule impE[OF hom_reg]) |
|
391 apply (rule hom) |
|
392 apply (assumption) |
|
393 done |
|
394 |
374 lemma hom': |
395 lemma hom': |
375 "\<forall>f_lam. \<forall>f_app. \<exists>hom. ( |
396 "\<exists>hom. ( |
376 (\<forall>x. hom (Var x) = f_var x) \<and> |
397 (\<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> |
398 (\<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))) |
399 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
379 )" |
400 )" |
380 (*apply (lifting hom)*) |
401 apply (lifting hom) |
381 sorry |
402 done |
382 |
403 |
383 thm rlam.recs |
404 thm bex_reg_eqv_range[OF identity_equivp, of "alpha"] |
|
405 |
384 |
406 |
385 end |
407 end |
|
408 |