# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307523126 -32400
# Node ID 76db0b854bf626d94067da8e6d8bf2b583ac300a
# Parent  fff147e99375edf97ca225f94c240c7d64cc0432
Simpler proof of TypeSchemes/substs

diff -r fff147e99375 -r 76db0b854bf6 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 17:25:54 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 17:52:06 2011 +0900
@@ -382,8 +382,7 @@
     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"
+               \<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)
@@ -421,25 +420,15 @@
   apply (simp add: Abs_fresh_iff)
   apply auto[1]
   apply (simp add: fresh_def fresh_star_def)
-  apply (rule contra_subsetD)
-  apply (rule supp_subst)
+  apply (rule contra_subsetD[OF  supp_subst])
   apply simp
   apply blast
+  apply clarify
   apply (simp add: subst_eqvt)
-  apply clarify
   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 (simp add: subst_eqvt)
   apply auto[1]
   apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
   apply (simp add: inter_eqvt)
@@ -449,17 +438,16 @@
   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 4)
-  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