equal
deleted
inserted
replaced
219 apply(simp add: fresh_star_def fresh_Unit) |
219 apply(simp add: fresh_star_def fresh_Unit) |
220 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
220 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
221 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
221 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
222 done |
222 done |
223 |
223 |
224 termination |
224 termination by lexicographic_order |
225 by lexicographic_order |
|
226 |
225 |
227 text {* a small test lemma *} |
226 text {* a small test lemma *} |
228 lemma shows "supp t = set (frees_lst t)" |
227 lemma shows "supp t = set (frees_lst t)" |
229 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
228 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
230 |
229 |
478 apply(auto)[1] |
477 apply(auto)[1] |
479 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
478 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
480 apply (auto simp add: fresh_star_def)[3] |
479 apply (auto simp add: fresh_star_def)[3] |
481 apply(simp_all) |
480 apply(simp_all) |
482 apply(erule conjE)+ |
481 apply(erule conjE)+ |
483 thm Abs_lst1_fcb2' |
|
484 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
482 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
485 apply (simp add: fresh_star_def) |
483 apply (simp add: fresh_star_def) |
486 apply (simp add: fresh_star_def) |
484 apply (simp add: fresh_star_def) |
487 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
485 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
488 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
486 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
553 nominal_datatype db = |
551 nominal_datatype db = |
554 DBVar nat |
552 DBVar nat |
555 | DBApp db db |
553 | DBApp db db |
556 | DBLam db |
554 | DBLam db |
557 |
555 |
558 lemma option_map_eqvt[eqvt]: |
|
559 "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
|
560 by (cases x) (simp_all, simp add: permute_fun_app_eq) |
|
561 |
|
562 lemma option_bind_eqvt[eqvt]: |
|
563 shows "(p \<bullet> (Option.map f c)) = (Option.map (p \<bullet> f) (p \<bullet> c))" |
|
564 by (cases c) (simp_all, simp add: permute_fun_app_eq) |
|
565 |
|
566 instance db :: pure |
556 instance db :: pure |
567 apply default |
557 apply default |
568 apply (induct_tac x rule: db.induct) |
558 apply (induct_tac x rule: db.induct) |
569 apply (simp_all add: permute_pure) |
559 apply (simp_all add: permute_pure) |
570 done |
560 done |
580 | "vindex (h # t) v n = (if v = h then (Some (DBVar n)) else (vindex t v (Suc n)))" |
570 | "vindex (h # t) v n = (if v = h then (Some (DBVar n)) else (vindex t v (Suc n)))" |
581 |
571 |
582 lemma vindex_eqvt[eqvt]: |
572 lemma vindex_eqvt[eqvt]: |
583 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
573 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
584 by (induct l arbitrary: n) (simp_all add: permute_pure) |
574 by (induct l arbitrary: n) (simp_all add: permute_pure) |
585 |
|
586 |
|
587 |
575 |
588 nominal_primrec |
576 nominal_primrec |
589 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
577 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
590 where |
578 where |
591 "transdb (Var x) l = vindex l x 0" |
579 "transdb (Var x) l = vindex l x 0" |
626 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
614 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
627 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
615 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
628 using a by simp |
616 using a by simp |
629 |
617 |
630 lemma supp_subst: |
618 lemma supp_subst: |
631 "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s" |
619 shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s" |
632 by (induct t x s rule: subst.induct) (auto simp add: lam.supp) |
620 by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base) |
633 |
621 |
634 lemma var_fresh_subst: |
622 lemma var_fresh_subst: |
635 "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])" |
623 "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])" |
636 by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base) |
624 by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base) |
637 |
625 |