--- a/Nominal/Fv.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -33,7 +33,7 @@
 *)
 
 (*
-The overview of the generation of free variables:
+An overview of the generation of free variables:
 
 1) fv_bn functions are generated only for the non-recursive binds.
 
@@ -76,6 +76,10 @@
    - for nominal datatype ty' return: fv_ty' x
 *)
 
+(*
+An overview of the generation of alpha-equivalence:
+*)
+
 ML {*
 fun is_atom thy typ =
   Sign.of_sort thy (typ, @{sort at})

--- a/Nominal/LFex.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -45,7 +45,7 @@
   "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 kind_ty_trm_perm)
+  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])
@@ -58,7 +58,7 @@
 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 kind_ty_trm_fv)
+  apply(simp_all (no_asm) only: supp_eqs)
   apply(simp_all)
   apply(simp_all add: supp_eqs)
   apply(simp_all add: supp_Abs)
@@ -74,7 +74,7 @@
   "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 kind_ty_trm_fv)
+apply (simp_all add: supp_fv)
 
 end
 

--- a/Nominal/Parser.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -381,15 +381,18 @@
   val q_name = space_implode "_" qty_names;
   val _ = tracing "Lifting induction";
   val q_induct = lift_thm lthy13 induct;
+  fun note_simp_suffix s th ctxt =
+    snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s),
+      [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
   val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14;
-  val q_perm = map (lift_thm lthy14) raw_perm_def;
-  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a;
+  val q_perm = map (lift_thm lthy14) raw_perm_def; 
+  val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm lthy15) fv_def;
-  val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
+  val lthy16 = note_simp_suffix "fv" q_fv lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
-  val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+  val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1
@@ -400,7 +403,7 @@
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
   val q_dis = map (lift_thm lthy18) rel_dists;
-  val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
+  val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;

--- a/Nominal/Test.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -23,13 +23,13 @@
 lemma finite_fv:
   shows "finite (fv_lm t)"
 apply(induct t rule: lm_induct)
-apply(simp_all add: lm_fv)
+apply(simp_all)
 done
 
 lemma supp_fn:
   shows "supp t = fv_lm t"
 apply(induct t rule: lm_induct)
-apply(simp_all add: lm_fv)
+apply(simp_all)
 apply(simp only: supp_def)
 apply(simp only: lm_perm)
 apply(simp only: lm_eq_iff)
@@ -77,7 +77,7 @@
     apply(erule exE)
     apply(rule_tac t="p \<bullet> Lm name lm" and 
                    s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp)
+    apply(simp del: lm_perm)
     apply(subst lm_perm)
     apply(subst (2) lm_perm)
     apply(rule flip_fresh_fresh)
@@ -85,7 +85,7 @@
     apply(simp only: supp_fn')
     apply(simp)
     apply(simp add: fresh_Pair)
-    apply(simp add: lm_perm)
+    apply(simp)
     apply(rule a3)
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
@@ -130,7 +130,7 @@
   shows "supp t = fv_lam t" 
   and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
 apply(induct t and bp rule: lam_bp_inducts)
-apply(simp_all add: lam_bp_fv)
+apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
@@ -218,7 +218,7 @@
   shows "supp t = fv_lam' t" 
   and "supp bp = fv_bp' bp"
 apply(induct t and bp rule: lam'_bp'_inducts)
-apply(simp_all add: lam'_bp'_fv)
+apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
@@ -304,7 +304,7 @@
   shows "supp t = fv_trm' t" 
   and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
 apply(induct t and bp rule: trm'_pat'_inducts)
-apply(simp_all add: trm'_pat'_fv)
+apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
@@ -439,7 +439,7 @@
   shows "supp T = fv_t T" 
   and   "supp S = fv_tyS S"
 apply(induct T and S rule: t_tyS_inducts)
-apply(simp_all add: t_tyS_fv)
+apply(simp_all)
 (* VarTS case *)
 apply(simp only: supp_def)
 apply(simp only: t_tyS_perm)
@@ -519,11 +519,6 @@
 thm trm3_rassigns3_induct
 thm trm3_rassigns3_distinct
 
-(* compat should be
-compat (ANil) pi (PNil) \<equiv> TRue
-compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts'
-*)
-
 (* example 5 from Terms.thy *)
 
 nominal_datatype trm5 =

--- a/Nominal/TySch.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -36,7 +36,7 @@
   shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
   apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts)
+  apply(simp add: alpha_gen fresh_star_def eqvts)
   apply auto
   done
 
@@ -44,7 +44,7 @@
   shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
 oops
 
 lemma
@@ -53,7 +53,7 @@
   using a
   apply(simp add: t_tyS_eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
   apply auto
   done
 

--- a/TODO	Thu Mar 18 11:37:10 2010 +0100
+++ b/TODO	Thu Mar 18 12:09:59 2010 +0100
@@ -3,13 +3,9 @@
 - case names for "weak" induction rules (names of the 
 constructors); see page 61/62 and 170 in Tutorial
 
-- <type>_perm rules should be added to the simplifier;
-  maybe <type>_perm whould be called permute_<type>.simps;
+- maybe <type>_perm whould be called permute_<type>.simps;
   that would conform with the terminology in Nominal2
 
-- <type>_fv / <type>_bn / <type>_distinct should also be 
-  added to the simplifier
-
 
 Bigger things: