equal
deleted
inserted
replaced
539 oops |
539 oops |
540 |
540 |
541 nominal_primrec |
541 nominal_primrec |
542 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
542 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
543 where |
543 where |
544 "map_term f (Var x) = f (Var x)" |
|
545 | "map_term f (App t1 t2) = App (f t1) (f t2)" |
|
546 | "map_term f (Lam [x].t) = Lam [x].(f t)" |
|
547 unfolding eqvt_def map_term_graph_def |
|
548 apply (rule, perm_simp, rule) |
|
549 apply (case_tac x, case_tac b rule: lam.exhaust) |
|
550 apply auto |
|
551 (*apply (erule Abs1_eq_fdest)*) |
|
552 oops |
|
553 |
|
554 nominal_primrec |
|
555 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
|
556 where |
|
557 "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)" |
544 "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)" |
558 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)" |
545 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)" |
559 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)" |
546 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)" |
560 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
547 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
561 apply (simp add: eqvt_def map_term_graph_def) |
548 apply (simp add: eqvt_def map_term_graph_def) |
613 where |
600 where |
614 "CPS (Var x) k = Var x" |
601 "CPS (Var x) k = Var x" |
615 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
602 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
616 oops |
603 oops |
617 |
604 |
|
605 (* Problem: nominal_primrec generates non-quantified free variable "x" *) |
|
606 consts b :: name |
|
607 nominal_primrec |
|
608 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
609 where |
|
610 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
611 unfolding eqvt_def Z_graph_def |
|
612 apply (rule, perm_simp, rule) |
|
613 prefer 2 |
|
614 ML_prf {* prop_of (hd (#prems (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))))) *} |
|
615 oops |
618 |
616 |
619 (* function tests *) |
617 (* function tests *) |
620 |
618 |
621 (* similar problem with function package *) |
619 (* similar problem with function package *) |
622 function |
620 function |