--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 13:41:30 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 16:13:42 2011 +0900
@@ -78,13 +78,6 @@
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
-
-term subst_substs_sumC
-thm subst_substs_sumC_def
-term Inl
-thm subst_substs_graph.induct
-thm subst_substs_graph.intros
-thm Projl.simps
 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)
@@ -192,7 +185,6 @@
 apply (auto)[5]
 --"LAST GOAL"
 apply(simp del: ty_tys.eq_iff)
-thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]
 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
@@ -343,45 +335,22 @@
 
 lemma lookup2_eqvt[eqvt]:
   shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup2.induct)
-apply(simp_all)
-done
+  by (induct Ts T rule: lookup2.induct) simp_all
 
 nominal_primrec
   subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
 where
   "subst \<theta> (Var2 X) = lookup2 \<theta> X"
 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
-defer
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="b" in ty2.exhaust)
-apply(blast)
-apply(blast)
-apply(simp_all add: ty2.distinct)
-apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
-apply(simp add: eqvt_def)
-apply(rule allI)
-apply(simp add: permute_fun_def permute_bool_def)
-apply(rule ext)
-apply(rule ext)
-apply(rule iffI)
-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 subst_graph.induct)
-apply(perm_simp)
-apply(rule subst_graph.intros)
-apply(perm_simp)
-apply(rule subst_graph.intros)
-apply(assumption)
-apply(assumption)
-done
+  unfolding eqvt_def subst_graph_def
+  apply (rule, perm_simp, rule)
+  apply(case_tac x)
+  apply(simp)
+  apply(rule_tac y="b" in ty2.exhaust)
+  apply(blast)
+  apply(blast)
+  apply(simp_all add: ty2.distinct)
+  done
 
 termination
   apply(relation "measure (size o snd)")
@@ -394,40 +363,87 @@
 apply(simp_all add: lookup2_eqvt)
 done
 
-lemma j:
-  assumes "a \<sharp> Ts" " a \<sharp> X"
-  shows "a \<sharp> lookup2 Ts X"
-using assms
-apply(induct Ts X rule: lookup2.induct)
-apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair)
-done
-
-lemma i:
-  assumes "a \<sharp> t" " a \<sharp> \<theta>"
-  shows "a \<sharp> subst \<theta> t"
-using assms
-apply(induct \<theta> t rule: subst.induct)
-apply(auto simp add: ty2.fresh j)
-done 
-
-lemma k:
-  assumes "as \<sharp>* t" " as \<sharp>* \<theta>"
-  shows "as \<sharp>* subst \<theta> t"
-using assms
-by (simp add: fresh_star_def i)
-
-lemma h:
-  assumes "as \<subseteq> bs \<union> cs"
-  and " cs \<sharp>* x"
-  shows "(as - bs) \<sharp>* x"
-using assms
-by (auto simp add: fresh_star_def)
-
+lemma supp_fun_app2_eqvt:
+  assumes e: "eqvt f"
+  shows "supp (f a b) \<subseteq> supp a \<union> supp b"
+  using supp_fun_app_eqvt[OF e] supp_fun_app
+  by blast
+ 
+lemma supp_subst:
+  "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
+  apply (rule supp_fun_app2_eqvt)
+  unfolding eqvt_def by (simp add: eqvts_raw)
+ 
+lemma fresh_star_inter1:
+  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
+  unfolding fresh_star_def by blast
+ 
 nominal_primrec
   substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
 where
   "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
-oops
+  unfolding eqvt_def substs_graph_def
+  apply (rule, perm_simp, rule)
+  apply auto[1]
+  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 (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
+  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 (simp add: alphas fresh_star_zero)
+  apply auto[1]
+  apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
+  apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
+  apply (drule subsetD[OF supp_subst])
+  apply auto[1]
+  apply (simp add: fresh_star_def fresh_def)
+  apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
+  apply (smt IntI inf_le1 inter_eqvt subsetD 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 (simp add: fresh_star_def fresh_def)
+  apply blast
+  done
 
 
 text {* Some Tests about Alpha-Equality *}