--- a/Nominal/NewParser.thy	Fri Jul 02 15:34:46 2010 +0100
+++ b/Nominal/NewParser.thy	Wed Jul 07 09:34:00 2010 +0100
@@ -336,7 +336,7 @@
   val _ = warning "Definition of raw fv-functions";
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
+  val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
     then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
     else raise TEST lthy3
@@ -370,7 +370,7 @@
   val _ = warning "Proving equivariance";
   val bn_eqvt = 
     if get_STEPS lthy > 6
-    then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
+    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
     else raise TEST lthy4
 
   (* noting the bn_eqvt lemmas in a temprorary theory *)
@@ -437,25 +437,38 @@
   val qtys = map #qtyp qty_infos
   
   (* defining of quotient term-constructors, binding functions, free vars functions *)
-  val qconstr_descr = 
+  val _ = warning "Defining the quotient constnats"
+  val qconstrs_descr = 
     flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
     |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs
 
   val qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs
+    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
 
   val qfvs_descr = 
-    map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs
+    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
+  val qfv_bns_descr = 
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs  raw_fv_bns
 
-  val (qs, lthy8) = 
+  (* TODO: probably also needs alpha_bn *)
+  val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = 
     if get_STEPS lthy > 15
-    then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7
+    then 
+      lthy7
+      |> qconst_defs qtys qconstrs_descr 
+      ||>> qconst_defs qtys qbns_descr 
+      ||>> qconst_defs qtys qfvs_descr
+      ||>> qconst_defs qtys qfv_bns_descr
     else raise TEST lthy7
 
-  val _ = tracing ("raw fvs  " ^ commas (map @{make_string} raw_fvs))
-  val _ = tracing ("raw fv_bns  " ^ commas (map @{make_string} raw_fv_bns))
+  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
 
+  (* respectfulness proofs *)
+  
   (* HERE *)
   
   val _ = 
@@ -464,18 +477,10 @@
   
   (* old stuff *)
 
-  val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
-  val raw_consts =
-    flat (map (fn (i, (_, _, l)) =>
-      map (fn (cname, dts) =>
-        Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
-          Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts
-  val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7;
   val _ = warning "Proving respects";
 
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bn_funs ~~ bn_nos;
+  val bns = raw_bns ~~ bn_nos;
 
   val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
@@ -504,27 +509,36 @@
     let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-    const_rsp_tac) raw_consts lthy11a
+    const_rsp_tac) all_raw_constrs lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
-  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12;
+  val (qfv_info, lthy12a) = qconst_defs qtys dd lthy12;
+  val qfv_ts = map #qconst qfv_info
+  val qfv_defs = map #def qfv_info
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs
-  val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a;
+  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns
+  val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a;
+  val qbn_ts = map #qconst qbn_info
+  val qbn_defs = map #def qbn_info
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms
-  val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b;
+  val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b;
+  val qalpha_bn_trms = map #qconst qalpha_info
+  val qalphabn_defs = map #def qalpha_info
+  
   val _ = warning "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   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
-  val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy;
+  (* use Local_Theory.theory_result *)
+  val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
+  
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
-  val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
+  val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;
   val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
@@ -556,7 +570,7 @@
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";
-  val supports = map (prove_supports lthy20 q_perm) consts;
+  val supports = map (prove_supports lthy20 q_perm) qconstrs;
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
   val thy3 = Local_Theory.exit_global lthy20;
   val _ = warning "Instantiating FS";

--- a/Nominal/Perm.thy	Fri Jul 02 15:34:46 2010 +0100
+++ b/Nominal/Perm.thy	Wed Jul 07 09:34:00 2010 +0100
@@ -24,38 +24,4 @@
 ML {* open Nominal_Dt_Quot *}
 
 
-(* permutations for quotient types *)
-
-ML {*
-fun quotient_lift_consts_export qtys spec ctxt =
-let
-  val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt;
-  val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result);
-  val morphism = ProofContext.export_morphism ctxt' ctxt;
-  val ts = map (Morphism.term morphism) ts_loc
-  val defs = Morphism.fact morphism defs_loc
-in
-  (ts, defs, ctxt')
 end
-*}
-
-
-
-ML {*
-fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
-let
-  val lthy =
-    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-  val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
-  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
-  fun tac _ =
-    Class.intro_classes_tac [] THEN
-    (ALLGOALS (resolve_tac lifted_thms))
-  val lthy'' = Class.prove_instantiation_instance tac lthy'
-in
-  Local_Theory.exit_global lthy''
-end
-*}
-
-
-end

--- a/Nominal/nominal_dt_quot.ML	Fri Jul 02 15:34:46 2010 +0100
+++ b/Nominal/nominal_dt_quot.ML	Wed Jul 07 09:34:00 2010 +0100
@@ -12,6 +12,9 @@
 
   val qconst_defs: typ list -> (string  * term * mixfix) list -> local_theory -> 
     Quotient_Info.qconsts_info list * local_theory
+
+  val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> 
+    thm list -> theory -> theory
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -38,6 +41,21 @@
 end
 
 
+(* defines the quotient permutations *)
+fun qperm_defs qtys full_tnames name_term_pairs thms thy =
+let
+  val lthy =
+    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+  val (_, lthy') = qconst_defs qtys name_term_pairs lthy;
+  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
+  fun tac _ =
+    Class.intro_classes_tac [] THEN
+    (ALLGOALS (resolve_tac lifted_thms))
+  val lthy'' = Class.prove_instantiation_instance tac lthy'
+in
+  Local_Theory.exit_global lthy''
+end
+
 
 end (* structure *)
 

--- a/Paper/Paper.thy	Fri Jul 02 15:34:46 2010 +0100
+++ b/Paper/Paper.thy	Wed Jul 07 09:34:00 2010 +0100
@@ -90,7 +90,7 @@
   we would like to regard the following two type-schemes as $\alpha$-equivalent
   %
   \begin{equation}\label{ex1}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"} 
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. x \<rightarrow> y"} 
   \end{equation}
 
   \noindent
@@ -214,8 +214,8 @@
   The scope of the binding is indicated by labels given to the types, for
   example @{text "s::trm"}, and a binding clause, in this case
   \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-  clause states to bind in @{text s} all the names the function @{text
-  "bn(as)"} returns.  This style of specifying terms and bindings is heavily
+  clause states that all the names the function @{text
+  "bn(as)"} returns should be bound in @{text s}.  This style of specifying terms and bindings is heavily
   inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
   However, we will not be able to cope with all specifications that are
@@ -358,7 +358,7 @@
   about them in a theorem prover would be a major pain.  \medskip
 
   \noindent
-  {\bf Contributions:}  We provide novel definitions for when terms
+  {\bf Contributions:}  We provide novel three definitions for when terms
   involving general binders are $\alpha$-equivalent. These definitions are
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for $\alpha$-equated
@@ -366,7 +366,7 @@
   conditions for $\alpha$-equated terms. We are also able to derive strong 
   induction principles that have the variable convention already built in.
   The method behind our specification of general binders is taken 
-  from the Ott-tool, but we introduce crucial restrictions, and also one extension, so 
+  from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 
   that our specifications make sense for reasoning about $\alpha$-equated terms. 
 
 
@@ -1026,7 +1026,7 @@
   
   \noindent
   In this specification the function @{text "bn"} determines which atoms of
-  @{text p} are bound in the argument @{text "t"}. Note that in the
+  the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
   second-last @{text bn}-clause the function @{text "atom"} coerces a name
   into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
   allows us to treat binders of different atom type uniformly.
@@ -1067,11 +1067,11 @@
   \noindent
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
-  inside the assignment. This difference has consequences for the free-variable 
-  function and $\alpha$-equivalence relation.
+  inside the assignment. This difference has consequences for the associated
+  notions of free-variables and $\alpha$-equivalence.
   
   To make sure that variables bound by deep binders cannot be free at the
-  same time, we cannot have more than one binding function for one deep binder. 
+  same time, we cannot have more than one binding function for a deep binder. 
   Consequently we exclude specifications such as
 
   \begin{center}
@@ -1090,9 +1090,9 @@
   
   We also need to restrict the form of the binding functions in order 
   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
-  terms. As a result we cannot return an atom in a binding function that is also
-  bound in the corresponding term-constructor. That means in the example
-  \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
+  terms. The main restriction is that we cannot return an atom in a binding function that is also
+  bound in the corresponding term-constructor. That means in \eqref{letpat} 
+  that the term-constructors @{text PVar} and @{text PTup} may
   not have a binding clause (all arguments are used to define @{text "bn"}).
   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
   may have a binding clause involving the argument @{text t} (the only one that
@@ -1143,12 +1143,12 @@
   term-constructors so that binders and their bodies are next to each other will 
   result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}. 
   Therefore we will first
-  extract datatype definitions from the specification and then define 
+  extract ``raw'' datatype definitions from the specification and then define 
   explicitly an $\alpha$-equivalence relation over them. We subsequently
   quotient the datatypes according to our $\alpha$-equivalence.
 
 
-  The datatype definition can be obtained by stripping off the 
+  The ``raw'' datatype definition can be obtained by stripping off the 
   binding clauses and the labels from the types. We also have to invent
   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
   given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
@@ -1179,15 +1179,14 @@
 
   The first non-trivial step we have to perform is the generation of
   free-variable functions from the specifications. For the 
-  \emph{raw} types @{text "ty"}$_{1..n}$ extracted from  a specification,
-  we define the free-variable functions
+  \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions
   %
   \begin{equation}\label{fvars}
   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
   \end{equation}
 
   \noindent
-  by recursion over the types @{text "ty"}$_{1..n}$.
+  by mutual recursion.
   We define these functions together with auxiliary free-variable functions for
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
@@ -1204,11 +1203,11 @@
   While the idea behind these free-variable functions is clear (they just
   collect all atoms that are not bound), because of our rather complicated
   binding mechanisms their definitions are somewhat involved.  Given
-  the term-constructor @{text "C"} of type @{text ty} and some associated
+  a term-constructor @{text "C"} of type @{text ty} and some associated
   binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
   "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
   "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
-  clause with mode \isacommand{bin\_set} means (similarly for the other modes). 
+  clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar). 
   Suppose the binding clause @{text bc\<^isub>i} is of the form 
   %
   \begin{equation}
@@ -1239,7 +1238,7 @@
   \noindent
   whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion 
   (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types 
-  @{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
   In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
   for atom types to which shallow binders have to refer
   %