author | bulwahn |
Thu, 27 Oct 2011 13:50:54 +0200 | |
changeset 45272 | 5995ab88a00f |
parent 42361 | 23f352990944 |
child 45273 | 728ed9d28c63 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Quotient/quotient_info.ML |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
35788 | 4 |
Data slots for the quotient package. |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
41451 | 7 |
(* FIXME odd names/signatures of data access operations *) |
8 |
||
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
signature QUOTIENT_INFO = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
sig |
40236
8694a12611f9
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
wenzelm
parents:
38764
diff
changeset
|
11 |
exception NotFound (* FIXME complicates signatures unnecessarily *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
type maps_info = {mapfun: string, relmap: string} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
val maps_defined: theory -> string -> bool |
41443 | 15 |
(* FIXME functions called "lookup" must return option, not raise exception! *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
val maps_update_thy: string -> maps_info -> theory -> theory |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
val maps_update: string -> maps_info -> Proof.context -> Proof.context |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
val print_mapsinfo: Proof.context -> unit |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
45272
5995ab88a00f
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
bulwahn
parents:
42361
diff
changeset
|
23 |
val quotdata_lookup: theory -> string -> quotdata_info option |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
val quotdata_dest: Proof.context -> quotdata_info list |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
val print_quotinfo: Proof.context -> unit |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
type qconsts_info = {qconst: term, rconst: term, def: thm} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
val qconsts_dest: Proof.context -> qconsts_info list |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
val print_qconstinfo: Proof.context -> unit |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
val equiv_rules_get: Proof.context -> thm list |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
val equiv_rules_add: attribute |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
val rsp_rules_get: Proof.context -> thm list |
35314
cbdf785a1eb3
export prs_rules and rsp_rules attributes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35278
diff
changeset
|
40 |
val rsp_rules_add: attribute |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
val prs_rules_get: Proof.context -> thm list |
35314
cbdf785a1eb3
export prs_rules and rsp_rules attributes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35278
diff
changeset
|
42 |
val prs_rules_add: attribute |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
val id_simps_get: Proof.context -> thm list |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
val quotient_rules_get: Proof.context -> thm list |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
val quotient_rules_add: attribute |
41452 | 46 |
val setup: theory -> theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
end; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
structure Quotient_Info: QUOTIENT_INFO = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
struct |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
41443 | 52 |
exception NotFound (* FIXME odd OCaml-ism!? *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
(** data containers **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41452
diff
changeset
|
57 |
(* FIXME just one data slot (record) per program unit *) |
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41452
diff
changeset
|
58 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
(* info about map- and rel-functions for a type *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
type maps_info = {mapfun: string, relmap: string} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
structure MapsData = Theory_Data |
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
63 |
( |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
64 |
type T = maps_info Symtab.table |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
65 |
val empty = Symtab.empty |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
66 |
val extend = I |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
67 |
fun merge data = Symtab.merge (K true) data |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
68 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
fun maps_defined thy s = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
Symtab.defined (MapsData.get thy) s |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
fun maps_lookup thy s = |
41444 | 74 |
(case Symtab.lookup (MapsData.get thy) s of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
SOME map_fun => map_fun |
41444 | 76 |
| NONE => raise NotFound) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
42361 | 79 |
fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo) (* FIXME *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
fun maps_attribute_aux s minfo = Thm.declaration_attribute |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
(fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
(* attribute to be used in declare statements *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
85 |
fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
41444 | 86 |
let |
42361 | 87 |
val thy = Proof_Context.theory_of ctxt |
41444 | 88 |
val tyname = Sign.intern_type thy tystr |
89 |
val mapname = Sign.intern_const thy mapstr |
|
90 |
val relname = Sign.intern_const thy relstr |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
|
41444 | 92 |
fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) |
93 |
val _ = List.app sanity_check [mapname, relname] |
|
94 |
in |
|
95 |
maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
|
96 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
val maps_attr_parser = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
Args.context -- Scan.lift |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35788
diff
changeset
|
100 |
((Args.name --| Parse.$$$ "=") -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35788
diff
changeset
|
101 |
(Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35788
diff
changeset
|
102 |
Args.name --| Parse.$$$ ")")) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
104 |
fun print_mapsinfo ctxt = |
41444 | 105 |
let |
106 |
fun prt_map (ty_name, {mapfun, relmap}) = |
|
41445 | 107 |
Pretty.block (separate (Pretty.brk 2) |
41444 | 108 |
(map Pretty.str |
41445 | 109 |
["type:", ty_name, |
41444 | 110 |
"map:", mapfun, |
111 |
"relation map:", relmap])) |
|
112 |
in |
|
42361 | 113 |
MapsData.get (Proof_Context.theory_of ctxt) |
41444 | 114 |
|> Symtab.dest |
115 |
|> map (prt_map) |
|
116 |
|> Pretty.big_list "maps for type constructors:" |
|
117 |
|> Pretty.writeln |
|
118 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
119 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
120 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
(* info about quotient types *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
structure QuotData = Theory_Data |
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
125 |
( |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
126 |
type T = quotdata_info Symtab.table |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
127 |
val empty = Symtab.empty |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
128 |
val extend = I |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
129 |
fun merge data = Symtab.merge (K true) data |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
130 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
131 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
{qtyp = Morphism.typ phi qtyp, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
rtyp = Morphism.typ phi rtyp, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
equiv_rel = Morphism.term phi equiv_rel, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
136 |
equiv_thm = Morphism.thm phi equiv_thm} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
|
45272
5995ab88a00f
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
bulwahn
parents:
42361
diff
changeset
|
138 |
fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
fun quotdata_dest lthy = |
42361 | 144 |
map snd (Symtab.dest (QuotData.get (Proof_Context.theory_of lthy))) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
145 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
146 |
fun print_quotinfo ctxt = |
41444 | 147 |
let |
148 |
fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
|
41445 | 149 |
Pretty.block (separate (Pretty.brk 2) |
41444 | 150 |
[Pretty.str "quotient type:", |
151 |
Syntax.pretty_typ ctxt qtyp, |
|
152 |
Pretty.str "raw type:", |
|
153 |
Syntax.pretty_typ ctxt rtyp, |
|
154 |
Pretty.str "relation:", |
|
155 |
Syntax.pretty_term ctxt equiv_rel, |
|
156 |
Pretty.str "equiv. thm:", |
|
157 |
Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
|
158 |
in |
|
42361 | 159 |
QuotData.get (Proof_Context.theory_of ctxt) |
41444 | 160 |
|> Symtab.dest |
161 |
|> map (prt_quot o snd) |
|
162 |
|> Pretty.big_list "quotients:" |
|
163 |
|> Pretty.writeln |
|
164 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
(* info about quotient constants *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
type qconsts_info = {qconst: term, rconst: term, def: thm} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
169 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
172 |
(* We need to be able to lookup instances of lifted constants, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
173 |
for example given "nat fset" we need to find "'a fset"; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
but overloaded constants share the same name *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
structure QConstsData = Theory_Data |
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
176 |
( |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
177 |
type T = qconsts_info list Symtab.table |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
178 |
val empty = Symtab.empty |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
179 |
val extend = I |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
180 |
val merge = Symtab.merge_list qconsts_info_eq |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38756
diff
changeset
|
181 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
183 |
fun transform_qconsts phi {qconst, rconst, def} = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
184 |
{qconst = Morphism.term phi qconst, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
rconst = Morphism.term phi rconst, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
186 |
def = Morphism.thm phi def} |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
187 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
188 |
fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
191 |
fun qconsts_dest lthy = |
42361 | 192 |
flat (map snd (Symtab.dest (QConstsData.get (Proof_Context.theory_of lthy)))) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
194 |
fun qconsts_lookup thy t = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
195 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
val (name, qty) = dest_Const t |
35241 | 197 |
fun matches (x: qconsts_info) = |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
198 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
199 |
val (name', qty') = dest_Const (#qconst x); |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
200 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
201 |
name = name' andalso Sign.typ_instance thy (qty, qty') |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
202 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
203 |
in |
41444 | 204 |
(case Symtab.lookup (QConstsData.get thy) name of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
205 |
NONE => raise NotFound |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
206 |
| SOME l => |
41444 | 207 |
(case find_first matches l of |
208 |
SOME x => x |
|
209 |
| NONE => raise NotFound)) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
210 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
211 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
212 |
fun print_qconstinfo ctxt = |
41444 | 213 |
let |
214 |
fun prt_qconst {qconst, rconst, def} = |
|
215 |
Pretty.block (separate (Pretty.brk 1) |
|
216 |
[Syntax.pretty_term ctxt qconst, |
|
217 |
Pretty.str ":=", |
|
218 |
Syntax.pretty_term ctxt rconst, |
|
219 |
Pretty.str "as", |
|
220 |
Syntax.pretty_term ctxt (prop_of def)]) |
|
221 |
in |
|
42361 | 222 |
QConstsData.get (Proof_Context.theory_of ctxt) |
41444 | 223 |
|> Symtab.dest |
224 |
|> map snd |
|
225 |
|> flat |
|
226 |
|> map prt_qconst |
|
227 |
|> Pretty.big_list "quotient constants:" |
|
228 |
|> Pretty.writeln |
|
229 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
230 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
231 |
(* equivalence relation theorems *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
232 |
structure EquivRules = Named_Thms |
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
233 |
( |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
234 |
val name = "quot_equiv" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
235 |
val description = "equivalence relation theorems" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
236 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
237 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
238 |
val equiv_rules_get = EquivRules.get |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
239 |
val equiv_rules_add = EquivRules.add |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
240 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
241 |
(* respectfulness theorems *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
242 |
structure RspRules = Named_Thms |
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
243 |
( |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
244 |
val name = "quot_respect" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
245 |
val description = "respectfulness theorems" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
246 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
247 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
248 |
val rsp_rules_get = RspRules.get |
35314
cbdf785a1eb3
export prs_rules and rsp_rules attributes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35278
diff
changeset
|
249 |
val rsp_rules_add = RspRules.add |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
250 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
(* preservation theorems *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
252 |
structure PrsRules = Named_Thms |
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
253 |
( |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
254 |
val name = "quot_preserve" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
255 |
val description = "preservation theorems" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
256 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
257 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
258 |
val prs_rules_get = PrsRules.get |
35314
cbdf785a1eb3
export prs_rules and rsp_rules attributes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35278
diff
changeset
|
259 |
val prs_rules_add = PrsRules.add |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
260 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
261 |
(* id simplification theorems *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
262 |
structure IdSimps = Named_Thms |
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
263 |
( |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
264 |
val name = "id_simps" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
265 |
val description = "identity simp rules for maps" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
266 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
267 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
268 |
val id_simps_get = IdSimps.get |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
269 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
270 |
(* quotient theorems *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
271 |
structure QuotientRules = Named_Thms |
38764
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
272 |
( |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
273 |
val name = "quot_thm" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
274 |
val description = "quotient theorems" |
e6a18808873c
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
wenzelm
parents:
38759
diff
changeset
|
275 |
) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
276 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
277 |
val quotient_rules_get = QuotientRules.get |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
278 |
val quotient_rules_add = QuotientRules.add |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
279 |
|
41452 | 280 |
|
281 |
(* theory setup *) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
282 |
|
41452 | 283 |
val setup = |
284 |
Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
|
285 |
"declaration of map information" #> |
|
286 |
EquivRules.setup #> |
|
287 |
RspRules.setup #> |
|
288 |
PrsRules.setup #> |
|
289 |
IdSimps.setup #> |
|
290 |
QuotientRules.setup |
|
291 |
||
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
292 |
|
41452 | 293 |
(* outer syntax commands *) |
294 |
||
295 |
val _ = |
|
296 |
Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag |
|
297 |
(Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of))) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
298 |
|
41452 | 299 |
val _ = |
300 |
Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag |
|
301 |
(Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
302 |
|
41452 | 303 |
val _ = |
304 |
Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag |
|
305 |
(Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
306 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
307 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
308 |
end; (* structure *) |