1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 type maps_info = {mapfun: string, relfun: string} |
|
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 |
3 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 |
4 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 |
5 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
6 val note: binding * thm -> local_theory -> thm * local_theory |
9 val maps_lookup: theory -> string -> maps_info option |
|
10 val maps_update_thy: string -> maps_info -> theory -> theory |
|
11 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
|
12 val print_quotdata: Proof.context -> unit |
|
13 val quotdata_lookup_thy: theory -> quotient_info list |
|
14 val quotdata_lookup: Proof.context -> quotient_info list |
|
15 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
|
16 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
|
17 end; |
7 end; |
18 |
8 |
19 structure Quotient: QUOTIENT = |
9 structure Quotient: QUOTIENT = |
20 struct |
10 struct |
21 |
|
22 (* data containers *) |
|
23 (*******************) |
|
24 |
|
25 (* info about map- and rel-functions *) |
|
26 type maps_info = {mapfun: string, relfun: string} |
|
27 |
|
28 structure MapsData = TheoryDataFun |
|
29 (type T = maps_info Symtab.table |
|
30 val empty = Symtab.empty |
|
31 val copy = I |
|
32 val extend = I |
|
33 fun merge _ = Symtab.merge (K true)) |
|
34 |
|
35 val maps_lookup = Symtab.lookup o MapsData.get |
|
36 |
|
37 |
|
38 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
|
39 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
|
40 |
|
41 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
|
42 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
|
43 |
|
44 (* attribute to be used in declare statements *) |
|
45 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
|
46 let |
|
47 val thy = ProofContext.theory_of ctxt |
|
48 val tyname = Sign.intern_type thy tystr |
|
49 val mapname = Sign.intern_const thy mapstr |
|
50 val relname = Sign.intern_const thy relstr |
|
51 in |
|
52 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
|
53 end |
|
54 |
|
55 val maps_attr_parser = |
|
56 Args.context -- Scan.lift |
|
57 ((Args.name --| OuterParse.$$$ "=") -- |
|
58 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
|
59 Args.name --| OuterParse.$$$ ")")) |
|
60 |
|
61 val _ = Context.>> (Context.map_theory |
|
62 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
|
63 "declaration of map information")) |
|
64 |
|
65 |
|
66 (* info about the quotient types *) |
|
67 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
|
68 |
|
69 structure QuotData = TheoryDataFun |
|
70 (type T = quotient_info list |
|
71 val empty = [] |
|
72 val copy = I |
|
73 val extend = I |
|
74 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
|
75 |
|
76 val quotdata_lookup_thy = QuotData.get |
|
77 val quotdata_lookup = QuotData.get o ProofContext.theory_of |
|
78 |
|
79 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
|
80 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
|
81 |
|
82 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
|
83 ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt |
|
84 |
|
85 fun print_quotdata ctxt = |
|
86 let |
|
87 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
|
88 Pretty.block (Library.separate (Pretty.brk 2) |
|
89 [Pretty.str ("quotient type:"), |
|
90 Syntax.pretty_typ ctxt qtyp, |
|
91 Pretty.str ("raw type:"), |
|
92 Syntax.pretty_typ ctxt rtyp, |
|
93 Pretty.str ("relation:"), |
|
94 Syntax.pretty_term ctxt rel, |
|
95 Pretty.str ("equiv. thm:"), |
|
96 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
|
97 in |
|
98 QuotData.get (ProofContext.theory_of ctxt) |
|
99 |> map prt_quot |
|
100 |> Pretty.big_list "quotients:" |
|
101 |> Pretty.writeln |
|
102 end |
|
103 |
|
104 val _ = |
|
105 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
|
106 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
|
107 |
|
108 |
|
109 |
11 |
110 (* wrappers for define, note and theorem_i *) |
12 (* wrappers for define, note and theorem_i *) |
111 fun define (name, mx, rhs) lthy = |
13 fun define (name, mx, rhs) lthy = |
112 let |
14 let |
113 val ((rhs, (_ , thm)), lthy') = |
15 val ((rhs, (_ , thm)), lthy') = |