5 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
5 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
6 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
7 val note: binding * thm -> local_theory -> thm * local_theory |
7 val note: binding * thm -> local_theory -> thm * local_theory |
8 val maps_lookup: theory -> string -> maps_info option |
8 val maps_lookup: theory -> string -> maps_info option |
9 val maps_update: string -> maps_info -> theory -> theory |
9 val maps_update: string -> maps_info -> theory -> theory |
10 |
10 val print_quotdata: Proof.context -> unit |
11 end; |
11 end; |
12 |
12 |
13 structure Quotient: QUOTIENT = |
13 structure Quotient: QUOTIENT = |
14 struct |
14 struct |
15 |
15 |
28 |
28 |
29 val maps_lookup = Symtab.lookup o MapsData.get |
29 val maps_lookup = Symtab.lookup o MapsData.get |
30 fun maps_update k v = MapsData.map (Symtab.update (k, v)) |
30 fun maps_update k v = MapsData.map (Symtab.update (k, v)) |
31 |
31 |
32 |
32 |
33 |
|
34 (* info about the quotient types *) |
33 (* info about the quotient types *) |
35 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
34 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
36 |
35 |
37 structure QuotData = TheoryDataFun |
36 structure QuotData = TheoryDataFun |
38 (type T = quotient_info list |
37 (type T = quotient_info list |
45 fun quotdata_update (qty, rty, rel) = |
44 fun quotdata_update (qty, rty, rel) = |
46 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
45 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
47 |
46 |
48 fun print_quotdata ctxt = |
47 fun print_quotdata ctxt = |
49 let |
48 let |
50 val quots = QuotData.get (Context.theory_of_proof ctxt) |
49 val quots = QuotData.get (ProofContext.theory_of ctxt) |
51 fun prt_quot {qtyp, rtyp, rel} = Pretty.block |
50 fun prt_quot {qtyp, rtyp, rel} = |
52 [Pretty.str ("quotient:"), |
51 Pretty.block [Pretty.str ("quotient:"), |
53 Pretty.brk 2, |
52 Pretty.brk 2, Syntax.pretty_typ ctxt qtyp, |
54 Syntax.pretty_typ ctxt qtyp, |
53 Pretty.brk 2, Syntax.pretty_typ ctxt rtyp, |
55 Pretty.brk 2, |
54 Pretty.brk 2, Syntax.pretty_term ctxt rel] |
56 Syntax.pretty_typ ctxt rtyp, |
|
57 Pretty.brk 2, |
|
58 Syntax.pretty_term ctxt rel] |
|
59 in |
55 in |
60 [Pretty.big_list "quotients:" (map prt_quot quots)] |
56 [Pretty.big_list "quotients:" (map prt_quot quots)] |
61 |> Pretty.chunks |> Pretty.writeln |
57 |> Pretty.chunks |> Pretty.writeln |
62 end |
58 end |
63 |
59 |
174 val rep_ty = #rep_type typedef_info |
170 val rep_ty = #rep_type typedef_info |
175 val abs_name = #Abs_name typedef_info |
171 val abs_name = #Abs_name typedef_info |
176 val rep_name = #Rep_name typedef_info |
172 val rep_name = #Rep_name typedef_info |
177 val abs = Const (abs_name, rep_ty --> abs_ty) |
173 val abs = Const (abs_name, rep_ty --> abs_ty) |
178 val rep = Const (rep_name, abs_ty --> rep_ty) |
174 val rep = Const (rep_name, abs_ty --> rep_ty) |
|
175 |
|
176 (* storing the quot-info *) |
|
177 val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy) |
179 |
178 |
180 (* ABS and REP definitions *) |
179 (* ABS and REP definitions *) |
181 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
180 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
182 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
181 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
183 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
182 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
244 |
243 |
245 fun mk_quotient_type quot_list lthy = |
244 fun mk_quotient_type quot_list lthy = |
246 let |
245 let |
247 fun get_goal (rty, rel) = |
246 fun get_goal (rty, rel) = |
248 let |
247 let |
249 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
248 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
250 in |
249 in |
251 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
250 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
252 end |
251 end |
253 |
252 |
254 val goals = map (get_goal o snd) quot_list |
253 val goals = map (get_goal o snd) quot_list |
272 val qty_name = Binding.name qty_str |
271 val qty_name = Binding.name qty_str |
273 val rty = Syntax.parse_typ lthy rty_str |
272 val rty = Syntax.parse_typ lthy rty_str |
274 val rel = Syntax.parse_term lthy rel_str |
273 val rel = Syntax.parse_term lthy rel_str |
275 |> Syntax.check_term lthy |
274 |> Syntax.check_term lthy |
276 in |
275 in |
277 ((qty_name, mx), (rty, rel)) |
276 ((qty_name, mx), (rty, rel)) |
278 end |
277 end |
279 in |
278 in |
280 mk_quotient_type (map parse_spec spec) lthy |
279 mk_quotient_type (map parse_spec spec) lthy |
281 end |
280 end |
282 |
281 |