--- a/Nominal/Ex/CoreHaskell.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/CoreHaskell.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -86,6 +86,10 @@
 
 (* generated theorems *)
 
+thm core_haskell.perm_bn_alpha
+thm core_haskell.perm_bn_simps
+thm core_haskell.bn_finite
+
 thm core_haskell.distinct
 thm core_haskell.induct
 thm core_haskell.exhaust

--- a/Nominal/Ex/Ex1.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Ex1.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -20,6 +20,11 @@
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+thm foo_bar.perm_bn_alpha
+thm foo_bar.perm_bn_simps
+thm foo_bar.bn_finite
+
+thm foo_bar.eq_iff
 thm foo_bar.distinct
 thm foo_bar.induct
 thm foo_bar.inducts

--- a/Nominal/Ex/Foo1.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -35,6 +35,9 @@
 | "bn4 (BNil) = {}"
 | "bn4 (BAs a as) = {atom a} \<union> bn4 as"
 
+thm foo.perm_bn_alpha
+thm foo.perm_bn_simps
+thm foo.bn_finite
 
 thm foo.distinct
 thm foo.induct

--- a/Nominal/Ex/Foo2.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -24,7 +24,9 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+thm foo.perm_bn_alpha
 thm foo.perm_bn_simps
+thm foo.bn_finite
 
 thm foo.distinct
 thm foo.induct
@@ -45,19 +47,23 @@
   shows "alpha_bn as (permute_bn p as)"
 apply(induct as rule: foo.inducts(2))
 apply(auto)[5]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
+apply(simp only: foo.perm_bn_simps)
+apply(simp only: foo.eq_iff)
+apply(simp only: foo.perm_bn_simps)
+apply(simp only: foo.eq_iff refl)
+apply(simp)
 done
 
 lemma tt1:
   shows "(p \<bullet> bn as) = bn (permute_bn p as)"
 apply(induct as rule: foo.inducts(2))
 apply(auto)[5]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
+apply(simp only: foo.perm_bn_simps foo.bn_defs)
+apply(perm_simp)
+apply(simp only:)
+apply(simp only: foo.perm_bn_simps foo.bn_defs)
+apply(perm_simp add: foo.fv_bn_eqvt)
+apply(simp only:)
 done
 
 text {*

--- a/Nominal/Ex/Modules.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Modules.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -63,6 +63,10 @@
 | "Cbinders (SVal v T) = {atom v}"
 
 
+thm modules.perm_bn_alpha
+thm modules.perm_bn_simps
+thm modules.bn_finite
+
 thm modules.distinct
 thm modules.induct
 thm modules.exhaust

--- a/Nominal/Ex/Multi_Recs2.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -49,6 +49,54 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
+
+
+thm fun_recs.perm_bn_alpha
+thm fun_recs.perm_bn_simps
+thm fun_recs.bn_finite
+thm fun_recs.inducts
+thm fun_recs.distinct
+thm fun_recs.induct
+thm fun_recs.inducts
+thm fun_recs.exhaust
+thm fun_recs.fv_defs
+thm fun_recs.bn_defs
+thm fun_recs.perm_simps
+thm fun_recs.eq_iff
+thm fun_recs.fv_bn_eqvt
+thm fun_recs.size_eqvt
+thm fun_recs.supports
+thm fun_recs.fsupp
+thm fun_recs.supp
+
+term alpha_b_fnclause
+term alpha_b_fnclauses
+term alpha_b_lrb
+term alpha_b_lrbs
+term alpha_b_pat
+
+term alpha_b_fnclause_raw
+term alpha_b_fnclauses_raw
+term alpha_b_lrb_raw
+term alpha_b_lrbs_raw
+term alpha_b_pat_raw
+
+lemma uu1:
+  fixes as0::exp  and as1::fnclause
+  shows "(\<lambda>x::exp. True) (as0::exp)"
+  and   "alpha_b_fnclause as1 (permute_b_fnclause p as1)"
+  and   "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)"
+  and   "alpha_b_lrb as3 (permute_b_lrb p as3)"
+  and   "alpha_b_lrbs as4 (permute_b_lrbs p as4)"
+  and   "alpha_b_pat as5 (permute_b_pat p as5)"
+apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts)
+apply(simp_all)
+apply(simp only: fun_recs.perm_bn_simps)
+apply(simp only: fun_recs.eq_iff)
+apply(simp)
+oops
+
+
 thm fun_recs.distinct
 thm fun_recs.induct
 thm fun_recs.inducts

--- a/Nominal/Nominal2.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -146,13 +146,9 @@
 ML {*
 (** definition of the raw binding functions **)
 
-(* TODO: needs cleaning *)
-fun find [] _ = error ("cannot find element")
-  | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
-
-fun prep_bn_info lthy dt_names dts eqs = 
+fun prep_bn_info lthy dt_names dts bn_funs eqs = 
 let
-  fun aux eq = 
+  fun process_eq eq = 
   let
     val (lhs, rhs) = eq
       |> HOLogic.dest_Trueprop
@@ -162,32 +158,32 @@
     val (ty_name, _) = dest_Type (domain_type ty)
     val dt_index = find_index (fn x => x = ty_name) dt_names
     val (cnstr_head, cnstr_args) = strip_comb cnstr    
+    val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))
     val rhs_elements = strip_bn_fun lthy cnstr_args rhs
   in
-    (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
+    ((bn_fun, dt_index), (cnstr_name, rhs_elements))
   end
 
-  fun order dts i ts = 
+  (* order according to constructor names *)
+  fun cntrs_order ((bn, dt_index), data) = 
   let
-    val dt = nth dts i
-    val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
-    val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
+    val dt = nth dts dt_index                      
+    val cts = (fn (_, _, _, x) => x) dt     
+    val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  
   in
-    map (find ts') cts
+    (bn, (bn, dt_index, order (op=) ct_names data))
   end
+ 
+in
+  eqs
+  |> map process_eq 
+  |> AList.group (op=)      (* eqs grouped according to bn_functions *)
+  |> map cntrs_order        (* inner data ordered according to constructors *)
+  |> order (op=) bn_funs    (* ordered according to bn_functions *)
+end
+*}
 
-  val unordered = AList.group (op=) (map aux eqs)
-  val unordered' = map (fn (x, y) =>  (x, AList.group (op=) y)) unordered
-  val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
-  val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
-
-  (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*)
-  (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
-  (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
-in
-  ordered'
-end
-
+ML {*
 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
   if null raw_bn_funs 
   then ([], [], [], [], lthy)
@@ -203,7 +199,7 @@
       val raw_bn_eqs = the simps
 
       val raw_bn_info = 
-        prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+        prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
     in
       (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
     end
@@ -269,6 +265,8 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs))
+ 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
 
@@ -311,6 +309,12 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
+  (*
+  val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns))
+  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info))
+  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info))
+  *)
+
   (* defining the permute_bn functions *)
   val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = 
     if get_STEPS lthy3a > 2
@@ -489,6 +493,14 @@
   val qalpha_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
+  (*
+  val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info))
+  val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs))
+  val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns))
+  val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns))
+  val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms))
+  *)
+
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
 
@@ -499,7 +511,7 @@
     map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
      
 
-  val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) = 
+  val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)= 
     if get_STEPS lthy > 24
     then 
       lthy7
@@ -527,6 +539,7 @@
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
+  val qperm_bns = map #qconst qperm_bns_info
 
   (* lifting of the theorems *)
   val _ = warning "Lifting of Theorems"
@@ -586,12 +599,6 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
-  (* proving that the qbn result is finite *)
-  val qbn_finite_thms =
-    if get_STEPS lthy > 33
-    then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
-    else []
-
   (* postprocessing of eq and fv theorems *)
 
   val qeq_iffs' = qeq_iffs
@@ -612,6 +619,18 @@
     |> map (fn thm => thm RS transform_thm) 
     |> map (simplify (HOL_basic_ss addsimps transform_thms))
 
+  (* proving that the qbn result is finite *)
+  val qbn_finite_thms =
+    if get_STEPS lthy > 33
+    then prove_bns_finite qtys qbns qinduct qbn_defs lthyC
+    else []
+
+  (* proving that perm_bns preserve alpha *)
+  val qperm_bn_alpha_thms = @{thms TrueI}
+  (*  if get_STEPS lthy > 33
+    then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC
+    else []*)
+
 
   (* noting the theorems *)  
 
@@ -639,6 +658,7 @@
      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
+     ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)

--- a/Nominal/nominal_dt_alpha.ML	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Mon Dec 06 14:24:17 2010 +0000
@@ -247,6 +247,8 @@
       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
     val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
 
+    val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names))
+
     val (alphas, lthy') = Inductive.add_inductive_i
        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
         coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}

--- a/Nominal/nominal_dt_supp.ML	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Dec 06 14:24:17 2010 +0000
@@ -17,7 +17,8 @@
     thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
 
   val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
-
+  val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+    Proof.context -> thm list
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -150,12 +151,6 @@
 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
   prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
 
-fun p_tac msg i = 
-  if false then print_tac ("ptest: " ^ msg) else all_tac
-
-fun q_tac msg i = 
-  if true then print_tac ("qtest: " ^ msg) else all_tac
-
 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
   fv_bn_eqvts qinduct bclausess ctxt =
   let
@@ -206,7 +201,29 @@
     val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
       @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
   in
-    induct_prove qtys props qinduct (K (ss_tac ORELSE' (K no_tac))) ctxt
+    induct_prove qtys props qinduct (K ss_tac) ctxt
+  end
+
+fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs ctxt =
+  let 
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+    val p = Free (p, @{typ perm})
+
+    fun mk_goal qperm_bn alpha_bn =
+      let
+        val arg_ty = domain_type (fastype_of alpha_bn)
+      in
+        (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
+      end
+
+    val props = map2 mk_goal qperm_bns alpha_bns
+    val ss_tac = (K (print_tac "test")) THEN' 
+      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs))
+  in
+    @{thms TrueI}
+    (*induct_prove qtys props qinduct (K ss_tac) ctxt'
+    |> ProofContext.export ctxt' ctxt
+    |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*)
   end
 
 

--- a/Nominal/nominal_library.ML	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Dec 06 14:24:17 2010 +0000
@@ -6,11 +6,14 @@
 
 signature NOMINAL_LIBRARY =
 sig
-  val is_true: term -> bool
+  val last2: 'a list -> 'a * 'a
+  val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
 
-  val last2: 'a list -> 'a * 'a
+  val is_true: term -> bool
+ 
+  val dest_listT: typ -> typ
 
-  val dest_listT: typ -> typ
+  val mk_id: term -> term
 
   val size_const: typ -> term 
 
@@ -91,17 +94,30 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
+(* orders an AList according to keys *)
+fun order eq keys list = 
+  map (the o AList.lookup eq list) keys
 
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
+
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
 fun dest_listT (Type (@{type_name list}, [T])) = T
   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
 
+fun mk_id trm =
+  let 
+    val ty = fastype_of trm
+  in
+    Const (@{const_name id}, ty --> ty) $ trm
+  end
+
+
 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
 
 fun sum_case_const ty1 ty2 ty3 =