quotient.ML
changeset 254 77ff9624cfd6
parent 218 df05cd030d2f
child 256 53d7477a1f94
equal deleted inserted replaced
252:e30997c88050 254:77ff9624cfd6
     4   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
     4   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
     5   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
     5   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
     6   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
     6   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
     7   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
     7   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
     8   val note: binding * thm -> local_theory -> thm * local_theory
     8   val note: binding * thm -> local_theory -> thm * local_theory
     9   val maps_lookup: theory -> string -> maps_info option
     9   val maps_lookup_thy: theory -> string -> maps_info option
    10   val maps_update_thy: string -> maps_info -> theory -> theory    
    10   val maps_update_thy: string -> maps_info -> theory -> theory    
    11   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
    11   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
    12   val print_quotdata: Proof.context -> unit
    12   val print_quotdata: Proof.context -> unit
    13   val quotdata_lookup_thy: theory -> quotient_info list
    13   val quotdata_lookup_thy: theory -> quotient_info list
    14   val quotdata_lookup: Proof.context -> quotient_info list
    14   val quotdata_lookup: Proof.context -> quotient_info list
    30    val empty = Symtab.empty
    30    val empty = Symtab.empty
    31    val copy = I
    31    val copy = I
    32    val extend = I
    32    val extend = I
    33    fun merge _ = Symtab.merge (K true))
    33    fun merge _ = Symtab.merge (K true))
    34 
    34 
    35 val maps_lookup = Symtab.lookup o MapsData.get
    35 val maps_lookup_thy = Symtab.lookup o MapsData.get
       
    36 
       
    37 
    36 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
    38 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
    37 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
    39 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
    38 
    40 
    39 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
    41 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
    40   (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
    42   (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
   240   (* quotient theorem *)
   242   (* quotient theorem *)
   241   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
   243   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
   242   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
   244   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
   243 
   245 
   244   (* storing the quot-info *)
   246   (* storing the quot-info *)
   245   val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2
   247   val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
   246 
   248 
   247   (* interpretation *)
   249   (* interpretation *)
   248   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
   250   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
   249   val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3;
   251   val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3;
   250   val eqn1i = Thm.prop_of (symmetric eqn1pre)
   252   val eqn1i = Thm.prop_of (symmetric eqn1pre)