405 apply simp |
405 apply simp |
406 apply auto |
406 apply auto |
407 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
407 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
408 done |
408 done |
409 |
409 |
410 nominal_primrec |
410 fun |
411 trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option" |
411 vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option" |
412 where |
412 where |
413 "trans (Var x) [] n = None" |
413 "vindex [] v n = None" |
414 | "trans (Var x) (h # t) n = |
414 | "vindex (h # t) v n = (if v = h then (Some (DBVar n)) else (vindex t v (Suc n)))" |
415 (if h = x then Some (DBVar n) else trans (Var x) t (n + 1))" |
415 |
416 | "trans (App t1 t2) xs n = dbapp_in (trans t1 xs n) (trans t2 xs n)" |
416 lemma vindex_eqvt[eqvt]: |
417 | "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs n = dblam_in (trans t (x # xs) n)" |
417 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
|
418 by (induct l arbitrary: n) (simp_all add: permute_pure) |
|
419 |
|
420 nominal_primrec |
|
421 trans :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
|
422 where |
|
423 "trans (Var x) l = vindex l x 0" |
|
424 | "trans (App t1 t2) xs = dbapp_in (trans t1 xs) (trans t2 xs)" |
|
425 | "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs = dblam_in (trans t (x # xs))" |
418 unfolding eqvt_def trans_graph_def |
426 unfolding eqvt_def trans_graph_def |
419 apply (rule, perm_simp, rule) |
427 apply (rule, perm_simp, rule) |
420 apply (case_tac x) |
428 apply (case_tac x) |
421 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
429 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
422 apply (case_tac b) |
|
423 apply (auto simp add: fresh_star_def fresh_at_list) |
430 apply (auto simp add: fresh_star_def fresh_at_list) |
424 apply (rule_tac f="dblam_in" in arg_cong) |
431 apply (rule_tac f="dblam_in" in arg_cong) |
425 apply (erule Abs1_eq_fdest) |
432 apply (erule Abs1_eq_fdest) |
426 apply (simp_all add: pure_fresh) |
433 apply (simp_all add: pure_fresh) |
427 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
434 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
428 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> na = na") |
|
429 apply (simp add: eqvt_at_def) |
435 apply (simp add: eqvt_at_def) |
430 apply (simp add: permute_pure) |
|
431 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
436 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
432 done |
437 done |
433 |
438 |
434 termination |
439 termination |
435 apply (relation "measure (\<lambda>(t,l,_). size t + size t + length l)") |
440 by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size) |
436 apply (simp_all add: lam.size) |
|
437 done |
|
438 |
441 |
439 lemma trans_eqvt[eqvt]: |
442 lemma trans_eqvt[eqvt]: |
440 "p \<bullet> trans t l n = trans (p \<bullet>t) (p \<bullet>l) (p \<bullet>n)" |
443 "p \<bullet> trans t l = trans (p \<bullet>t) (p \<bullet>l)" |
441 proof (nominal_induct t avoiding: l p arbitrary: n rule: lam.strong_induct) |
444 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
442 fix name l n p |
445 apply (simp add: vindex_eqvt) |
443 show "p \<bullet> trans (Var name) l n = |
446 apply (simp_all add: permute_pure) |
444 trans (p \<bullet> Var name) (p \<bullet> l) (p \<bullet> n)" |
|
445 apply (induct l arbitrary: n) |
|
446 apply simp |
|
447 apply auto |
|
448 apply (simp add: permute_pure) |
|
449 done |
|
450 next |
|
451 fix lam1 lam2 l n p |
|
452 assume |
|
453 "\<And>b ba n. ba \<bullet> trans lam1 b n = trans (ba \<bullet> lam1) (ba \<bullet> b) (ba \<bullet> n)" |
|
454 " \<And>b ba n. ba \<bullet> trans lam2 b n = trans (ba \<bullet> lam2) (ba \<bullet> b) (ba \<bullet> n)" |
|
455 then show "p \<bullet> trans (App lam1 lam2) l n = |
|
456 trans (p \<bullet> App lam1 lam2) (p \<bullet> l) (p \<bullet> n)" |
|
457 by (simp add: db_in_eqvt) |
|
458 next |
|
459 fix name :: name and l :: "name list" and p :: perm |
|
460 fix lam n |
|
461 assume |
|
462 "atom name \<sharp> l" |
|
463 "atom name \<sharp> p" |
|
464 "\<And>b ba n. ba \<bullet> trans lam b n = trans (ba \<bullet> lam) (ba \<bullet> b) (ba \<bullet> n)" |
|
465 then show |
|
466 "p \<bullet> trans (Lam [name]. lam) l n = |
|
467 trans (p \<bullet> Lam [name]. lam) (p \<bullet> l) (p \<bullet> n)" |
|
468 apply (simp add: fresh_at_list) |
447 apply (simp add: fresh_at_list) |
469 apply (subst trans.simps) |
448 apply (subst trans.simps) |
470 apply (simp add: fresh_at_list[symmetric]) |
449 apply (simp add: fresh_at_list[symmetric]) |
471 apply (simp add: db_in_eqvt) |
450 apply (drule_tac x="name # l" in meta_spec) |
472 done |
451 apply auto |
473 qed |
452 done |
474 |
453 |
475 lemma db_trans_test: |
454 lemma db_trans_test: |
476 assumes a: "y \<noteq> x" |
455 assumes a: "y \<noteq> x" |
477 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
456 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
478 using a by simp |
457 using a by simp |