# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265014592 -3600
# Node ID b7d259ded92ee0fae8892f10dfd4db751b1d9aa7
# Parent  2fcd18e7bb182dcbcf2cebb571d901d77450b2c1
Ported LF to the generic lambda and solved the simpler _supp cases.

diff -r 2fcd18e7bb18 -r b7d259ded92e Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Sat Jan 30 12:12:52 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 01 09:56:32 2010 +0100
@@ -150,8 +150,6 @@
 apply (simp only: akind_aty_atrm.intros)
 done
 
-(* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *)
-
 lemma rfv_eqvt[eqvt]:
   "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
   "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
@@ -591,7 +589,7 @@
 apply simp_all
 sorry
 
-lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
+lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
 apply (subst supp_Pair[symmetric])
 unfolding supp_def
 apply (simp add: permute_set_eq)
@@ -602,11 +600,23 @@
 apply (unfold supp_def)
 sorry
 
+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)
+sorry
+
+instance KIND and TY and TRM :: fs
+apply(default)
+apply(simp_all only: KIND_TY_TRM_fs)
+done
+
 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
 apply(subst supp_kpi_pre)
-thm supp_Abs
-(*apply(simp add: supp_Abs)*)
-sorry
+apply(subst supp_Abst)
+apply (simp only: Set.Un_commute)
+done
 
 lemma supp_kind_ty_trm:
  "supp TYP = {}"
@@ -621,7 +631,12 @@
 apply -
 apply (simp add: supp_def)
 apply (simp add: supp_kpi)
-apply (simp add: supp_def) (* need ty.distinct lifted *)
+apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base)
+apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq)
+defer
+apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base)
+apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base)
+apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq)
 sorry
 
 
diff -r 2fcd18e7bb18 -r b7d259ded92e Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Sat Jan 30 12:12:52 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 09:56:32 2010 +0100
@@ -548,7 +548,7 @@
 
 lemma app_supp:
   shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
-apply(simp only: permute_lam supp_def lam_inject)
+apply(simp only: supp_def lam_inject)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done