481 apply(simp) |
481 apply(simp) |
482 apply(simp) |
482 apply(simp) |
483 sorry |
483 sorry |
484 |
484 |
485 function |
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" |
486 term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow> |
|
487 (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> |
|
488 ((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a" |
487 where |
489 where |
488 "term1_hom var app abs' (rVar x) = (var x)" |
490 "term1_hom var app abs' (rVar x) = (var x)" |
489 | "term1_hom var app abs' (rApp t u) = |
491 | "term1_hom var app abs' (rApp t u) = |
490 app t u (term1_hom var app abs' t) (term1_hom var app abs' u)" |
492 app t u (term1_hom var app abs' t) (term1_hom var app abs' u)" |
491 | "term1_hom var app abs' (rLam x u) = |
493 | "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))" |
494 abs' (\<lambda>y. [(x, y)] \<bullet> u) (\<lambda>y. term1_hom var app abs' ([(x, y)] \<bullet> u))" |
493 sorry |
495 apply(pat_completeness) |
494 |
496 apply(auto) |
495 print_theorems |
497 done |
|
498 |
|
499 lemma pi_size: |
|
500 fixes pi::"name prm" |
|
501 and t::"rlam" |
|
502 shows "size (pi \<bullet> t) = size t" |
|
503 apply(induct t) |
|
504 apply(auto) |
|
505 done |
|
506 |
|
507 termination term1_hom |
|
508 apply - |
|
509 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
|
510 apply(auto simp add: pi_size) |
|
511 done |
496 |
512 |
497 lemma hom_res: " |
513 lemma hom_res: " |
498 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
514 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
499 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
515 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
500 \<exists>hom\<in>Respects (alpha ===> op =). |
516 \<exists>hom\<in>Respects (alpha ===> op =). |