# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307532656 -3600
# Node ID 80bbb023402577460f94b5d0bdae3e336230bfd4
# Parent  71382ce4d2ed2157162f8a41cff58c89d7080a83# Parent  76db0b854bf626d94067da8e6d8bf2b583ac300a
merged

diff -r 71382ce4d2ed -r 80bbb0234025 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 08 12:30:46 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 08 12:30:56 2011 +0100
@@ -432,7 +432,11 @@
   shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}"
   by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln.supp pure_supp supp_at_base)
 
-lemma [eqvt]:
+lemma supp_lookup_fresh:
+  shows "atom ` set xs \<sharp>* lookup xs n x"
+  by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin)
+
+lemma lookup_eqvt[eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
@@ -442,73 +446,43 @@
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
-apply(simp add: eqvt_def trans_graph_def)
-apply (rule, perm_simp, rule)
+  apply (simp add: eqvt_def trans_graph_def)
+  apply (rule, perm_simp, rule)
   apply (erule trans_graph.induct)
-  apply(simp)
-  apply (case_tac "xa \<in> set xs")
-  apply (simp add: fresh_star_def fresh_def supp_lookup_in)
-  apply (simp add: fresh_star_def fresh_def supp_lookup_notin)
-  apply blast
+  apply (auto simp add: ln.fresh)
+  apply (simp add: supp_lookup_fresh)
   apply (simp add: fresh_star_def ln.fresh)
-  apply(simp)
   apply (simp add: ln.fresh fresh_star_def)
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-apply(simp_all add: fresh_star_def)[3]
-apply(blast)
-apply(blast)
-apply(simp_all)
-apply(elim conjE)
-apply clarify
-apply (erule Abs1_eq_fdest)
-apply (simp_all add: ln.fresh)
-prefer 2
-apply(drule supp_eqvt_at)
-apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
-prefer 2
-apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
-apply (simp add: eqvt_at_def)
-apply (metis atom_name_def swap_fresh_fresh)
-apply(simp add: fresh_star_def)
-done
+  apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply (auto simp add: fresh_star_def)[3]
+  apply (erule Abs1_eq_fdest)
+  apply (simp_all add: fresh_star_def)
+  apply (drule supp_eqvt_at)
+  apply (rule finite_supp)
+  apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1]
+  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  done
 
 
 termination
   by (relation "measure (size o fst)") (simp_all add: lam.size)
 
-nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+nominal_primrec
   cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
 where
   "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))"
-apply(simp add: eqvt_def cbvs_graph_def)
-apply (rule, perm_simp, rule)
-  apply (erule cbvs_graph.induct)
-  apply(simp add: fresh_star_def pure_fresh)
-  apply(simp add: fresh_star_def pure_fresh)
-  apply(simp add: fresh_star_def pure_fresh)
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-apply(simp_all add: fresh_star_def)[3]
-apply(blast)
-apply(blast)
-apply(simp_all)
-apply(elim conjE)
-apply clarify
-apply (erule Abs1_eq_fdest)
-apply (simp_all add: ln.fresh)
-apply(simp add: fresh_star_def)
-apply(drule supp_eqvt_at)
-apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
-apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
-apply (simp add: eqvt_at_def)
-apply (metis atom_name_def swap_fresh_fresh)
-done
-
+  apply(simp add: eqvt_def cbvs_graph_def)
+  apply(rule, perm_simp, rule)
+  apply(simp_all)
+  apply(case_tac x)
+  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply(auto simp add: fresh_star_def)
+  apply(erule Abs1_eq_fdest)
+  apply(simp_all add: pure_fresh)
+  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  done
 
 termination
   by (relation "measure (size o fst)") (simp_all add: lam.size)
diff -r 71382ce4d2ed -r 80bbb0234025 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 12:30:46 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 12:30:56 2011 +0100
@@ -362,7 +362,6 @@
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   apply(case_tac x)
-  apply(simp)
   apply(rule_tac y="b" in ty2.exhaust)
   apply(blast)
   apply(blast)
@@ -370,15 +369,11 @@
   done
 
 termination
-  apply(relation "measure (size o snd)")
-  apply(simp_all add: ty2.size)
-  done
+  by (relation "measure (size o snd)") (simp_all add: ty2.size)
 
 lemma subst_eqvt[eqvt]:
   shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
-apply(induct \<theta> T rule: subst.induct)
-apply(simp_all add: lookup2_eqvt)
-done
+  by (induct \<theta> T rule: subst.induct) (simp_all add: lookup2_eqvt)
 
 lemma supp_fun_app2_eqvt:
   assumes e: "eqvt f"
@@ -394,7 +389,38 @@
 lemma fresh_star_inter1:
   "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
   unfolding fresh_star_def by blast
- 
+
+lemma Abs_res_fcb:
+  fixes xs ys :: "('a :: at_base) set"
+    and S T :: "'b :: fs"
+  assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)"
+    and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T"
+    and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T"
+    and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S
+               \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S \<Longrightarrow> p \<bullet> (f xs T) = f ys S"
+  shows "f xs T = f ys S"
+  using e apply -
+  apply (subst (asm) Abs_eq_res_set)
+  apply (subst (asm) Abs_eq_iff2)
+  apply (simp add: alphas)
+  apply (elim exE conjE)
+  apply(rule trans)
+  apply (rule_tac p="p" in supp_perm_eq[symmetric])
+  apply(rule fresh_star_supp_conv)
+  apply(drule fresh_star_perm_set_conv)
+  apply (rule finite_Diff)
+  apply (rule finite_supp)
+  apply (subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T")
+  apply (metis Un_absorb2 fresh_star_Un)
+  apply (subst fresh_star_Un)
+  apply (rule conjI)
+  apply (simp add: fresh_star_def f1)
+  apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys")
+  apply (simp add: fresh_star_def f2)
+  apply blast
+  apply (simp add: eqv)
+  done
+
 nominal_primrec
   substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
 where
@@ -404,65 +430,39 @@
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
   apply auto
-  apply (subst (asm) Abs_eq_res_set)
-  apply (subst (asm) Abs_eq_iff2)
-  apply (clarify)
-  apply (simp add: alphas)
-  apply (clarify)
-  apply (rule trans)
-  apply(rule_tac p="p" in supp_perm_eq[symmetric])
-  apply(rule fresh_star_supp_conv)
-  apply(drule fresh_star_perm_set_conv)
-  apply (rule finite_Diff)
-  apply (rule finite_supp)
-  apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* ([atom ` fset xs]res. subst \<theta>' t)")
-  apply (metis Un_absorb2 fresh_star_Un)
-  apply (subst fresh_star_Un)
-  apply (rule conjI)
-  apply (simp (no_asm) add: fresh_star_def)
-  apply (rule)
+  apply (erule Abs_res_fcb)
+  apply (simp add: Abs_fresh_iff)
   apply (simp add: Abs_fresh_iff)
-  apply (simp add: fresh_star_def)
-  apply (rule)
-  apply (simp (no_asm) add: Abs_fresh_iff)
   apply auto[1]
-  apply (simp add: fresh_def supp_Abs)
-  apply (rule contra_subsetD)
-  apply (rule supp_subst)
-  apply auto[1]
+  apply (simp add: fresh_def fresh_star_def)
+  apply (rule contra_subsetD[OF  supp_subst])
   apply simp
+  apply blast
+  apply clarify
+  apply (simp add: subst_eqvt)
   apply (subst Abs_eq_iff)
   apply (rule_tac x="0::perm" in exI)
-  apply (subgoal_tac "p \<bullet> subst \<theta>' t = subst \<theta>' (p \<bullet> t)")
-  prefer 2
-  apply (subgoal_tac "\<theta>' = p \<bullet> \<theta>'")
-  apply (simp add: subst_eqvt)
-  apply (rule sym)
-  apply (rule perm_supp_eq)
-  apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'")
-  apply (metis Diff_partition fresh_star_Un)
-  apply (simp add: fresh_star_Un fresh_star_inter1)
+  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
   apply auto[1]
   apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
   apply (simp add: inter_eqvt)
   apply blast
   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
-  apply (simp add: IntI image_eqI)
+  apply (auto simp add: IntI image_eqI)
   apply (drule subsetD[OF supp_subst])
   apply (simp add: fresh_star_def fresh_def)
   apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
-  apply (simp add: )
+  apply (simp)
   apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
-  apply (metis inf1I inter_eqvt mem_def supp_eqvt )
-  apply (rotate_tac 6)
-  apply (drule sym)
-  apply (simp add: subst_eqvt)
-  apply (drule subsetD[OF supp_subst])
-  apply auto[1]
-  apply (rotate_tac 2)
-  apply (subst (asm) fresh_star_permute_iff[symmetric])
+  apply (metis inf1I inter_eqvt mem_def supp_eqvt)
+  apply (subgoal_tac "x \<notin> supp \<theta>'")
+  apply (metis UnE subsetD supp_subst)
+  apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>')")
   apply (simp add: fresh_star_def fresh_def)
+  apply (simp (no_asm) add: fresh_star_permute_iff)
+  apply (rule perm_supp_eq)
+  apply (simp add: fresh_def fresh_star_def)
   apply blast
   done