equal
deleted
inserted
replaced
559 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
559 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
560 apply (simp add: eqvt_def map_term_graph_def) |
560 apply (simp add: eqvt_def map_term_graph_def) |
561 apply (rule, perm_simp, rule) |
561 apply (rule, perm_simp, rule) |
562 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
562 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
563 apply auto |
563 apply auto |
564 apply (simp add: Abs1_eq_iff) |
564 apply (erule Abs1_eq_fdest) |
565 apply (auto) |
565 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
566 apply (simp add: eqvt_def permute_fun_app_eq) |
566 apply (simp add: eqvt_def permute_fun_app_eq) |
567 apply (drule supp_fun_app_eqvt) |
|
568 apply (simp add: fresh_def ) |
|
569 apply blast |
|
570 apply (simp add: eqvt_def permute_fun_app_eq) |
|
571 apply (drule supp_fun_app_eqvt) |
|
572 apply (simp add: fresh_def ) |
|
573 apply blast |
|
574 done |
567 done |
575 |
568 |
576 termination |
569 termination |
577 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
570 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
578 |
571 |
618 consts b :: name |
611 consts b :: name |
619 nominal_primrec |
612 nominal_primrec |
620 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
613 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
621 where |
614 where |
622 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
615 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
616 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
623 unfolding eqvt_def Z_graph_def |
617 unfolding eqvt_def Z_graph_def |
624 apply (rule, perm_simp, rule) |
618 apply (rule, perm_simp, rule) |
625 oops |
619 oops |
626 |
620 |
627 (* function tests *) |
621 (* function tests *) |
631 f :: "int list \<Rightarrow> int" |
625 f :: "int list \<Rightarrow> int" |
632 where |
626 where |
633 "f [] = 0" |
627 "f [] = 0" |
634 | "f [e] = e" |
628 | "f [e] = e" |
635 | "f (l @ m) = f l + f m" |
629 | "f (l @ m) = f l + f m" |
636 apply(simp_all) |
630 apply(simp_all) |
637 oops |
631 oops |
638 |
632 |
639 |
633 |
640 |
634 |
641 |
635 |