383 fun dbapp_in where

   384   "dbapp_in None _ = None"

   385 | "dbapp_in (Some _ ) None = None"

   386 | "dbapp_in (Some x) (Some y) = Some (DBApp x y)"

   387 

   388 fun dblam_in where

   389   "dblam_in None = None"

   390 | "dblam_in (Some x) = Some (DBLam x)"

   391 

   392 lemma [eqvt]:

   393   "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)"

   394   "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)"

   395   apply (case_tac [!] x)

   396   apply (simp_all add: eqvts)

   397   apply (case_tac y)

   398   apply (simp_all add: eqvts)

   399   done

   400 

   401 instance db :: pure

   402   apply default

   403   apply (induct_tac x rule: db.induct)

   404   apply (simp_all add: permute_pure)

   405   done

   406 nominal_primrec

   407   trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option"

   408 where

   409   "trans (Var x) [] n = None"

   410 | "trans (Var x) (h # t) n =

   411      (if h = x then Some (DBVar n) else trans (Var x) t (n + 1))"

   412 | "trans (App t1 t2) xs n = dbapp_in (trans t1 xs n) (trans t2 xs n)"

   413 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x].t) xs n = dblam_in (trans t (x # xs) n)"

   414   unfolding eqvt_def trans_graph_def

   415   apply (rule, perm_simp, rule)

   416   apply (case_tac x)

   417   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)

   418   apply (case_tac b)

   419   apply (auto simp add: fresh_star_def)

   420   apply (rule_tac f="dblam_in" in arg_cong)

   421   apply (erule Abs1_eq_fdest)

   422   apply (simp_all add: pure_fresh)

   423   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")

   424   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> na = na")

   425   apply (simp add: eqvt_at_def)

   426   apply (simp add: permute_pure)

   427   apply (metis atom_name_def swap_fresh_fresh)

   428   done

   429 

   430 termination

   431   apply (relation "measure (\<lambda>(t,l,_). size t + size t + length l)")

   432   apply (simp_all add: lam.size)

   433   done

   434 

   435 lemma db_trans_test:

   436   assumes a: "y \<noteq> x"

   437   shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"

   438   apply (subst trans.simps)

   439   apply (simp add: fresh_def supp_Nil)

   440   apply (subst trans.simps)

   441   apply (simp add: fresh_def supp_Nil supp_Cons supp_at_base a)

   442   apply (simp add: a)

   443   done

   444 

   445 

   446