396 instance db :: pure |
396 instance db :: pure |
397 apply default |
397 apply default |
398 apply (induct_tac x rule: db.induct) |
398 apply (induct_tac x rule: db.induct) |
399 apply (simp_all add: permute_pure) |
399 apply (simp_all add: permute_pure) |
400 done |
400 done |
|
401 |
|
402 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs" |
|
403 unfolding fresh_def supp_set[symmetric] |
|
404 apply (induct xs) |
|
405 apply (simp add: supp_set_empty) |
|
406 apply simp |
|
407 apply auto |
|
408 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
|
409 done |
|
410 |
401 nominal_primrec |
411 nominal_primrec |
402 trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option" |
412 trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option" |
403 where |
413 where |
404 "trans (Var x) [] n = None" |
414 "trans (Var x) [] n = None" |
405 | "trans (Var x) (h # t) n = |
415 | "trans (Var x) (h # t) n = |
406 (if h = x then Some (DBVar n) else trans (Var x) t (n + 1))" |
416 (if h = x then Some (DBVar n) else trans (Var x) t (n + 1))" |
407 | "trans (App t1 t2) xs n = dbapp_in (trans t1 xs n) (trans t2 xs n)" |
417 | "trans (App t1 t2) xs n = dbapp_in (trans t1 xs n) (trans t2 xs n)" |
408 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x].t) xs n = dblam_in (trans t (x # xs) n)" |
418 | "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs n = dblam_in (trans t (x # xs) n)" |
409 unfolding eqvt_def trans_graph_def |
419 unfolding eqvt_def trans_graph_def |
410 apply (rule, perm_simp, rule) |
420 apply (rule, perm_simp, rule) |
411 apply (case_tac x) |
421 apply (case_tac x) |
412 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
422 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
413 apply (case_tac b) |
423 apply (case_tac b) |
414 apply (auto simp add: fresh_star_def) |
424 apply (auto simp add: fresh_star_def fresh_at_list) |
415 apply (rule_tac f="dblam_in" in arg_cong) |
425 apply (rule_tac f="dblam_in" in arg_cong) |
416 apply (erule Abs1_eq_fdest) |
426 apply (erule Abs1_eq_fdest) |
417 apply (simp_all add: pure_fresh) |
427 apply (simp_all add: pure_fresh) |
418 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
428 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
419 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> na = na") |
429 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> na = na") |
420 apply (simp add: eqvt_at_def) |
430 apply (simp add: eqvt_at_def) |
421 apply (simp add: permute_pure) |
431 apply (simp add: permute_pure) |
422 apply (metis atom_name_def swap_fresh_fresh) |
432 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
423 done |
433 done |
424 |
434 |
425 termination |
435 termination |
426 apply (relation "measure (\<lambda>(t,l,_). size t + size t + length l)") |
436 apply (relation "measure (\<lambda>(t,l,_). size t + size t + length l)") |
427 apply (simp_all add: lam.size) |
437 apply (simp_all add: lam.size) |
428 done |
438 done |
429 |
439 |
430 lemma db_trans_test: |
440 lemma db_trans_test: |
431 assumes a: "y \<noteq> x" |
441 assumes a: "y \<noteq> x" |
432 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
442 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
433 apply (subst trans.simps) |
443 using a by simp |
434 apply (simp add: fresh_def supp_Nil) |
|
435 apply (subst trans.simps) |
|
436 apply (simp add: fresh_def supp_Nil supp_Cons supp_at_base a) |
|
437 apply (simp add: a) |
|
438 done |
|
439 |
|
440 |
|
441 |
444 |
442 abbreviation |
445 abbreviation |
443 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
446 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
444 where |
447 where |
445 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
448 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |