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) |