--- a/Quot/Nominal/Abs.thy	Wed Feb 03 12:06:10 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Wed Feb 03 12:13:22 2010 +0100
@@ -138,7 +138,7 @@
   apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
-  apply(rule conjI)+
+  apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
   apply(simp add: a[symmetric] atom_eqvt eqvts)
   apply(rule conjI)

--- a/Quot/Nominal/LFex.thy	Wed Feb 03 12:06:10 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 03 12:13:22 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
 

--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:06:10 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:13:22 2010 +0100
@@ -121,7 +121,29 @@
   shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
   apply (induct t s rule: alpha1.inducts)
   apply (simp_all add:eqvts alpha1_inj)
-  sorry
+  apply (erule exE)
+  apply (rule_tac x="pi \<bullet> pia" in exI)
+  apply (simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+  apply(simp add: atom_eqvt eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: eqvts atom_eqvt)
+  apply(simp add: permute_eqvt[symmetric])
+  apply (erule exE)
+  apply (rule_tac x="pi \<bullet> pia" in exI)
+  apply (simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+  apply(simp add: atom_eqvt eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: eqvts atom_eqvt)
+  apply(simp add: permute_eqvt[symmetric])
+  done
 
 lemma alpha1_equivp: "equivp alpha1" 
   sorry
@@ -331,7 +353,7 @@
 apply(simp (no_asm) add: supp_def)
 apply(simp add: alpha1_INJ)
 apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen.simps)
+apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
@@ -349,7 +371,7 @@
   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
   shows   "P a rtrma"
-
+sorry
 
 section {*** lets with single assignments ***}
 
@@ -628,4 +650,85 @@
 
 
 
+
+
+
+
+
+datatype rtrm5 =
+  rVr5 "name"
+| rAp5 "rtrm5" "rtrm5"
+| rLt5 "rlts" "rtrm5"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
+
+primrec
+  bv5
+where
+  "bv5 rLnil = {}"
+| "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+primrec
+  rfv_trm5 and rfv_lts
+where
+  "rfv_trm5 (rVr5 n) = {atom n}"
+| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
+| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)"
+| "rfv_lts (rLnil) = {}"
+| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
+
+instantiation
+  rtrm5 and rlts :: pt
+begin
+
+primrec
+  permute_rtrm5 and permute_rlts
+where
+  "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
+| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
+| "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)"
+| "permute_rlts pi (rLnil) = rLnil"
+| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
+
+lemma pt_rtrm5_zero:
+  fixes t::rtrm5
+  and   l::rlts
+  shows "0 \<bullet> t = t"
+  and   "0 \<bullet> l = l"
+apply(induct t and l rule: rtrm5_rlts.inducts)
+apply(simp_all)
+done
+
+lemma pt_rtrm5_plus:
+  fixes t::rtrm5
+  and   l::rlts
+  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+  and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
+apply(induct t and l rule: rtrm5_rlts.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
+done
+
 end
+
+inductive
+  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
+and
+  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
+| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
+| a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
+             (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
+              (pi \<bullet> (bv5 l1) = bv5 l2))
+        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
+| a4: "rLnil \<approx>l rLnil"
+| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+
+thm a3[simplified alpha_gen]
+end

--- a/Quot/Nominal/Test.thy	Wed Feb 03 12:06:10 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Feb 03 12:13:22 2010 +0100
@@ -131,7 +131,7 @@
   fun fv_var (t as Free (s, (ty as Type (tyS, _)))) =
     if is_atom tyS then HOLogic.mk_set ty [t] else
     if (Long_Name.base_name tyS) mem dt_names then
-      fv_bds s bds (Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
+      fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
     HOLogic.mk_set @{typ name} []
   val fv_eq =
     if null vars then HOLogic.mk_set @{typ name} []
@@ -155,7 +155,7 @@
 
 ML {*
 fun fv_dt lthy dt_names (((s2, s3), syn), constrs) =
-    map (fv_constr lthy ("fv_" ^ Binding.name_of s3) dt_names) constrs
+    map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs
  |> separate "\n"
  |> implode
 *}