--- a/Nominal-General/nominal_library.ML	Mon Jul 26 09:19:28 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Tue Jul 27 09:09:02 2010 +0200
@@ -112,7 +112,7 @@
   | mk_union (@{term "{}::atom set"}, t2) = t2
   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
  
-fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
+fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
 
 
 

--- a/Nominal/Ex/SingleLet.thy	Mon Jul 26 09:19:28 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 27 09:09:02 2010 +0200
@@ -21,6 +21,14 @@
 where
   "bn (As x y t) = {atom x}"
 
+thm alpha_bn_imps
+thm distinct
+thm eq_iff
+thm fv_defs
+thm perm_simps
+thm perm_laws
+
+
 typ trm
 typ assg
 term Var 
@@ -28,25 +36,35 @@
 term Baz
 term bn
 term fv_trm
+term alpha_bn
 
-lemma a1:
-  shows "alpha_trm_raw x1 y1 \<Longrightarrow> True"
-  and   "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2"
-  and   "alpha_bn_raw x3 y3 \<Longrightarrow> True"
-apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(rule TrueI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-sorry
+
 
 lemma a2:
   shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
-apply(simp_all only: alphas prod_alpha_def)
-apply(auto)[1]
-apply(auto simp add: prod_alpha_def)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
+-- ""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc)
+-- ""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
+apply(simp only: Un_insert_left Un_empty_right Un_empty_left)
+-- ""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
+--""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
+apply(simp (no_asm) only: simp_thms)
+--""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
 done
 
 lemma [quot_respect]: 

--- a/Nominal/NewParser.thy	Mon Jul 26 09:19:28 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Jul 27 09:09:02 2010 +0200
@@ -320,14 +320,14 @@
 
   (* definitions of raw permutations *)
   val _ = warning "Definition of raw permutations";
-  val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
+  val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
     if get_STEPS lthy0 > 1 
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
   val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-  val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2
+  val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2
 
   val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy
@@ -371,7 +371,7 @@
   val _ = warning "Proving equivariance";
   val bn_eqvt = 
     if get_STEPS lthy > 6
-    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
+    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4
     else raise TEST lthy4
 
   (* noting the bn_eqvt lemmas in a temprorary theory *)
@@ -380,7 +380,7 @@
 
   val fv_eqvt = 
     if get_STEPS lthy > 7
-    then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) 
+    then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) 
        (Local_Theory.restore lthy_tmp)
     else raise TEST lthy4
  
@@ -423,6 +423,11 @@
     then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 
     else raise TEST lthy6
   
+  (* auxiliary lemmas for respectfulness proofs *)
+  (* HERE *)
+  
+
+
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
@@ -452,8 +457,10 @@
   val qfv_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs  raw_fv_bns
 
-  (* TODO: probably also needs alpha_bn *)
-  val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = 
+  val qalpha_bns_descr = 
+    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
+
+  val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
     if get_STEPS lthy > 15
     then 
       lthy7
@@ -461,24 +468,24 @@
       ||>> qconst_defs qtys qbns_descr 
       ||>> qconst_defs qtys qfvs_descr
       ||>> qconst_defs qtys qfv_bns_descr
+      ||>> qconst_defs qtys qalpha_bns_descr
     else raise TEST lthy7
 
   val qconstrs = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
+  val qalpha_bns = map #qconst qalpha_bns_info
 
-  (* respectfulness proofs *)
-  
   (* HERE *)
 
   val (_, lthy8') = lthy8
      |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
      ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) 
      ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
-     ||>> Local_Theory.note ((@{binding "perm_defs"}, []), raw_perm_defs) 
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
-
+     ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
+     ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
   
   val _ = 
     if get_STEPS lthy > 16
@@ -541,7 +548,7 @@
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
   (* use Local_Theory.theory_result *)
-  val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy;
+  val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy;
   val lthy13 = Theory_Target.init NONE thy';
   
   val q_name = space_implode "_" qty_names;
@@ -558,7 +565,7 @@
     [Rule_Cases.name constr_names q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
-  val q_perm = map (lift_thm qtys lthy14) raw_perm_defs;
+  val q_perm = map (lift_thm qtys lthy14) raw_perm_simps;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;

--- a/Nominal/nominal_dt_rawfuns.ML	Mon Jul 26 09:19:28 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jul 27 09:09:02 2010 +0200
@@ -213,6 +213,8 @@
 
 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
 let
+  val _ = tracing ("bclausesss\n" ^ cat_lines (map (cat_lines o map PolyML.makestring) bclausesss))
+
   val fv_names = prefix_dt_names descr sorts "fv_"
   val fv_arg_tys = all_dtyps descr sorts
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;