--- a/FIXME-TODO	Thu Dec 17 17:59:12 2009 +0100
+++ b/FIXME-TODO	Sat Dec 19 22:04:34 2009 +0100
@@ -14,14 +14,21 @@
 
 - Handle theorems that include Ball/Bex
 
-- quotient_respects and preserves in a natural form.
+- user should be able to give quotient_respects and 
+  preserves theorems in a more natural form.
 
+- the test in the (_, Const _) needs to be fixed
 
 Lower Priority
 ==============
 
 - accept partial equvalence relations
 
+- what happens if the original theorem contains bounded
+  quantifiers? can such theorems be lifted? If not, would 
+  it help if we introduced separate Bex and Ball constants
+  for quotienting?
+
 - inductions from the datatype package have a strange
   order of quantifiers in assumptions.
 

--- a/Quot/quotient_def.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_def.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -3,6 +3,7 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
+  
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
@@ -29,10 +30,13 @@
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
 fun get_fun_aux lthy s fs =
-  case (maps_lookup (ProofContext.theory_of lthy) s) of
-    SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-  | NONE      => raise
-        (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
+let
+  val thy = ProofContext.theory_of lthy
+  val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])
+  val info = maps_lookup thy s handle NotFound => raise exc
+in
+  list_comb (Const (#mapfun info, dummyT), fs)
+end
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)
@@ -72,9 +76,9 @@
   | (TFree x, TFree x') =>
      if x = x'
      then mk_identity qty
-     else raise (LIFT_MATCH "get_fun")
-  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
-  | _ => raise (LIFT_MATCH "get_fun")
+     else raise (LIFT_MATCH "get_fun (frees)")
+  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)")
+  | _ => raise (LIFT_MATCH "get_fun (default)")
 
 (* interface and syntax setup *)
 
@@ -84,6 +88,7 @@
 (* - name and attributes of the meta eq           *)
 (* - the new constant including its type          *)
 (* - the rhs of the definition                    *)
+
 fun quotient_def mx attr lhs rhs lthy =
 let
   val Free (lhs_str, lhs_ty) = lhs;
@@ -115,9 +120,9 @@
 
 val quotdef_parser =
   (SpecParse.opt_thm_name ":" --
-  OuterParse.term) --
-  (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
-  OuterParse.term)
+     OuterParse.term) --
+      (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
+         OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)

--- a/Quot/quotient_info.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_info.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -3,7 +3,7 @@
   exception NotFound
 
   type maps_info = {mapfun: string, relfun: string}
-  val maps_lookup: theory -> string -> maps_info option
+  val maps_lookup: theory -> string -> maps_info       (* raises NotFound *)
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
   val print_mapsinfo: Proof.context -> unit
@@ -18,7 +18,7 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
-  val qconsts_lookup: theory -> term -> qconsts_info
+  val qconsts_lookup: theory -> term -> qconsts_info    (* raises NotFound *)
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: theory -> qconsts_info list
@@ -50,7 +50,10 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
-val maps_lookup = Symtab.lookup o MapsData.get
+fun maps_lookup thy s = 
+  case (Symtab.lookup (MapsData.get thy) s) of
+    SOME map_fun => map_fun
+  | NONE => raise NotFound
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
@@ -188,14 +191,15 @@
     | _ => raise NotFound
   end
 
-(* We omit printing the definition *)
 fun print_qconstinfo ctxt =
 let
   fun prt_qconst {qconst, rconst, def} =
       Pretty.block (separate (Pretty.brk 1)
           [Syntax.pretty_term ctxt qconst,
            Pretty.str ":=",
-           Syntax.pretty_term ctxt rconst])
+           Syntax.pretty_term ctxt rconst,
+           Pretty.str "as",
+           Syntax.pretty_term ctxt (prop_of def)])
 in
   QConstsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest

--- a/Quot/quotient_term.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -10,31 +10,32 @@
 (*
 Regularizing an rtrm means:
  
- - Quantifiers over a type that need lifting are replaced 
+ - Quantifiers over types that need lifting are replaced 
    by bounded quantifiers, for example:
 
-      All P  ===> All (Respects R) P
+      All P  ----> All (Respects R) P
 
-   where the relation R is given by the rty and qty;
+   where the aggregate relation R is given by the rty and qty;
  
- - Abstractions over a type that needs lifting are replaced
-   by bounded abstractions:
+ - Abstractions over types that need lifting are replaced
+   by bounded abstractions, for example:
       
-      %x. P  ===> Ball (Respects R) %x. P
+      %x. P  ----> Ball (Respects R) %x. P
 
- - Equalities over the type being lifted are replaced by
-   corresponding equivalence relations:
+ - Equalities over types that need lifting are replaced by
+   corresponding equivalence relations, for example:
 
-      A = B  ===> R A B
+      A = B  ----> R A B
 
    or 
 
-      A = B  ===> (R ===> R) A B
+      A = B  ----> (R ===> R) A B
  
    for more complicated types of A and B
 *)
 
-(* builds the relation that is the argument of respects *)
+(* builds the aggregate equivalence relation *)
+(* that will be the argument of Respects     *)
 fun mk_resp_arg lthy (rty, qty) =
 let
   val thy = ProofContext.theory_of lthy
@@ -46,8 +47,9 @@
       (Type (s, tys), Type (s', tys')) =>
        if s = s' 
        then let
-              val SOME map_info = maps_lookup thy s
-              (* FIXME dont return an option, raise an exception *)
+              val map_info = maps_lookup thy s
+                             handle NotFound => 
+                               raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
               val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
               list_comb (Const (#relfun map_info, dummyT), args) 
@@ -88,7 +90,7 @@
 
 (* produces a regularized version of rtrm       *)
 (*                                              *)
-(* - the result is still contains dummyT        *)
+(* - the result still contains dummyTs          *)
 (*                                              *)
 (* - for regularisation we do not need any      *)
 (*   special treatment of bound variables       *)
@@ -124,14 +126,14 @@
          if ty = ty' then rtrm
          else mk_resp_arg lthy (domain_type ty, domain_type ty') 
 
-  | (* in this case we check whether the given equivalence relation is correct *) 
+  | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
          val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
          val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
        in 
-         if rel' = rel then rtrm else raise exc
+         if rel' aconv rel then rtrm else raise exc
        end  
 
   | (_, Const _) =>
@@ -168,10 +170,6 @@
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
 
-  | (Free (x, ty), Free (x', ty')) => 
-       (* this case cannot arrise as we start with two fully atomized terms *)
-       raise (LIFT_MATCH "regularize (frees)")
-
   | (Bound i, Bound i') =>
        if i = i' then rtrm 
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
@@ -187,32 +185,31 @@
 
 
 (*
-Injecting of Rep/Abs means:
+Injection of Rep/Abs means:
 
   For abstractions
 :
-  * If the type of the abstraction doesn't need lifting we recurse.
-
-  * If it needs lifting then we add Rep/Abs around the whole term and 
-    check if the bound variable needs lifting.
+  * If the type of the abstraction needs lifting, then we add Rep/Abs 
+    around the abstraction; otherwise we leave it unchanged.
  
-    * If it does we recurse and put Rep/Abs around all occurences
-      of the variable in the obtained subterm. This in combination
-      with the Rep/Abs from above will let us change the type of 
-      the abstraction with rewriting.
-  
   For applications:
   
-  * If the term is Respects applied to anything we leave it unchanged
+  * If the application involves a bounded quantifier, we recurse on 
+    the second argument. If the application is a bounded abstraction,
+    we always put an Re/Abs around it (since bounded abstractions
+    always need lifting). Otherwise we recurse on both arguments.
 
-  * If the term needs lifting and the head is a constant that we know
-    how to lift, we put a Rep/Abs and recurse
+  For constants:
 
-  * If the term needs lifting and the head is a Free applied to subterms
-    (if it is not applied we treated it in Abs branch) then we
-    put Rep/Abs and recurse
+  * If the constant is (op =), we leave it always unchanged. 
+    Otherwise the type of the constant needs lifting, we put
+    and Rep/Abs around it. 
 
-  * Otherwise just recurse.
+  For free variables:
+
+  * We put aRep/Abs around it if the type needs lifting.
+
+  Vars case cannot occur.
 *)
 
 fun mk_repabs lthy (T, T') trm = 
@@ -269,7 +266,7 @@
         else mk_repabs lthy (rty, T') rtrm
       end   
   
-  | _ => raise (LIFT_MATCH "injection")
+  | _ => raise (LIFT_MATCH "injection (default)")
 
 end; (* structure *)
 

--- a/Quot/quotient_typ.ML	Thu Dec 17 17:59:12 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 19 22:04:34 2009 +0100
@@ -12,7 +12,7 @@
 
 exception LIFT_MATCH of string
 
-(* wrappers for define, note and theorem_i *)
+(* wrappers for define, note, Attrib.internal and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
@@ -28,7 +28,7 @@
   (thm', lthy')
 end
 
-fun internal_attr at = Attrib.internal (K at)
+fun intern_attr at = Attrib.internal (K at)
 
 fun theorem after_qed goals ctxt =
 let
@@ -117,13 +117,13 @@
     (K typedef_quotient_thm_tac)
 end
 
-(* main function for constructing the quotient type *)
+(* main function for constructing a quotient type *)
 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
-  (* generates typedef *)
+  (* generates the typedef *)
   val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
 
-  (* abs and rep functions *)
+  (* abs and rep functions from the typedef *)
   val abs_ty = #abs_type typedef_info
   val rep_ty = #rep_type typedef_info
   val abs_name = #Abs_name typedef_info
@@ -131,7 +131,7 @@
   val abs = Const (abs_name, rep_ty --> abs_ty)
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
-  (* ABS and REP definitions *)
+  (* more abstract ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT )
   val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT )
   val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
@@ -155,14 +155,14 @@
   val lthy3 = quotdata_update qty_str 
                (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
-  (* FIXME: the relation needs to be a string, since its type needs *)
-  (* FIXME: to recalculated in for example REGULARIZE *)
+  (* FIXME: the relation can be any term, that later maybe needs to be given *)
+  (* FIXME: a different type (in regularize_trm); how should tis be done?    *)
 
 in
   lthy3
   |> note (quot_thm_name, quot_thm, [])
-  ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
-  ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add])
+  ||>> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
+  ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add])
 end