--- a/Quot/Nominal/LFex.thy	Wed Feb 24 12:06:55 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 14:09:34 2010 +0100
@@ -196,72 +196,49 @@
 apply(simp_all only: kind_ty_trm_fs)
 done
 
-lemma supp_rkind_rty_rtrm_easy:
- "supp TYP = {}"
- "supp (TCONST i) = {atom i}"
- "supp (TAPP A M) = supp A \<union> supp M"
- "supp (CONS i) = {atom i}"
- "supp (VAR x) = {atom x}"
- "supp (APP M N) = supp M \<union> supp N"
-apply (simp_all add: supp_def permute_ktt)
-apply (simp_all only: kind_ty_trm_INJECT)
-apply (simp_all only: supp_at_base[simplified supp_def])
-apply (simp_all add: Collect_imp_eq Collect_neg_eq)
-done
+lemma supp_eqs:
+  "supp TYP = {}"
+  "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
+  "supp (TCONST i) = {atom i}"
+  "supp (TAPP A M) = supp A \<union> supp M"
+  "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
+  "supp (CONS i) = {atom i}"
+  "supp (VAR x) = {atom x}"
+  "supp (APP M N) = supp M \<union> supp N"
+  "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
+  apply(simp_all (no_asm) add: supp_def)
+  apply(simp_all only: kind_ty_trm_INJECT Abs_eq_iff alpha_gen)
+  apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])
+  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)
+  apply(simp_all add: supp_at_base[simplified supp_def])
+  done
 
 lemma supp_fv:
- "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_rkind_rty_rtrm_easy)
-apply (simp_all add: fv_kind_ty_trm)
-apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
-apply(simp only: supp_Abs)
-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: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
-apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)")
-apply(simp add: supp_Abs)
-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] insert_eqvt empty_eqvt atom_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)")
-apply(simp add: supp_Abs)
-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] insert_eqvt empty_eqvt atom_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
-done
-
-(* Not needed anymore *)
-lemma supp_kpi: "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
-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
+  "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 (no_asm) only: supp_eqs fv_kind_ty_trm)
+  apply(simp_all)
+  apply(subst supp_eqs)
+  apply(simp_all add: supp_Abs)
+  apply(subst supp_eqs)
+  apply(simp_all add: supp_Abs)
+  apply(subst supp_eqs)
+  apply(simp_all add: supp_Abs)
+  done
 
 lemma supp_rkind_rty_rtrm:
- "supp TYP = {}"
- "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
- "supp (TCONST i) = {atom i}"
- "supp (TAPP A M) = supp A \<union> supp M"
- "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
- "supp (CONS i) = {atom i}"
- "supp (VAR x) = {atom x}"
- "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_rkind_rty_rtrm_easy)
-apply (simp_all only: supp_fv fv_kind_ty_trm)
-done
+  "supp TYP = {}"
+  "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
+  "supp (TCONST i) = {atom i}"
+  "supp (TAPP A M) = supp A \<union> supp M"
+  "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
+  "supp (CONS i) = {atom i}"
+  "supp (VAR x) = {atom x}"
+  "supp (APP M N) = supp M \<union> supp N"
+  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
+  by (simp_all only: supp_fv fv_kind_ty_trm)
 
 end