468 nominal_datatype db = |
468 nominal_datatype db = |
469 DBVar nat |
469 DBVar nat |
470 | DBApp db db |
470 | DBApp db db |
471 | DBLam db |
471 | DBLam db |
472 |
472 |
473 fun dbapp_in where |
473 lemma option_map_eqvt[eqvt]: |
474 "dbapp_in None _ = None" |
474 "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
475 | "dbapp_in (Some _ ) None = None" |
475 by (cases x) (simp_all, simp add: permute_fun_app_eq) |
476 | "dbapp_in (Some x) (Some y) = Some (DBApp x y)" |
476 |
477 |
477 lemma option_bind_eqvt[eqvt]: |
478 fun dblam_in where |
478 shows "(p \<bullet> (Option.map f c)) = (Option.map (p \<bullet> f) (p \<bullet> c))" |
479 "dblam_in None = None" |
479 by (cases c) (simp_all, simp add: permute_fun_app_eq) |
480 | "dblam_in (Some x) = Some (DBLam x)" |
|
481 |
|
482 lemma db_in_eqvt[eqvt]: |
|
483 "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)" |
|
484 "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)" |
|
485 apply (case_tac [!] x) |
|
486 apply (simp_all add: eqvts) |
|
487 apply (case_tac y) |
|
488 apply (simp_all add: eqvts) |
|
489 done |
|
490 |
480 |
491 instance db :: pure |
481 instance db :: pure |
492 apply default |
482 apply default |
493 apply (induct_tac x rule: db.induct) |
483 apply (induct_tac x rule: db.induct) |
494 apply (simp_all add: permute_pure) |
484 apply (simp_all add: permute_pure) |
510 |
500 |
511 nominal_primrec |
501 nominal_primrec |
512 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
502 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
513 where |
503 where |
514 "transdb (Var x) l = vindex l x 0" |
504 "transdb (Var x) l = vindex l x 0" |
515 | "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)" |
505 | "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
516 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))" |
506 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
517 unfolding eqvt_def transdb_graph_def |
507 unfolding eqvt_def transdb_graph_def |
518 apply (rule, perm_simp, rule) |
508 apply (rule, perm_simp, rule) |
519 apply(rule TrueI) |
509 apply(rule TrueI) |
520 apply (case_tac x) |
510 apply (case_tac x) |
521 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
511 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
522 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
512 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
523 apply(simp_all) |
513 apply(simp_all) |
524 apply(erule conjE) |
514 apply(elim conjE) |
525 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
515 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
526 apply (simp add: pure_fresh) |
516 apply (simp add: pure_fresh) |
527 apply(simp add: fresh_star_def fresh_at_list) |
517 apply(simp add: fresh_star_def fresh_at_list) |
528 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) |
518 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ |
529 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) |
|
530 done |
519 done |
531 |
520 |
532 termination |
521 termination |
533 by lexicographic_order |
522 by lexicographic_order |
534 |
523 |
535 lemma transdb_eqvt[eqvt]: |
524 lemma transdb_eqvt[eqvt]: |
536 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
525 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
537 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
526 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
538 apply (simp add: vindex_eqvt) |
527 apply (simp add: vindex_eqvt) |
539 apply (simp_all add: permute_pure) |
528 apply (simp_all add: permute_pure) |
540 apply (simp add: fresh_at_list) |
529 apply (simp add: fresh_at_list) |
541 apply (subst transdb.simps) |
530 apply (subst transdb.simps) |
542 apply (simp add: fresh_at_list[symmetric]) |
531 apply (simp add: fresh_at_list[symmetric]) |
547 lemma db_trans_test: |
536 lemma db_trans_test: |
548 assumes a: "y \<noteq> x" |
537 assumes a: "y \<noteq> x" |
549 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
538 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = |
550 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
539 Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
551 using a by simp |
540 using a by simp |
|
541 |
552 |
542 |
553 abbreviation |
543 abbreviation |
554 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
544 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
555 where |
545 where |
556 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
546 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |