--- 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;