357 nominal_datatype db = |
357 nominal_datatype db = |
358 DBVar nat |
358 DBVar nat |
359 | DBApp db db |
359 | DBApp db db |
360 | DBLam db |
360 | DBLam db |
361 |
361 |
362 fun dbapp_in where |
362 lemma option_map_eqvt[eqvt]: |
363 "dbapp_in None _ = None" |
363 "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
364 | "dbapp_in (Some _ ) None = None" |
364 by (cases x) (simp_all, simp add: permute_fun_app_eq) |
365 | "dbapp_in (Some x) (Some y) = Some (DBApp x y)" |
365 |
366 |
366 lemma option_bind_eqvt[eqvt]: |
367 fun dblam_in where |
367 shows "(p \<bullet> (Option.map f c)) = (Option.map (p \<bullet> f) (p \<bullet> c))" |
368 "dblam_in None = None" |
368 by (cases c) (simp_all, simp add: permute_fun_app_eq) |
369 | "dblam_in (Some x) = Some (DBLam x)" |
|
370 |
|
371 lemma db_in_eqvt[eqvt]: |
|
372 "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)" |
|
373 "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)" |
|
374 apply (case_tac [!] x) |
|
375 apply (simp_all add: eqvts) |
|
376 apply (case_tac y) |
|
377 apply (simp_all add: eqvts) |
|
378 done |
|
379 |
369 |
380 instance db :: pure |
370 instance db :: pure |
381 apply default |
371 apply default |
382 apply (induct_tac x rule: db.induct) |
372 apply (induct_tac x rule: db.induct) |
383 apply (simp_all add: permute_pure) |
373 apply (simp_all add: permute_pure) |
399 |
389 |
400 nominal_primrec |
390 nominal_primrec |
401 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
391 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
402 where |
392 where |
403 "transdb (Var x) l = vindex l x 0" |
393 "transdb (Var x) l = vindex l x 0" |
404 | "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)" |
394 | "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
405 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))" |
395 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
406 unfolding eqvt_def transdb_graph_def |
396 unfolding eqvt_def transdb_graph_def |
407 apply (rule, perm_simp, rule) |
397 apply (rule, perm_simp, rule) |
408 apply(rule TrueI) |
398 apply(rule TrueI) |
409 apply (case_tac x) |
399 apply (case_tac x) |
410 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
400 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
411 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
401 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
412 apply(simp_all) |
402 apply(simp_all) |
413 apply(erule conjE) |
403 apply(elim conjE) |
414 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
404 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
415 apply (simp add: pure_fresh) |
405 apply (simp add: pure_fresh) |
416 apply(simp add: fresh_star_def fresh_at_list) |
406 apply(simp add: fresh_star_def fresh_at_list) |
417 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) |
407 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ |
418 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) |
|
419 done |
408 done |
420 |
409 |
421 termination |
410 termination |
422 by lexicographic_order |
411 by lexicographic_order |
423 |
412 |
424 lemma transdb_eqvt[eqvt]: |
413 lemma transdb_eqvt[eqvt]: |
425 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
414 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
426 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
415 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
427 apply (simp add: vindex_eqvt) |
416 apply (simp add: vindex_eqvt) |
428 apply (simp_all add: permute_pure) |
417 apply (simp_all add: permute_pure) |
429 apply (simp add: fresh_at_list) |
418 apply (simp add: fresh_at_list) |
430 apply (subst transdb.simps) |
419 apply (subst transdb.simps) |
431 apply (simp add: fresh_at_list[symmetric]) |
420 apply (simp add: fresh_at_list[symmetric]) |
436 lemma db_trans_test: |
425 lemma db_trans_test: |
437 assumes a: "y \<noteq> x" |
426 assumes a: "y \<noteq> x" |
438 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
427 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
439 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
428 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
440 using a by simp |
429 using a by simp |
|
430 |
441 |
431 |
442 abbreviation |
432 abbreviation |
443 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
433 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
444 where |
434 where |
445 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
435 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
608 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
598 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
609 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
599 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))" |
610 unfolding eqvt_def Z_graph_def |
600 unfolding eqvt_def Z_graph_def |
611 apply (rule, perm_simp, rule) |
601 apply (rule, perm_simp, rule) |
612 oops |
602 oops |
613 |
|
614 text {* tests of functions containing if and case *} |
|
615 |
|
616 consts P :: "lam \<Rightarrow> bool" |
|
617 |
|
618 nominal_primrec |
|
619 A :: "lam => lam" |
|
620 where |
|
621 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
622 | "A (Var x) = (Var x)" |
|
623 | "A (App M N) = (if True then M else A N)" |
|
624 oops |
|
625 |
|
626 nominal_primrec |
|
627 C :: "lam => lam" |
|
628 where |
|
629 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
630 | "C (Var x) = (Var x)" |
|
631 | "C (App M N) = (if True then M else C N)" |
|
632 oops |
|
633 |
|
634 nominal_primrec |
|
635 A :: "lam => lam" |
|
636 where |
|
637 "A (Lam [x].M) = (Lam [x].M)" |
|
638 | "A (Var x) = (Var x)" |
|
639 | "A (App M N) = (if True then M else A N)" |
|
640 oops |
|
641 |
|
642 nominal_primrec |
|
643 B :: "lam => lam" |
|
644 where |
|
645 "B (Lam [x].M) = (Lam [x].M)" |
|
646 | "B (Var x) = (Var x)" |
|
647 | "B (App M N) = (if True then M else (B N))" |
|
648 unfolding eqvt_def |
|
649 unfolding B_graph_def |
|
650 apply(perm_simp) |
|
651 apply(rule allI) |
|
652 apply(rule refl) |
|
653 oops |
|
654 |
|
655 |
603 |
656 lemma test: |
604 lemma test: |
657 assumes "t = s" |
605 assumes "t = s" |
658 and "supp p \<sharp>* t" "supp p \<sharp>* x" |
606 and "supp p \<sharp>* t" "supp p \<sharp>* x" |
659 and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y" |
607 and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y" |
718 apply(simp del: Product_Type.prod.inject) |
666 apply(simp del: Product_Type.prod.inject) |
719 sorry |
667 sorry |
720 |
668 |
721 termination by lexicographic_order |
669 termination by lexicographic_order |
722 |
670 |
|
671 lemma abs_same_binder: |
|
672 fixes t ta s sa :: "_ :: fs" |
|
673 assumes "sort_of (atom x) = sort_of (atom y)" |
|
674 shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa |
|
675 \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)" |
|
676 by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair) |
|
677 |
|
678 nominal_primrec |
|
679 aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" |
|
680 where |
|
681 "aux2 (Var x) (Var y) = (x = y)" |
|
682 | "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)" |
|
683 | "aux2 (Var x) (App t1 t2) = False" |
|
684 | "aux2 (Var x) (Lam [y].t) = False" |
|
685 | "aux2 (App t1 t2) (Var x) = False" |
|
686 | "aux2 (App t1 t2) (Lam [x].t) = False" |
|
687 | "aux2 (Lam [x].t) (Var y) = False" |
|
688 | "aux2 (Lam [x].t) (App t1 t2) = False" |
|
689 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s" |
|
690 apply(simp add: eqvt_def aux2_graph_def) |
|
691 apply(rule, perm_simp, rule, rule) |
|
692 apply(case_tac x) |
|
693 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
|
694 apply(rule_tac y="b" in lam.exhaust) |
|
695 apply(auto)[3] |
|
696 apply(rule_tac y="b" in lam.exhaust) |
|
697 apply(auto)[3] |
|
698 apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust) |
|
699 apply(auto)[3] |
|
700 apply(drule_tac x="name" in meta_spec) |
|
701 apply(drule_tac x="name" in meta_spec) |
|
702 apply(drule_tac x="lam" in meta_spec) |
|
703 apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec) |
|
704 apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def) |
|
705 apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2)) |
|
706 apply simp_all |
|
707 apply (simp add: abs_same_binder) |
|
708 apply (erule_tac c="()" in Abs_lst1_fcb2) |
|
709 apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def) |
|
710 done |
|
711 |
|
712 text {* tests of functions containing if and case *} |
|
713 |
|
714 consts P :: "lam \<Rightarrow> bool" |
|
715 |
|
716 nominal_primrec |
|
717 A :: "lam => lam" |
|
718 where |
|
719 "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" |
|
720 | "A (Var x) = (Var x)" |
|
721 | "A (App M N) = (if True then M else A N)" |
|
722 oops |
|
723 |
|
724 nominal_primrec |
|
725 C :: "lam => lam" |
|
726 where |
|
727 "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" |
|
728 | "C (Var x) = (Var x)" |
|
729 | "C (App M N) = (if True then M else C N)" |
|
730 oops |
|
731 |
|
732 nominal_primrec |
|
733 A :: "lam => lam" |
|
734 where |
|
735 "A (Lam [x].M) = (Lam [x].M)" |
|
736 | "A (Var x) = (Var x)" |
|
737 | "A (App M N) = (if True then M else A N)" |
|
738 oops |
|
739 |
|
740 nominal_primrec |
|
741 B :: "lam => lam" |
|
742 where |
|
743 "B (Lam [x].M) = (Lam [x].M)" |
|
744 | "B (Var x) = (Var x)" |
|
745 | "B (App M N) = (if True then M else (B N))" |
|
746 unfolding eqvt_def |
|
747 unfolding B_graph_def |
|
748 apply(perm_simp) |
|
749 apply(rule allI) |
|
750 apply(rule refl) |
|
751 oops |
|
752 |
723 end |
753 end |
724 |
754 |
725 |
755 |
726 |
756 |