author | kuncar |
Thu, 24 May 2012 14:20:23 +0200 | |
changeset 47982 | 7aa35601ff65 |
parent 47951 | 8c8a03765de7 |
child 50227 | 01d545993e8c |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Tools/Lifting/lifting_info.ML |
2 |
Author: Ondrej Kuncar |
|
3 |
||
4 |
Context data for the lifting package. |
|
5 |
*) |
|
6 |
||
7 |
signature LIFTING_INFO = |
|
8 |
sig |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
9 |
type quotmaps = {rel_quot_thm: thm} |
47308 | 10 |
val lookup_quotmaps: Proof.context -> string -> quotmaps option |
11 |
val lookup_quotmaps_global: theory -> string -> quotmaps option |
|
12 |
val print_quotmaps: Proof.context -> unit |
|
13 |
||
14 |
type quotients = {quot_thm: thm} |
|
15 |
val transform_quotients: morphism -> quotients -> quotients |
|
16 |
val lookup_quotients: Proof.context -> string -> quotients option |
|
17 |
val lookup_quotients_global: theory -> string -> quotients option |
|
18 |
val update_quotients: string -> quotients -> Context.generic -> Context.generic |
|
19 |
val dest_quotients: Proof.context -> quotients list |
|
20 |
val print_quotients: Proof.context -> unit |
|
21 |
||
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
22 |
val get_invariant_commute_rules: Proof.context -> thm list |
47936
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
23 |
|
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
24 |
val get_reflexivity_rules: Proof.context -> thm list |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
25 |
val add_reflexivity_rule_attribute: attribute |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
26 |
val add_reflexivity_rule_attrib: Attrib.src |
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
27 |
|
47308 | 28 |
val setup: theory -> theory |
29 |
end; |
|
30 |
||
31 |
structure Lifting_Info: LIFTING_INFO = |
|
32 |
struct |
|
33 |
||
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
34 |
open Lifting_Util |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
35 |
|
47308 | 36 |
(** data containers **) |
37 |
||
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
38 |
(* info about Quotient map theorems *) |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
39 |
type quotmaps = {rel_quot_thm: thm} |
47308 | 40 |
|
41 |
structure Quotmaps = Generic_Data |
|
42 |
( |
|
43 |
type T = quotmaps Symtab.table |
|
44 |
val empty = Symtab.empty |
|
45 |
val extend = I |
|
46 |
fun merge data = Symtab.merge (K true) data |
|
47 |
) |
|
48 |
||
49 |
val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof |
|
50 |
val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory |
|
51 |
||
52 |
(* FIXME export proper internal update operation!? *) |
|
53 |
||
47784 | 54 |
fun quot_map_thm_sanity_check rel_quot_thm ctxt = |
55 |
let |
|
56 |
fun quot_term_absT ctxt quot_term = |
|
57 |
let |
|
58 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term |
|
59 |
handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block |
|
60 |
[Pretty.str "The Quotient map theorem is not in the right form.", |
|
61 |
Pretty.brk 1, |
|
62 |
Pretty.str "The following term is not the Quotient predicate:", |
|
63 |
Pretty.brk 1, |
|
64 |
Syntax.pretty_term ctxt t])) |
|
65 |
in |
|
66 |
fastype_of abs |
|
67 |
end |
|
68 |
||
69 |
val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt |
|
70 |
val rel_quot_thm_prop = prop_of rel_quot_thm_fixed |
|
71 |
val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop |
|
72 |
val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop; |
|
73 |
val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl |
|
74 |
val concl_tfrees = Term.add_tfree_namesT (concl_absT) [] |
|
75 |
val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) |
|
76 |
rel_quot_thm_prems [] |
|
77 |
val extra_prem_tfrees = |
|
78 |
case subtract (op =) concl_tfrees prems_tfrees of |
|
79 |
[] => [] |
|
80 |
| extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:", |
|
81 |
Pretty.brk 1] @ |
|
82 |
((Pretty.commas o map (Pretty.str o quote)) extras) @ |
|
83 |
[Pretty.str "."])] |
|
84 |
val errs = extra_prem_tfrees |
|
85 |
in |
|
86 |
if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] |
|
87 |
@ (map Pretty.string_of errs))) |
|
88 |
end |
|
89 |
||
90 |
||
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
91 |
fun add_quot_map rel_quot_thm ctxt = |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
92 |
let |
47784 | 93 |
val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
94 |
val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
95 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
96 |
val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
97 |
val minfo = {rel_quot_thm = rel_quot_thm} |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
98 |
in |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
99 |
Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
100 |
end |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
101 |
|
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
102 |
val quot_map_attribute_setup = |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
103 |
Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map)) |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
104 |
"declaration of the Quotient map theorem" |
47308 | 105 |
|
106 |
fun print_quotmaps ctxt = |
|
107 |
let |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
108 |
fun prt_map (ty_name, {rel_quot_thm}) = |
47308 | 109 |
Pretty.block (separate (Pretty.brk 2) |
110 |
[Pretty.str "type:", |
|
111 |
Pretty.str ty_name, |
|
112 |
Pretty.str "quot. theorem:", |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
113 |
Syntax.pretty_term ctxt (prop_of rel_quot_thm)]) |
47308 | 114 |
in |
115 |
map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) |
|
116 |
|> Pretty.big_list "maps for type constructors:" |
|
117 |
|> Pretty.writeln |
|
118 |
end |
|
119 |
||
120 |
(* info about quotient types *) |
|
121 |
type quotients = {quot_thm: thm} |
|
122 |
||
123 |
structure Quotients = Generic_Data |
|
124 |
( |
|
125 |
type T = quotients Symtab.table |
|
126 |
val empty = Symtab.empty |
|
127 |
val extend = I |
|
128 |
fun merge data = Symtab.merge (K true) data |
|
129 |
) |
|
130 |
||
131 |
fun transform_quotients phi {quot_thm} = |
|
132 |
{quot_thm = Morphism.thm phi quot_thm} |
|
133 |
||
134 |
val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof |
|
135 |
val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory |
|
136 |
||
137 |
fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) |
|
138 |
||
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
139 |
fun delete_quotients quot_thm ctxt = |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
140 |
let |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
141 |
val (_, qtyp) = quot_thm_rty_qty quot_thm |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
142 |
val qty_full_name = (fst o dest_Type) qtyp |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
143 |
val symtab = Quotients.get ctxt |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
144 |
val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
145 |
in |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
146 |
case maybe_stored_quot_thm of |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
147 |
SOME {quot_thm = stored_quot_thm} => |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
148 |
if Thm.eq_thm_prop (stored_quot_thm, quot_thm) then |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
149 |
Quotients.map (Symtab.delete qty_full_name) ctxt |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
150 |
else |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
151 |
ctxt |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
152 |
| NONE => ctxt |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
153 |
end |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
154 |
|
47308 | 155 |
fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *) |
156 |
map snd (Symtab.dest (Quotients.get (Context.Proof ctxt))) |
|
157 |
||
158 |
fun print_quotients ctxt = |
|
159 |
let |
|
160 |
fun prt_quot (qty_name, {quot_thm}) = |
|
161 |
Pretty.block (separate (Pretty.brk 2) |
|
162 |
[Pretty.str "type:", |
|
163 |
Pretty.str qty_name, |
|
164 |
Pretty.str "quot. thm:", |
|
165 |
Syntax.pretty_term ctxt (prop_of quot_thm)]) |
|
166 |
in |
|
167 |
map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt))) |
|
168 |
|> Pretty.big_list "quotients:" |
|
169 |
|> Pretty.writeln |
|
170 |
end |
|
171 |
||
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
172 |
val quot_del_attribute_setup = |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
173 |
Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients)) |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
174 |
"deletes the Quotient theorem" |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
175 |
|
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
176 |
structure Invariant_Commute = Named_Thms |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
177 |
( |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
178 |
val name = @{binding invariant_commute} |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
179 |
val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate" |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
180 |
) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
181 |
|
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
182 |
fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
183 |
|
47936
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
184 |
structure Reflp_Preserve = Named_Thms |
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
185 |
( |
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
186 |
val name = @{binding reflexivity_rule} |
47936
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
187 |
val description = "theorems that a relator preserves a reflexivity property" |
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
188 |
) |
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
189 |
|
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
190 |
val get_reflexivity_rules = Reflp_Preserve.get |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
191 |
val add_reflexivity_rule_attribute = Reflp_Preserve.add |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
192 |
val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute) |
47936
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
193 |
|
47308 | 194 |
(* theory setup *) |
195 |
||
196 |
val setup = |
|
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
197 |
quot_map_attribute_setup |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
198 |
#> quot_del_attribute_setup |
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
199 |
#> Invariant_Commute.setup |
47936
756f30eac792
infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents:
47784
diff
changeset
|
200 |
#> Reflp_Preserve.setup |
47308 | 201 |
|
202 |
(* outer syntax commands *) |
|
203 |
||
204 |
val _ = |
|
205 |
Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions" |
|
206 |
(Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of))) |
|
207 |
||
208 |
val _ = |
|
209 |
Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" |
|
210 |
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) |
|
211 |
||
212 |
end; |