diff -r 74888979e9cd -r 4355eb3b7161 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/LFex.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -22,57 +22,7 @@
   | App "trm" "trm"
   | Lam "ty" n::"name" t::"trm" bind n in t
 
-lemma ex_out: 
-  "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
-  "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
-  "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
-  "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
-apply (blast)+
-done
-
-lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
-by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-
-lemma supp_eqs:
-  "supp Type = {}"
-  "supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)"
-  "supp (TConst i) = {atom i}"
-  "supp (TApp A M) = supp A \<union> supp M"
-  "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)"
-  "supp (Const i) = {atom i}"
-  "supp (Var x) = {atom x}"
-  "supp (App M N) = supp M \<union> supp N"
-  "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
-  apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)
-  apply(simp_all only: kind_ty_trm.eq_iff Abs_eq_iff alpha_gen)
-  apply(simp_all only: ex_out)
-  apply(simp_all only: eqvts[symmetric])
-  apply(simp_all only: Collect_neg_conj)
-  apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc)
-  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc)
-  apply(simp_all add: Un_left_commute)
-  done
-
-lemma supp_fv:
-  "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
-  apply(induct rule: kind_ty_trm.induct)
-  apply(simp_all (no_asm) only: supp_eqs)
-  apply(simp_all)
-  apply(simp_all add: supp_eqs)
-  apply(simp_all add: supp_Abs)
-  done
-
-lemma supp_kind_ty_trm:
-  "supp Type = {}"
-  "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 (Const 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 add: supp_fv)
+thm kind_ty_trm.supp
 
 end