1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 type maps_info = {mapfun: string, relfun: string} |
3 type maps_info = {mapfun: string, relfun: string} |
4 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
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: 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: theory -> quotient_info list |
13 val quotdata_lookup: theory -> quotient_info list |
14 val quotdata_update_thy: (typ * typ * term) -> theory -> theory |
14 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
15 val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context |
15 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
16 end; |
16 end; |
17 |
17 |
18 structure Quotient: QUOTIENT = |
18 structure Quotient: QUOTIENT = |
19 struct |
19 struct |
20 |
20 |
59 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
59 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
60 "declaration of map information")) |
60 "declaration of map information")) |
61 |
61 |
62 |
62 |
63 (* info about the quotient types *) |
63 (* info about the quotient types *) |
64 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
64 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
65 |
65 |
66 structure QuotData = TheoryDataFun |
66 structure QuotData = TheoryDataFun |
67 (type T = quotient_info list |
67 (type T = quotient_info list |
68 val empty = [] |
68 val empty = [] |
69 val copy = I |
69 val copy = I |
70 val extend = I |
70 val extend = I |
71 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
71 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
72 |
72 |
73 val quotdata_lookup = QuotData.get |
73 val quotdata_lookup = QuotData.get |
74 |
74 |
75 fun quotdata_update_thy (qty, rty, rel) thy = |
75 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
76 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy |
76 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
77 |
77 |
78 fun quotdata_update (qty, rty, rel) ctxt = |
78 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
79 ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt |
79 ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt |
80 |
80 |
81 fun print_quotdata ctxt = |
81 fun print_quotdata ctxt = |
82 let |
82 let |
83 fun prt_quot {qtyp, rtyp, rel} = |
83 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
84 Pretty.block (Library.separate (Pretty.brk 2) |
84 Pretty.block (Library.separate (Pretty.brk 2) |
85 [Pretty.str ("quotient type:"), |
85 [Pretty.str ("quotient type:"), |
86 Syntax.pretty_typ ctxt qtyp, |
86 Syntax.pretty_typ ctxt qtyp, |
87 Pretty.str ("raw type:"), |
87 Pretty.str ("raw type:"), |
88 Syntax.pretty_typ ctxt rtyp, |
88 Syntax.pretty_typ ctxt rtyp, |
89 Pretty.str ("relation:"), |
89 Pretty.str ("relation:"), |
90 Syntax.pretty_term ctxt rel]) |
90 Syntax.pretty_term ctxt rel, |
|
91 Pretty.str ("equiv. thm:"), |
|
92 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
91 in |
93 in |
92 QuotData.get (ProofContext.theory_of ctxt) |
94 QuotData.get (ProofContext.theory_of ctxt) |
93 |> map prt_quot |
95 |> map prt_quot |
94 |> Pretty.big_list "quotients:" |
96 |> Pretty.big_list "quotients:" |
95 |> Pretty.writeln |
97 |> Pretty.writeln |
99 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
101 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
100 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
102 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
101 |
103 |
102 |
104 |
103 |
105 |
104 (* wrappers for define and note *) |
106 (* wrappers for define, note and theorem_i*) |
105 fun define (name, mx, rhs) lthy = |
107 fun define (name, mx, rhs) lthy = |
106 let |
108 let |
107 val ((rhs, (_ , thm)), lthy') = |
109 val ((rhs, (_ , thm)), lthy') = |
108 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
110 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
109 in |
111 in |
229 (* quotient theorem *) |
238 (* quotient theorem *) |
230 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
239 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
231 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
240 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
232 |
241 |
233 (* storing the quot-info *) |
242 (* storing the quot-info *) |
234 val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 |
243 val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2 |
235 |
244 |
236 (* interpretation *) |
245 (* interpretation *) |
237 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
246 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
238 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
247 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
239 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
248 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
279 let |
288 let |
280 fun mk_goal (rty, rel) = |
289 fun mk_goal (rty, rel) = |
281 let |
290 let |
282 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
291 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
283 in |
292 in |
284 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
293 HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel) |
285 end |
294 end |
286 |
295 |
287 val goals = map (mk_goal o snd) quot_list |
296 val goals = map (mk_goal o snd) quot_list |
288 |
297 |
289 fun after_qed thms lthy = |
298 fun after_qed thms lthy = |
290 fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd |
299 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
291 in |
300 in |
292 Proof.theorem_i NONE after_qed [goals] lthy |
301 theorem after_qed goals lthy |
293 end |
302 end |
294 |
303 |
295 val quotspec_parser = |
304 val quotspec_parser = |
296 OuterParse.and_list1 |
305 OuterParse.and_list1 |
297 (OuterParse.short_ident -- OuterParse.opt_infix -- |
306 (OuterParse.short_ident -- OuterParse.opt_infix -- |