--- a/Quot/Nominal/LFex.thy	Wed Feb 03 11:47:37 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 03 12:11:23 2010 +0100
@@ -640,9 +640,9 @@
 done
 
 lemma supp_fv:
- "fv_kind t1 = supp t1"
- "fv_ty t2 = supp t2"
- "fv_trm t3 = supp t3"
+ "supp t1 = fv_kind t1"
+ "supp t2 = fv_ty t2"
+ "supp t3 = fv_trm t3"
 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
 apply (simp_all add: supp_kind_ty_trm_easy)
 apply (simp_all add: fv_kind_ty_trm)
@@ -650,39 +650,33 @@
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
 apply(simp add: KIND_TY_TRM_INJECT)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] alpha_gen)
-apply(simp add: Abs_eq_iff alpha_gen)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
+apply(simp add: supp_Abs Set.Un_commute)
+apply(simp (no_asm) add: supp_def)
+apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-sorry (* Stuck *)
+apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
+apply(simp add: supp_Abs Set.Un_commute)
+apply(simp (no_asm) add: supp_def)
+apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: Abs_eq_iff)
+apply(simp add: alpha_gen)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+done
 
+(* Not needed anymore *)
 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
-(*apply (subst supp_Pair[symmetric])*)
-unfolding supp_def
-apply (simp add: permute_set_eq)
-apply(subst Abs_eq_iff)
-apply(subst KIND_TY_TRM_INJECT)
-apply(simp only: alpha_gen supp_fv)
-apply simp
-apply (simp_all add: Collect_imp_eq Collect_neg_eq)
-apply(subst Set.Un_commute)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-prefer 2
-apply (rule refl)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
-apply (rule refl)
-apply (simp_all)
-apply (simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
-sorry (* should be true... *)
-
-lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
-apply(subst supp_kpi_pre)
-apply(subst supp_Abs)
-apply (simp only: Set.Un_commute)
+apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT)
+apply (simp add: alpha_gen supp_fv)
+apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
 done
 
 lemma supp_kind_ty_trm:
@@ -696,9 +690,8 @@
  "supp (APP M N) = supp M \<union> supp N"
  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
 apply (simp_all only: supp_kind_ty_trm_easy)
-apply (simp add: supp_kpi)
-sorry (* Other ones will follow similarily *)
-
+apply (simp_all only: supp_fv fv_kind_ty_trm)
+done
 
 end