# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267009615 -3600
# Node ID 605a0ebe87da7a97cdf08a9ad1181f23189684be
# Parent  14cf3d2b0e16c14fa0776ae099e229f2a25b0e44
Regularize the proofs about finite support.

diff -r 14cf3d2b0e16 -r 605a0ebe87da Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 11:28:34 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 12:06:55 2010 +0100
@@ -165,6 +165,37 @@
 
 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
+lemma supports:
+  "{} supports TYP"
+  "(supp (atom i)) supports (TCONST i)"
+  "(supp A \<union> supp M) supports (TAPP A M)"
+  "(supp (atom i)) supports (CONS i)"
+  "(supp (atom x)) supports (VAR x)"
+  "(supp M \<union> supp N) supports (APP M N)"
+  "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"
+  "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"
+  "(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)"
+apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
+apply(rule_tac [!] allI)+
+apply(rule_tac [!] impI)
+apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
+apply(simp_all add: fresh_atom)
+done
+
+lemma kind_ty_trm_fs:
+  "finite (supp (x\<Colon>kind))"
+  "finite (supp (y\<Colon>ty))"
+  "finite (supp (z\<Colon>trm))"
+apply(induct x and y and z rule: kind_ty_trm_inducts)
+apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
+apply(simp_all add: supp_atom)
+done
+
+instance kind and ty and trm :: fs
+apply(default)
+apply(simp_all only: kind_ty_trm_fs)
+done
+
 lemma supp_rkind_rty_rtrm_easy:
  "supp TYP = {}"
  "supp (TCONST i) = {atom i}"
@@ -178,46 +209,6 @@
 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 done
 
-lemma supp_bind:
-  "(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
-  "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
-  "(supp (atom na, (ty, rtrm))) supports (LAM ty na rtrm)"
-apply(simp_all add: supports_def)
-apply(fold fresh_def)
-apply(simp_all add: fresh_Pair swap_fresh_fresh)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
-apply(simp_all add: fresh_atom)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
-apply(simp_all add: fresh_atom)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
-apply(simp_all add: fresh_atom)
-done
-
-lemma kind_ty_trm_fs:
-  "finite (supp (x\<Colon>kind))"
-  "finite (supp (y\<Colon>ty))"
-  "finite (supp (z\<Colon>trm))"
-apply(induct x and y and z rule: kind_ty_trm_inducts)
-apply(simp_all add: supp_rkind_rty_rtrm_easy)
-apply(rule supports_finite)
-apply(rule supp_bind(1))
-apply(simp add: supp_Pair supp_atom)
-apply(rule supports_finite)
-apply(rule supp_bind(2))
-apply(simp add: supp_Pair supp_atom)
-apply(rule supports_finite)
-apply(rule supp_bind(3))
-apply(simp add: supp_Pair supp_atom)
-done
-
-instance kind and ty and trm :: fs
-apply(default)
-apply(simp_all only: kind_ty_trm_fs)
-done
-
 lemma supp_fv:
  "supp t1 = fv_kind t1"
  "supp t2 = fv_ty t2"
@@ -226,7 +217,7 @@
 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 add: supp_Abs Set.Un_commute)
+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)
@@ -234,7 +225,7 @@
 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 Set.Un_commute)
+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)
@@ -242,7 +233,7 @@
 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 Set.Un_commute)
+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)
@@ -252,7 +243,7 @@
 done
 
 (* Not needed anymore *)
-lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
+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)