# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1262304499 -3600
# Node ID 71225f4a46355bc66f8379fc700a844b23fdd5a1
# Parent  0755f8fd56b3ea2efde5aad82d9e7d6d9a9d9c3c
some slight tuning

diff -r 0755f8fd56b3 -r 71225f4a4635 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Thu Dec 31 23:53:10 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Jan 01 01:08:19 2010 +0100
@@ -26,16 +26,19 @@
 
 (* interface and syntax setup *)
 
-(* the ML-interface takes a 4-tuple consisting of *)
-(*                                                *)
-(* - the mixfix annotation                        *)
-(* - name and attributes of the meta eq           *)
-(* - the new constant including its type          *)
-(* - the rhs of the definition                    *)
+(* the ML-interface takes a 4-tuple consisting of  *)
+(*                                                 *)
+(* - the mixfix annotation                         *)
+(* - name and attributes                           *)
+(* - the new constant including its type           *)
+(* - the rhs of the definition                     *)
+(*                                                 *)
+(* returns the defined constant and its definition *)
+(* theorem; stores the data in the qconsts slot    *)
 
 fun quotient_def mx attr lhs rhs lthy =
 let
-  val Free (lhs_str, lhs_ty) = lhs;
+  val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.)
   val qconst_bname = Binding.name lhs_str;
   val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, absrep_trm)
@@ -44,6 +47,7 @@
 
   val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
 
+  (* data storage *)
   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
                  (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
@@ -72,7 +76,3 @@
              OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 
 end; (* structure *)
-
-
-
-
diff -r 0755f8fd56b3 -r 71225f4a4635 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Dec 31 23:53:10 2009 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 01 01:08:19 2010 +0100
@@ -40,9 +40,6 @@
 val mk_id = Const (@{const_name "id"}, dummyT)
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
-
 fun mk_compose flag (trm1, trm2) = 
   case flag of
     absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
@@ -57,10 +54,17 @@
   Const (mapfun, dummyT)
 end
 
+(* makes a Free out of a TVar *)
+fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+
 (* produces an aggregate map function for the       *)
 (* rty-part of a quotient definition; abstracts     *)
 (* over all variables listed in vs (these variables *)
 (* correspond to the type variables in rty)         *)        
+(*                                                  *)
+(* for example for: ?'a list                        *)
+(* it produces:     %a. map a                       *)
+(* 
 fun mk_mapfun ctxt vs ty =
 let
   val vs' = map (mk_Free) vs
@@ -96,7 +100,7 @@
   (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
 end
 
-(* produces the rep or abs constants for a qty *)
+(* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
 let
   val thy = ProofContext.theory_of ctxt
@@ -175,7 +179,7 @@
                           handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
              val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
                           handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty 
-             val args_aux = map (double_lookup rtyenv qtyenv) vs            
+             val args_aux = map (double_lookup rtyenv qtyenv) vs 
              val args = map (absrep_fun flag ctxt) args_aux
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
diff -r 0755f8fd56b3 -r 71225f4a4635 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Dec 31 23:53:10 2009 +0100
+++ b/Quot/quotient_typ.ML	Fri Jan 01 01:08:19 2010 +0100
@@ -217,9 +217,15 @@
 (* - its mixfix annotation                                  *)
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
+(*                                                          *)
+(* opens a proof-state in which one has to show that the    *)
+(* relation is an equivalence relation                      *)
 
 fun quotient_type quot_list lthy = 
 let
+  (* sanity check *)  
+  val _ = map sanity_check quot_list 
+
   fun mk_goal (rty, rel) =
   let
     val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
@@ -231,14 +237,11 @@
               
   fun after_qed thms lthy =
     fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
-
-  (* sanity check *)  
-  val _ = map sanity_check quot_list 
 in
   theorem after_qed goals lthy
 end
            
-fun quotient_type_cmd spec lthy = 
+fun quotient_type_cmd specs lthy = 
 let
   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =
   let
@@ -248,7 +251,7 @@
     ((vs, qty_name, mx), (rty, rel))
   end
 in
-  quotient_type (map parse_spec spec) lthy
+  quotient_type (map parse_spec specs) lthy
 end
 
 val quotspec_parser =