equal
deleted
inserted
replaced
529 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
529 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
530 apply (simp add: eqvt_def map_term_graph_def) |
530 apply (simp add: eqvt_def map_term_graph_def) |
531 apply (rule, perm_simp, rule) |
531 apply (rule, perm_simp, rule) |
532 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
532 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
533 apply auto |
533 apply auto |
534 apply (simp add: Abs1_eq_iff) |
534 apply (erule Abs1_eq_fdest) |
535 apply (auto) |
535 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
536 apply (simp add: eqvt_def permute_fun_app_eq) |
536 apply (simp add: eqvt_def permute_fun_app_eq) |
537 apply (drule supp_fun_app_eqvt) |
|
538 apply (simp add: fresh_def ) |
|
539 apply blast |
|
540 apply (simp add: eqvt_def permute_fun_app_eq) |
|
541 apply (drule supp_fun_app_eqvt) |
|
542 apply (simp add: fresh_def ) |
|
543 apply blast |
|
544 done |
537 done |
545 |
538 |
546 termination |
539 termination |
547 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
540 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
548 |
541 |
588 consts b :: name |
581 consts b :: name |
589 nominal_primrec |
582 nominal_primrec |
590 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
583 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
591 where |
584 where |
592 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
585 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
586 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
593 unfolding eqvt_def Z_graph_def |
587 unfolding eqvt_def Z_graph_def |
594 apply (rule, perm_simp, rule) |
588 apply (rule, perm_simp, rule) |
595 oops |
589 oops |
596 |
590 |
597 (* function tests *) |
591 (* function tests *) |
601 f :: "int list \<Rightarrow> int" |
595 f :: "int list \<Rightarrow> int" |
602 where |
596 where |
603 "f [] = 0" |
597 "f [] = 0" |
604 | "f [e] = e" |
598 | "f [e] = e" |
605 | "f (l @ m) = f l + f m" |
599 | "f (l @ m) = f l + f m" |
606 apply(simp_all) |
600 apply(simp_all) |
607 oops |
601 oops |
608 |
602 |
609 |
603 |
610 |
604 |
611 |
605 |