--- a/Nominal/Ex/Lambda.thy	Tue Jul 05 04:19:02 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 04:23:33 2011 +0200
@@ -359,23 +359,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
@@ -401,8 +391,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)
@@ -410,12 +400,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
@@ -423,7 +412,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)
@@ -439,6 +428,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  
@@ -611,48 +601,6 @@
 apply (rule, perm_simp, rule)
 oops
 
-text {* tests of functions containing if and case *}
-
-consts P :: "lam \<Rightarrow> bool"
-
-nominal_primrec  
-  A :: "lam => lam"
-where  
-  "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
-| "A (Var x) = (Var x)" 
-| "A (App M N) = (if True then M else A N)"
-oops
-
-nominal_primrec  
-  C :: "lam => lam"
-where  
-  "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
-| "C (Var x) = (Var x)" 
-| "C (App M N) = (if True then M else C N)"
-oops
-
-nominal_primrec  
-  A :: "lam => lam"
-where  
-  "A (Lam [x].M) = (Lam [x].M)"
-| "A (Var x) = (Var x)"
-| "A (App M N) = (if True then M else A N)"
-oops
-
-nominal_primrec  
-  B :: "lam => lam"
-where  
-  "B (Lam [x].M) = (Lam [x].M)"
-| "B (Var x) = (Var x)"
-| "B (App M N) = (if True then M else (B N))"
-unfolding eqvt_def
-unfolding B_graph_def
-apply(perm_simp)
-apply(rule allI)
-apply(rule refl)
-oops
-
-
 lemma test:
   assumes "t = s"
   and "supp p \<sharp>* t" "supp p \<sharp>* x"
@@ -720,6 +668,88 @@
 
 termination by lexicographic_order
 
+lemma abs_same_binder:
+  fixes t ta s sa :: "_ :: fs"
+  assumes "sort_of (atom x) = sort_of (atom y)"
+  shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa
+     \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"
+  by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)
+
+nominal_primrec
+  aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"
+where
+  "aux2 (Var x) (Var y) = (x = y)"
+| "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)"
+| "aux2 (Var x) (App t1 t2) = False"
+| "aux2 (Var x) (Lam [y].t) = False"
+| "aux2 (App t1 t2) (Var x) = False"
+| "aux2 (App t1 t2) (Lam [x].t) = False"
+| "aux2 (Lam [x].t) (Var y) = False"
+| "aux2 (Lam [x].t) (App t1 t2) = False"
+| "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
+  apply(simp add: eqvt_def aux2_graph_def)
+  apply(rule, perm_simp, rule, rule)
+  apply(case_tac x)
+  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply(rule_tac y="b" in lam.exhaust)
+  apply(auto)[3]
+  apply(rule_tac y="b" in lam.exhaust)
+  apply(auto)[3]
+  apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)
+  apply(auto)[3]
+  apply(drule_tac x="name" in meta_spec)
+  apply(drule_tac x="name" in meta_spec)
+  apply(drule_tac x="lam" in meta_spec)
+  apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
+  apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def)
+  apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
+  apply simp_all
+  apply (simp add: abs_same_binder)
+  apply (erule_tac c="()" in Abs_lst1_fcb2)
+  apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)
+  done
+
+text {* tests of functions containing if and case *}
+
+consts P :: "lam \<Rightarrow> bool"
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
+| "A (Var x) = (Var x)" 
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  C :: "lam => lam"
+where  
+  "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
+| "C (Var x) = (Var x)" 
+| "C (App M N) = (if True then M else C N)"
+oops
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (Lam [x].M) = (Lam [x].M)"
+| "A (Var x) = (Var x)"
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  B :: "lam => lam"
+where  
+  "B (Lam [x].M) = (Lam [x].M)"
+| "B (Var x) = (Var x)"
+| "B (App M N) = (if True then M else (B N))"
+unfolding eqvt_def
+unfolding B_graph_def
+apply(perm_simp)
+apply(rule allI)
+apply(rule refl)
+oops
+
 end