1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
|
3 type maps_info = {mapfun: string, relfun: string} |
3 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
4 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
4 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 |
5 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
6 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
6 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 |
|
9 val maps_update: string -> maps_info -> theory -> theory |
|
10 |
7 end; |
11 end; |
8 |
12 |
9 structure Quotient: QUOTIENT = |
13 structure Quotient: QUOTIENT = |
10 struct |
14 struct |
|
15 |
|
16 (* data containers *) |
|
17 (*******************) |
|
18 |
|
19 (* map-functions and rel-functions *) |
|
20 type maps_info = {mapfun: string, relfun: string} |
|
21 |
|
22 local |
|
23 structure Data = TheoryDataFun |
|
24 (type T = maps_info Symtab.table |
|
25 val empty = Symtab.empty |
|
26 val copy = I |
|
27 val extend = I |
|
28 fun merge _ = Symtab.merge (K true)) |
|
29 in |
|
30 val maps_lookup = Symtab.lookup o Data.get |
|
31 fun maps_update k v = Data.map (Symtab.update (k, v)) |
|
32 end |
|
33 |
|
34 |
|
35 (* definition of the quotient type *) |
|
36 (***********************************) |
11 |
37 |
12 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
38 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
13 fun typedef_term rel rty lthy = |
39 fun typedef_term rel rty lthy = |
14 let |
40 let |
15 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
41 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
165 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
191 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
166 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
192 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
167 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
193 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
168 end |
194 end |
169 |
195 |
|
196 |
|
197 |
|
198 |
170 (* interface and syntax setup *) |
199 (* interface and syntax setup *) |
171 |
200 |
172 (* the ML-interface takes a list of 4-tuples consisting of *) |
201 (* the ML-interface takes a list of 4-tuples consisting of *) |
173 (* *) |
202 (* *) |
174 (* - the name of the quotient type *) |
203 (* - the name of the quotient type *) |
175 (* - its mixfix annotation *) |
204 (* - its mixfix annotation *) |
176 (* - the type to be quotient *) |
205 (* - the type to be quotient *) |
177 (* - the relation according to which the type is quotient *) |
206 (* - the relation according to which the type is quotient *) |
178 |
207 |
179 fun mk_quotient_type quot_list lthy = |
208 fun mk_quotient_type quot_list lthy = |
180 let |
209 let |
181 fun get_goal (rty, rel) = |
210 fun get_goal (rty, rel) = |
182 let |
211 let |
183 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
212 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |