14 struct |
14 struct |
15 |
15 |
16 (* data containers *) |
16 (* data containers *) |
17 (*******************) |
17 (*******************) |
18 |
18 |
19 (* map-functions and rel-functions *) |
19 (* info about map- and rel-functions *) |
20 type maps_info = {mapfun: string, relfun: string} |
20 type maps_info = {mapfun: string, relfun: string} |
21 |
21 |
22 local |
22 structure MapsData = TheoryDataFun |
23 structure Data = TheoryDataFun |
|
24 (type T = maps_info Symtab.table |
23 (type T = maps_info Symtab.table |
25 val empty = Symtab.empty |
24 val empty = Symtab.empty |
26 val copy = I |
25 val copy = I |
27 val extend = I |
26 val extend = I |
28 fun merge _ = Symtab.merge (K true)) |
27 fun merge _ = Symtab.merge (K true)) |
29 in |
28 |
30 val maps_lookup = Symtab.lookup o Data.get |
29 val maps_lookup = Symtab.lookup o MapsData.get |
31 fun maps_update k v = Data.map (Symtab.update (k, v)) |
30 fun maps_update k v = MapsData.map (Symtab.update (k, v)) |
32 end |
31 |
|
32 |
|
33 |
|
34 (* info about the quotient types *) |
|
35 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
|
36 |
|
37 structure QuotData = TheoryDataFun |
|
38 (type T = quotient_info list |
|
39 val empty = [] |
|
40 val copy = I |
|
41 val extend = I |
|
42 fun merge _ = (op @)) |
|
43 |
|
44 val quotdata_lookup = QuotData.get |
|
45 fun quotdata_update (qty, rty, rel) = |
|
46 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
|
47 |
|
48 fun print_quotdata ctxt = |
|
49 let |
|
50 val quots = QuotData.get (Context.theory_of_proof ctxt) |
|
51 fun prt_quot {qtyp, rtyp, rel} = Pretty.block |
|
52 [Pretty.str ("quotient:"), |
|
53 Pretty.brk 2, |
|
54 Syntax.pretty_typ ctxt qtyp, |
|
55 Pretty.brk 2, |
|
56 Syntax.pretty_typ ctxt rtyp, |
|
57 Pretty.brk 2, |
|
58 Syntax.pretty_term ctxt rel] |
|
59 in |
|
60 [Pretty.big_list "quotients:" (map prt_quot quots)] |
|
61 |> Pretty.chunks |> Pretty.writeln |
|
62 end |
|
63 |
|
64 val _ = |
|
65 OuterSyntax.improper_command "print_quotients" "print quotient types of this theory" |
|
66 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
|
67 |
|
68 |
|
69 |
|
70 (* wrappers for define and note *) |
|
71 fun define (name, mx, rhs) lthy = |
|
72 let |
|
73 val ((rhs, (_ , thm)), lthy') = |
|
74 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
|
75 in |
|
76 ((rhs, thm), lthy') |
|
77 end |
|
78 |
|
79 fun note (name, thm) lthy = |
|
80 let |
|
81 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
|
82 in |
|
83 (thm', lthy') |
|
84 end |
|
85 |
33 |
86 |
34 |
87 |
35 (* definition of the quotient type *) |
88 (* definition of the quotient type *) |
36 (***********************************) |
89 (***********************************) |
37 |
90 |
106 rtac @{thm QUOT_TYPE.QUOTIENT}, |
159 rtac @{thm QUOT_TYPE.QUOTIENT}, |
107 rtac quot_type_thm] |
160 rtac quot_type_thm] |
108 in |
161 in |
109 Goal.prove lthy [] [] goal |
162 Goal.prove lthy [] [] goal |
110 (K typedef_quotient_thm_tac) |
163 (K typedef_quotient_thm_tac) |
111 end |
|
112 |
|
113 (* two wrappers for define and note *) |
|
114 fun define (name, mx, rhs) lthy = |
|
115 let |
|
116 val ((rhs, (_ , thm)), lthy') = |
|
117 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
|
118 in |
|
119 ((rhs, thm), lthy') |
|
120 end |
|
121 |
|
122 fun note (name, thm) lthy = |
|
123 let |
|
124 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
|
125 in |
|
126 (thm', lthy') |
|
127 end |
164 end |
128 |
165 |
129 (* main function for constructing the quotient type *) |
166 (* main function for constructing the quotient type *) |
130 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
167 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
131 let |
168 let |
207 |
244 |
208 fun mk_quotient_type quot_list lthy = |
245 fun mk_quotient_type quot_list lthy = |
209 let |
246 let |
210 fun get_goal (rty, rel) = |
247 fun get_goal (rty, rel) = |
211 let |
248 let |
212 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
249 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
213 in |
250 in |
214 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
251 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
215 end |
252 end |
216 |
253 |
217 val goals = map (get_goal o snd) quot_list |
254 val goals = map (get_goal o snd) quot_list |
218 |
255 |
219 fun after_qed thms lthy = |
256 fun after_qed thms lthy = |
220 let |
257 fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd |
221 val thms' = flat thms |
|
222 in |
|
223 fold_map mk_typedef_main (quot_list ~~ thms') lthy |> snd |
|
224 end |
|
225 in |
258 in |
226 Proof.theorem_i NONE after_qed [goals] lthy |
259 Proof.theorem_i NONE after_qed [goals] lthy |
227 end |
260 end |
228 |
261 |
229 val quotspec_parser = |
262 val quotspec_parser = |