# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1298075482 -32400
# Node ID 1feef59f3aa40cd5a119b1179944fa5cad2ded0c
# Parent  c10b56d226ce6a9a5fc8d02e7d6f94fe0b382e27
typeschemes/subst

diff -r c10b56d226ce -r 1feef59f3aa4 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Feb 17 17:02:25 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Feb 19 09:31:22 2011 +0900
@@ -255,21 +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]
-apply auto[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)
@@ -291,11 +288,31 @@
 apply (subst supp_Pair[symmetric])
 apply (rule supp_eqvt_at)
 apply (simp add: eqvt_at_def)
-defer --"because eqvt_at Ta"
+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)
---"p and xs and xsa are fresh for theta"
+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 *}