--- a/Nominal/Ex/Lambda.thy	Thu Feb 24 16:26:11 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Feb 24 18:50:02 2011 +0000
@@ -320,9 +320,9 @@
 
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-apply(induct xs arbitrary: n)
-apply(simp_all add: permute_pure)
-done
+  apply(induct xs arbitrary: n)
+  apply(simp_all add: permute_pure)
+  done
 
 nominal_primrec
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
@@ -334,20 +334,16 @@
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-apply(simp_all)[3]
+apply(simp_all add: fresh_star_def)[3]
 apply(blast)
 apply(blast)
-apply(simp add: fresh_star_def)
 apply(simp_all add: lam.distinct)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(simp add: lam.eq_iff)
 apply(erule conjE)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
+apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
 prefer 2
-apply(rule conjI)
-apply(simp add: Abs_fresh_iff)
-apply(drule sym)
 apply(simp add: Abs_fresh_iff)
 apply(subst (asm) Abs_eq_iff2)
 apply(auto)
@@ -356,22 +352,92 @@
 apply(clarify)
 apply(rule trans)
 apply(rule_tac p="p" in supp_perm_eq[symmetric])
+prefer 2
+apply (subgoal_tac "p \<bullet> xsa = xsa")
+apply (simp add: eqvt_at_def)
+apply (rule supp_perm_eq)
+apply (rule fresh_star_supp_conv)
+apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa")
+apply (simp add: fresh_star_def fresh_def)
+apply blast
+apply (simp add: fresh_star_def fresh_def)
+apply (simp add:  ln.supp)
 apply(rule fresh_star_supp_conv)
-apply(drule fresh_star_perm_set_conv)
-apply(simp add: finite_supp)
-apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* LNLam (trans_sumC (t, x # xsa))")
-apply(auto simp add: fresh_star_def)[1]
-apply(simp (no_asm) add: fresh_star_def ln.fresh)
-apply(rule conjI)
+apply (subst (asm) supp_perm_pair)
+apply (elim disjE)
+apply (simp add: fresh_star_def supp_zero_perm)
+apply (simp add: flip_def[symmetric])
+apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)")
+apply simp
+apply (subst flip_def)
+apply (simp add: supp_swap)
+apply (simp add: fresh_star_def)
+apply (rule)
+apply rule
+prefer 2
 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
 apply(simp add: finite_supp)
 apply(simp (no_asm_use) add: fresh_Pair)
 apply(simp add: Abs_fresh_iff fresh_Cons)[1]
-apply(erule disjE)
-apply(erule disjE)
-apply(simp)
+apply (metis Rep_name_inverse atom_name_def fresh_at_base)
+apply assumption
 oops
 
+(* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"
+  apply (case_tac "x = xa")
+  apply simp
+  apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric])
+  by (metis atom_eqvt flip_at_simps(2) fresh_permute_iff)
+
+lemma supp_lookup: "supp (lookup l n name) = {atom name} - supp l"
+  apply (induct l arbitrary: n)
+  apply (simp_all add: ln.supp supp_at_base supp_Nil supp_Cons pure_supp)
+  done
+
+lemma trans_eqvt[eqvt]: "p \<bullet> (trans t l) = trans (p \<bullet> t) (p \<bullet> l)"
+  apply (induct t l rule: trans.induct)
+  apply simp_all
+  apply (simp add: eqvts permute_pure)
+  done
+
+lemma diff_un: "a - (b \<union> c) = a - b - c"
+  by blast
+
+lemma supp_trans: "supp (trans t l) = supp t - supp l"
+  apply (induct t arbitrary: l rule: lam.induct)
+  apply (simp_all add: lam.supp supp_at_base supp_lookup ln.supp)
+  apply blast
+  apply (rule_tac x="(lam, l)" and ?'a="name" in obtain_fresh)
+  apply (simp add: fresh_Pair)
+  apply clarify
+  apply (subgoal_tac "supp (Lambda.trans (Lam [a]. ((name \<leftrightarrow> a) \<bullet> lam)) l) =
+    supp lam - {atom name} - supp l")
+  using helpr
+  apply simp
+  apply (simp add: ln.supp)
+  apply (subgoal_tac "supp ((name \<leftrightarrow> a) \<bullet> (Lambda.trans lam ((name \<leftrightarrow> a) \<bullet> (a # l)))) = supp lam - {atom name} - supp l")
+  apply (simp add: trans_eqvt)
+  apply (simp add: supp_eqvt[symmetric])
+  apply (simp add: Diff_eqvt)
+  apply (simp add: supp_eqvt supp_Cons  union_eqvt)
+  apply (simp add: diff_un)
+  apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})
+  apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})
+  apply rule
+  prefer 2
+  apply rule
+  apply (simp add: supp_at_base)
+  apply (subgoal_tac "(name \<leftrightarrow> a) \<bullet> (supp lam - {atom name}) = supp lam - {atom name}")
+  apply (simp add: eqvts)
+  unfolding flip_def
+  apply (rule swap_fresh_fresh)
+apply (metis fresh_at_base fresh_def fresh_minus_atom_set lam.fsupp supp_at_base)
+by (metis fresh_def fresh_finite_atom_set fresh_minus_atom_set lam.fsupp)
+
+lemma "atom x \<sharp> trans_sumC (t, x # xsa)"
+  by (simp add: fresh_def meta_eq_to_obj_eq[OF trans_def, symmetric, unfolded fun_eq_iff] supp_trans supp_Cons supp_at_base)
+*)
+
 nominal_datatype db = 
   DBVar nat
 | DBApp db db

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Lambda_add.thy	Thu Feb 24 18:50:02 2011 +0000
@@ -0,0 +1,79 @@
+theory Lambda_add
+imports "Lambda"
+begin
+
+nominal_primrec
+  addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)"
+| "addlam_pre (Var x) (App t1 t2) = Var x"
+| "addlam_pre (Var x) (Var v) = Var x"
+| "addlam_pre (App t1 t2) it = App t1 t2"
+| "addlam_pre (Lam [x]. t) it = Lam [x].t"
+apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_pre_graph (p \<bullet> a) (p \<bullet> x)")
+apply (simp add: eqvt_def)
+apply (intro allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply rule
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply simp
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply simp
+apply (erule addlam_pre_graph.induct)
+apply (simp_all add: addlam_pre_graph.intros)
+apply (simp_all add:lam.distinct)
+apply clarify
+apply simp
+apply (rule_tac y="a" in lam.exhaust)
+apply(auto simp add: lam.distinct lam.eq_iff)
+prefer 2 apply blast
+prefer 2 apply blast
+apply (rule_tac y="b" and c="name" in lam.strong_exhaust)
+apply(auto simp add: lam.distinct lam.eq_iff)[3]
+apply blast
+apply(drule_tac x="namea" in meta_spec)
+apply(drule_tac x="name" in meta_spec)
+apply(drule_tac x="lam" in meta_spec)
+apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1]
+apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base)
+done
+
+termination
+  by (relation "measure (\<lambda>(t,_). size t)")
+     (simp_all add: lam.size)
+
+function
+  addlam :: "lam \<Rightarrow> lam"
+where
+  "addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))"
+| "addlam (App t1 t2) = App t1 t2"
+| "addlam (Lam [x]. t) = Lam [x].t"
+apply (simp_all add:lam.distinct)
+apply (rule_tac y="x" in lam.exhaust)
+apply auto
+apply (simp add:lam.eq_iff)
+done
+
+termination
+  by (relation "measure (\<lambda>(t). size t)")
+     (simp_all add: lam.size)
+
+lemma addlam':
+  "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
+  apply simp
+  apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv")
+  apply simp
+  apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base)
+  done
+
+end
+
+
+

--- a/Nominal/Ex/TypeSchemes.thy	Thu Feb 24 16:26:11 2011 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Feb 24 18:50:02 2011 +0000
@@ -63,6 +63,14 @@
 apply(simp)
 done
 
+lemma helper:
+  assumes "A - C = A - D"
+  and "B - C = B - D"
+  and "E \<subseteq> A \<union> B"
+  shows "E - C = E - D"
+using assms
+by blast
+
 nominal_primrec
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
@@ -224,7 +232,7 @@
 defer
 apply (simp add: ty_tys.eq_iff)
 apply (simp only: Abs_eq_res_set)
-apply (subgoal_tac "(atom ` fset xsa \<inter> supp T - atom ` fset xs \<inter> supp Ta) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
+apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
 apply (subst (asm) Abs_eq_iff2)
 apply (clarify)
 apply (simp add: alphas)
@@ -247,25 +255,18 @@
 apply(clarify)
 apply auto[1]
 apply (simp add: fresh_star_def fresh_def)
---"HERE"
+
 apply (simp (no_asm) add: fresh_star_def)
 apply rule
 apply auto[1]
 apply(simp (no_asm) only: Abs_fresh_iff)
 apply(clarify)
 apply auto[1]
-prefer 2
-apply (simp add: fresh_def)
 apply(drule_tac a="atom x" in fresh_eqvt_at)
 apply (simp add: supp_Pair finite_supp)
 apply (simp add: fresh_Pair)
-apply(auto simp add: Abs_fresh_iff fresh_star_def)[1]
-prefer 2
-apply auto[1]
-apply (erule_tac x="atom x" in ballE)
-apply auto[1]
-apply (auto simp add: fresh_def)[1]
-
+apply(auto simp add: Abs_fresh_iff fresh_star_def)[2]
+apply (simp add: fresh_def)
 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
 prefer 2
 apply (rule perm_supp_eq)
@@ -275,12 +276,45 @@
 apply blast
 apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
 apply (simp only: Abs_eq_res_set[symmetric])
-
-apply (rule_tac s="[p \<bullet> atom ` fset xs \<inter> supp (\<theta>', p \<bullet> T)]res. subst \<theta>' (p \<bullet> T)" in trans)
---"What if (p \<bullet> xs) is not fresh for \<theta>' ?"
+apply (simp add: Abs_eq_iff alphas)
+apply rule
+prefer 2
+apply (rule_tac x="0 :: perm" in exI)
+apply (simp add: fresh_star_zero)
+apply (rule helper)
+prefer 3
+apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)")
+apply simp
+apply (subst supp_Pair[symmetric])
+apply (rule supp_eqvt_at)
+apply (simp add: eqvt_at_def)
+apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)")
+apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)")
+apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)")
+apply (thin_tac "(atom ` fset xsa \<inter> supp (p \<bullet> T) - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
+apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'")
+apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'")
+apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p")
+apply (rule)
+apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)")
+apply (erule_tac x="p" in allE)
+apply (erule_tac x="pa + p" in allE)
+apply (metis permute_plus)
+apply assumption
+apply (simp add: supp_Pair finite_supp)
+prefer 2 apply blast
+prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI)
+apply (rule_tac s="supp \<theta>'" in trans)
+apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'")
+apply (auto simp add: fresh_star_def fresh_def)[1]
+apply (subgoal_tac "supp p \<sharp>* \<theta>'")
+apply (metis fresh_star_permute_iff)
+apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'")
+apply (auto simp add: fresh_star_def)[1]
+apply (simp add: fresh_star_Un)
+apply (auto simp add: fresh_star_def fresh_def)[1]
 oops
 
-
 section {* defined as two separate nominal datatypes *}
 
 nominal_datatype ty2 =