equal
deleted
inserted
replaced
642 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
642 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
643 apply(induct xs arbitrary: n) |
643 apply(induct xs arbitrary: n) |
644 apply(simp_all add: permute_pure) |
644 apply(simp_all add: permute_pure) |
645 done |
645 done |
646 |
646 |
|
647 (* function that evaluates a lambda term *) |
|
648 nominal_primrec |
|
649 eval :: "lam \<Rightarrow> lam" and |
|
650 app :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
|
651 where |
|
652 "eval (Var x) = Var x" |
|
653 | "eval (Lam [x].t) = Lam [x].(eval t)" |
|
654 | "eval (App t1 t2) = sub (eval t1) (eval t2)" |
|
655 | "app (Var x) t2 = App (Var x) t2" |
|
656 | "app (App t0 t1) t2 = App (App t0 t1) t2" |
|
657 | "app (Lam [x].t1) t2 = eval (t1[x::= t2])" |
|
658 apply(simp add: eval_app_graph_def eqvt_def) |
|
659 apply(perm_simp) |
|
660 apply(simp) |
|
661 apply(rule TrueI) |
|
662 defer |
|
663 apply(simp_all) |
|
664 defer |
|
665 oops (* can this be defined ? *) |
647 |
666 |
648 text {* tests of functions containing if and case *} |
667 text {* tests of functions containing if and case *} |
649 |
668 |
650 consts P :: "lam \<Rightarrow> bool" |
669 consts P :: "lam \<Rightarrow> bool" |
651 |
670 |
749 |
768 |
750 |
769 |
751 |
770 |
752 |
771 |
753 |
772 |
|
773 |
|
774 |
|
775 |
754 end |
776 end |
755 |
777 |
756 |
778 |
757 |
779 |