616 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
616 shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
617 apply(induct xs arbitrary: n) |
617 apply(induct xs arbitrary: n) |
618 apply(simp_all add: permute_pure) |
618 apply(simp_all add: permute_pure) |
619 done |
619 done |
620 |
620 |
|
621 lemma supp_subst: |
|
622 "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s" |
|
623 by (induct t x s rule: subst.induct) (auto simp add: lam.supp) |
|
624 |
|
625 lemma var_fresh_subst: |
|
626 "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])" |
|
627 by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base) |
|
628 |
621 (* function that evaluates a lambda term *) |
629 (* function that evaluates a lambda term *) |
622 nominal_primrec |
630 nominal_primrec |
623 eval :: "lam \<Rightarrow> lam" and |
631 eval :: "lam \<Rightarrow> lam" and |
624 app :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
632 app :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
625 where |
633 where |
626 "eval (Var x) = Var x" |
634 "eval (Var x) = Var x" |
627 | "eval (Lam [x].t) = Lam [x].(eval t)" |
635 | "eval (Lam [x].t) = Lam [x].(eval t)" |
628 | "eval (App t1 t2) = sub (eval t1) (eval t2)" |
636 | "eval (App t1 t2) = sub (eval t1) (eval t2)" |
629 | "app (Var x) t2 = App (Var x) t2" |
637 | "app (Var x) t2 = App (Var x) t2" |
630 | "app (App t0 t1) t2 = App (App t0 t1) t2" |
638 | "app (App t0 t1) t2 = App (App t0 t1) t2" |
631 | "app (Lam [x].t1) t2 = eval (t1[x::= t2])" |
639 | "atom x \<sharp> t2 \<Longrightarrow> app (Lam [x].t1) t2 = eval (t1[x::= t2])" |
632 apply(simp add: eval_app_graph_def eqvt_def) |
640 apply(simp add: eval_app_graph_def eqvt_def) |
633 apply(perm_simp) |
641 apply(rule, perm_simp, rule) |
634 apply(simp) |
|
635 apply(rule TrueI) |
642 apply(rule TrueI) |
|
643 apply (case_tac x) |
|
644 apply (case_tac a rule: lam.exhaust) |
|
645 apply simp_all[3] |
|
646 apply blast |
|
647 apply (case_tac b) |
|
648 apply (rule_tac y="a" and c="ba" in lam.strong_exhaust) |
|
649 apply simp_all[3] |
|
650 apply blast |
|
651 apply blast |
|
652 apply (simp add: Abs1_eq_iff fresh_star_def) |
|
653 apply(simp_all) |
|
654 apply(erule Abs1_eq_fdest) |
|
655 apply (simp add: Abs_fresh_iff) |
|
656 apply (simp add: Abs_fresh_iff) |
|
657 apply (erule fresh_eqvt_at) |
|
658 apply (simp add: finite_supp) |
|
659 apply (simp add: fresh_Inl) |
|
660 apply (simp add: eqvt_at_def) |
|
661 apply simp |
636 defer |
662 defer |
637 apply(simp_all) |
663 apply clarify |
638 defer |
664 apply(erule Abs1_eq_fdest) |
|
665 apply (erule fresh_eqvt_at) |
|
666 apply (simp add: finite_supp) |
|
667 apply (simp add: fresh_Inl var_fresh_subst) |
|
668 apply (erule fresh_eqvt_at) |
|
669 apply (simp add: finite_supp) |
|
670 apply (simp add: fresh_Inl) |
|
671 apply (simp add: fresh_def) |
|
672 using supp_subst apply blast |
|
673 apply (simp add: eqvt_at_def subst_eqvt) |
|
674 apply (subst swap_fresh_fresh) |
|
675 apply assumption+ |
|
676 apply rule |
|
677 apply simp |
639 oops (* can this be defined ? *) |
678 oops (* can this be defined ? *) |
640 |
679 |
641 text {* tests of functions containing if and case *} |
680 text {* tests of functions containing if and case *} |
642 |
681 |
643 consts P :: "lam \<Rightarrow> bool" |
682 consts P :: "lam \<Rightarrow> bool" |