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 |
|
472 lemma hom: |
|
473 "\<exists>hom\<in>Respects (alpha ===> op =). |
|
474 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
|
475 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
|
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(rule_tac x="rlam_rec f_var f_app XX" in bexI) |
|
478 apply(rule conjI) |
|
479 apply(simp) |
|
480 apply(rule conjI) |
|
481 apply(simp) |
|
482 apply(simp) |
|
483 sorry |
|
484 |
|
485 function |
470 function |
486 term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow> |
471 term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow> |
487 (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> |
472 (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> |
488 ((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a" |
473 ((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a" |
489 where |
474 where |
490 "term1_hom var app abs' (rVar x) = (var x)" |
475 "term1_hom var app abs' (rVar x) = (var x)" |
491 | "term1_hom var app abs' (rApp t u) = |
476 | "term1_hom var app abs' (rApp t u) = |
492 app t u (term1_hom var app abs' t) (term1_hom var app abs' u)" |
477 app t u (term1_hom var app abs' t) (term1_hom var app abs' u)" |
508 apply - |
493 apply - |
509 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
494 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
510 apply(auto simp add: pi_size) |
495 apply(auto simp add: pi_size) |
511 done |
496 done |
512 |
497 |
513 lemma hom_res: " |
498 lemma term1_hom_rsp: |
|
499 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
|
500 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
|
501 sorry |
|
502 |
|
503 lemma hom: " |
514 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
504 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
515 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
505 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
516 \<exists>hom\<in>Respects (alpha ===> op =). |
506 \<exists>hom\<in>Respects (alpha ===> op =). |
517 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
507 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
518 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
508 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
519 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
509 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
520 apply(rule allI) |
510 apply(rule allI) |
521 apply(rule ballI)+ |
511 apply(rule ballI)+ |
522 apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI) |
512 apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI) |
523 apply(rule conjI) |
513 apply(simp_all) |
524 (* apply(simp add: term1_hom.psimps) *) |
514 apply(simp only: in_respects) |
525 prefer 2 |
515 apply(rule term1_hom_rsp) |
526 apply(rule conjI) |
516 apply(assumption)+ |
527 (* apply(simp add: term1_hom.psimps) *) |
517 done |
528 sorry |
|
529 |
518 |
530 lemma hom': |
519 lemma hom': |
531 "\<exists>hom. |
520 "\<exists>hom. |
532 ((\<forall>x. hom (Var x) = f_var x) \<and> |
521 ((\<forall>x. hom (Var x) = f_var x) \<and> |
533 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
522 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
534 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
523 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
535 apply (lifting hom_res) |
524 apply (lifting hom) |
536 done |
525 done |
537 |
526 |
538 (* test test |
527 (* test test |
539 lemma raw_hom_correct: |
528 lemma raw_hom_correct: |
540 assumes f1: "f_var \<in> Respects (op= ===> op=)" |
529 assumes f1: "f_var \<in> Respects (op= ===> op=)" |