# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306814350 -32400
# Node ID c4ed08a7454ad94179d92b8e76bcc2b01312ccb2
# Parent  5d0875b7ed3e188ba32a1a1b88e694b676f7e5ee
Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.

diff -r 5d0875b7ed3e -r c4ed08a7454a Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 31 12:54:21 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 12:59:10 2011 +0900
@@ -380,6 +380,70 @@
 | DBApp db db
 | DBLam db
 
+fun dbapp_in where
+  "dbapp_in None _ = None"
+| "dbapp_in (Some _ ) None = None"
+| "dbapp_in (Some x) (Some y) = Some (DBApp x y)"
+
+fun dblam_in where
+  "dblam_in None = None"
+| "dblam_in (Some x) = Some (DBLam x)"
+
+lemma [eqvt]:
+  "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)"
+  "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)"
+  apply (case_tac [!] x)
+  apply (simp_all add: eqvts)
+  apply (case_tac y)
+  apply (simp_all add: eqvts)
+  done
+
+instance db :: pure
+  apply default
+  apply (induct_tac x rule: db.induct)
+  apply (simp_all add: permute_pure)
+  done
+nominal_primrec
+  trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option"
+where
+  "trans (Var x) [] n = None"
+| "trans (Var x) (h # t) n =
+     (if h = x then Some (DBVar n) else trans (Var x) t (n + 1))"
+| "trans (App t1 t2) xs n = dbapp_in (trans t1 xs n) (trans t2 xs n)"
+| "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x].t) xs n = dblam_in (trans t (x # xs) n)"
+  unfolding eqvt_def trans_graph_def
+  apply (rule, perm_simp, rule)
+  apply (case_tac x)
+  apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply (case_tac b)
+  apply (auto simp add: fresh_star_def)
+  apply (rule_tac f="dblam_in" in arg_cong)
+  apply (erule Abs1_eq_fdest)
+  apply (simp_all add: pure_fresh)
+  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
+  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> na = na")
+  apply (simp add: eqvt_at_def)
+  apply (simp add: permute_pure)
+  apply (metis atom_name_def swap_fresh_fresh)
+  done
+
+termination
+  apply (relation "measure (\<lambda>(t,l,_). size t + size t + length l)")
+  apply (simp_all add: lam.size)
+  done
+
+lemma db_trans_test:
+  assumes a: "y \<noteq> x"
+  shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
+  apply (subst trans.simps)
+  apply (simp add: fresh_def supp_Nil)
+  apply (subst trans.simps)
+  apply (simp add: fresh_def supp_Nil supp_Cons supp_at_base a)
+  apply (simp add: a)
+  done
+
+
+
 abbreviation
   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
 where