465 apply(clarify) |
465 apply(clarify) |
466 apply(simp) |
466 apply(simp) |
467 (* probably true *) |
467 (* probably true *) |
468 sorry |
468 sorry |
469 |
469 |
|
470 |
|
471 |
470 lemma hom: |
472 lemma hom: |
471 "\<exists>hom\<in>Respects (alpha ===> op =). |
473 "\<exists>hom\<in>Respects (alpha ===> op =). |
472 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
474 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
473 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
475 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
474 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
476 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
477 apply(simp) |
479 apply(simp) |
478 apply(rule conjI) |
480 apply(rule conjI) |
479 apply(simp) |
481 apply(simp) |
480 apply(simp) |
482 apply(simp) |
481 sorry |
483 sorry |
|
484 |
|
485 function |
|
486 term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow> (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a" |
|
487 where |
|
488 "term1_hom var app abs' (rVar x) = (var x)" |
|
489 | "term1_hom var app abs' (rApp t u) = |
|
490 app t u (term1_hom var app abs' t) (term1_hom var app abs' u)" |
|
491 | "term1_hom var app abs' (rLam x u) = |
|
492 abs' (\<lambda>y. [(x, y)] \<bullet> u) (\<lambda>y. term1_hom var app abs' ([(x, y)] \<bullet> u))" |
|
493 sorry |
|
494 |
|
495 print_theorems |
482 |
496 |
483 lemma hom_res: " |
497 lemma hom_res: " |
484 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
498 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
485 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
499 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
486 \<exists>hom\<in>Respects (alpha ===> op =). |
500 \<exists>hom\<in>Respects (alpha ===> op =). |
487 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
501 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
488 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
502 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
489 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
503 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
490 apply(rule allI) |
504 apply(rule allI) |
491 apply(rule ballI)+ |
505 apply(rule ballI)+ |
492 apply(rule_tac x="rlam_rec f_var f_app XX" in bexI) |
506 apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI) |
493 apply(rule conjI) |
507 apply(rule conjI) |
494 apply(simp) |
508 (* apply(simp add: term1_hom.psimps) *) |
495 apply(rule conjI) |
509 prefer 2 |
496 apply(simp) |
510 apply(rule conjI) |
497 apply(simp_all only: in_respects) |
511 (* apply(simp add: term1_hom.psimps) *) |
498 sorry |
512 sorry |
499 |
513 |
500 lemma hom': |
514 lemma hom': |
501 "\<exists>hom. |
515 "\<exists>hom. |
502 ((\<forall>x. hom (Var x) = f_var x) \<and> |
516 ((\<forall>x. hom (Var x) = f_var x) \<and> |