diff -r 40991ebcda12 -r fac8895b109a Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Jul 05 09:28:16 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 10:13:34 2011 +0900
@@ -470,23 +470,13 @@
 | 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 option_map_eqvt[eqvt]:
+  "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
+  by (cases x) (simp_all, simp add: permute_fun_app_eq)
 
-lemma db_in_eqvt[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
+lemma option_bind_eqvt[eqvt]:
+  shows "(p \<bullet> (Option.map f c)) = (Option.map (p \<bullet> f) (p \<bullet> c))"
+  by (cases c) (simp_all, simp add: permute_fun_app_eq)
 
 instance db :: pure
   apply default
@@ -512,8 +502,8 @@
   transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
 where
   "transdb (Var x) l = vindex l x 0"
-| "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)"
-| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))"
+| "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
+| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
   unfolding eqvt_def transdb_graph_def
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
@@ -521,12 +511,11 @@
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def fresh_at_list)[3]
   apply(simp_all)
-  apply(erule conjE)
+  apply(elim conjE)
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
   apply (simp add: pure_fresh)
   apply(simp add: fresh_star_def fresh_at_list)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+
   done
 
 termination
@@ -534,7 +523,7 @@
 
 lemma transdb_eqvt[eqvt]:
   "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"
-  apply (nominal_induct t avoiding: l p rule: lam.strong_induct)
+  apply (nominal_induct t avoiding: l rule: lam.strong_induct)
   apply (simp add: vindex_eqvt)
   apply (simp_all add: permute_pure)
   apply (simp add: fresh_at_list)
@@ -550,6 +539,7 @@
   Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
   using a by simp
 
+
 abbreviation
   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
 where