# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306818751 -32400
# Node ID 929bd2dd1ab2bfb68a522a51d3d41abf7fb97a30
# Parent  9bc46d04fb2cd3af846d39de76919eb8d005026e
DeBruijn translation in a simplifier friendly way

diff -r 9bc46d04fb2c -r 929bd2dd1ab2 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 31 13:25:35 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 14:12:31 2011 +0900
@@ -398,6 +398,16 @@
   apply (induct_tac x rule: db.induct)
   apply (simp_all add: permute_pure)
   done
+
+lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
+  unfolding fresh_def supp_set[symmetric]
+  apply (induct xs)
+  apply (simp add: supp_set_empty)
+  apply simp
+  apply auto
+  apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
+  done
+
 nominal_primrec
   trans :: "lam \<Rightarrow> name list \<Rightarrow> nat \<Rightarrow> db option"
 where
@@ -405,13 +415,13 @@
 | "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)"
+| "x \<notin> set 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 (auto simp add: fresh_star_def fresh_at_list)
   apply (rule_tac f="dblam_in" in arg_cong)
   apply (erule Abs1_eq_fdest)
   apply (simp_all add: pure_fresh)
@@ -419,7 +429,7 @@
   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)
+  apply (metis atom_name_def swap_fresh_fresh fresh_at_list)
   done
 
 termination
@@ -430,14 +440,7 @@
 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
-
-
+  using a by simp
 
 abbreviation
   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65)