kuncar@48153
|
1 |
(* Title: HOL/Tools/Lifting/lifting_setup.ML
|
kuncar@48153
|
2 |
Author: Ondrej Kuncar
|
kuncar@48153
|
3 |
|
huffman@48210
|
4 |
Setting up the lifting infrastructure.
|
kuncar@48153
|
5 |
*)
|
kuncar@48153
|
6 |
|
kuncar@48153
|
7 |
signature LIFTING_SETUP =
|
kuncar@48153
|
8 |
sig
|
kuncar@48153
|
9 |
exception SETUP_LIFTING_INFR of string
|
kuncar@48153
|
10 |
|
kuncar@52511
|
11 |
val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
|
kuncar@48153
|
12 |
|
kuncar@48437
|
13 |
val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
|
kuncar@54788
|
14 |
|
kuncar@54788
|
15 |
val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
|
kuncar@54788
|
16 |
end
|
kuncar@48153
|
17 |
|
huffman@48205
|
18 |
structure Lifting_Setup: LIFTING_SETUP =
|
kuncar@48153
|
19 |
struct
|
kuncar@48153
|
20 |
|
kuncar@48569
|
21 |
open Lifting_Util
|
kuncar@48569
|
22 |
|
kuncar@48153
|
23 |
infix 0 MRSL
|
kuncar@48153
|
24 |
|
kuncar@48153
|
25 |
exception SETUP_LIFTING_INFR of string
|
kuncar@48153
|
26 |
|
kuncar@51242
|
27 |
fun define_crel rep_fun lthy =
|
kuncar@48153
|
28 |
let
|
kuncar@48219
|
29 |
val (qty, rty) = (dest_funT o fastype_of) rep_fun
|
kuncar@48219
|
30 |
val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
|
kuncar@52511
|
31 |
val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph))
|
kuncar@51190
|
32 |
val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
|
kuncar@51242
|
33 |
val crel_name = Binding.prefix_name "cr_" qty_name
|
kuncar@48153
|
34 |
val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
|
kuncar@48153
|
35 |
val ((_, (_ , def_thm)), lthy'') =
|
kuncar@51242
|
36 |
Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy'
|
kuncar@48153
|
37 |
in
|
kuncar@48153
|
38 |
(def_thm, lthy'')
|
kuncar@48153
|
39 |
end
|
kuncar@48153
|
40 |
|
kuncar@51242
|
41 |
fun print_define_pcrel_warning msg =
|
kuncar@51242
|
42 |
let
|
kuncar@51242
|
43 |
val warning_msg = cat_lines
|
kuncar@51242
|
44 |
["Generation of a parametrized correspondence relation failed.",
|
kuncar@51242
|
45 |
(Pretty.string_of (Pretty.block
|
kuncar@51242
|
46 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))]
|
kuncar@51242
|
47 |
in
|
kuncar@51242
|
48 |
warning warning_msg
|
kuncar@51242
|
49 |
end
|
kuncar@51242
|
50 |
|
kuncar@51242
|
51 |
fun define_pcrel crel lthy =
|
kuncar@51242
|
52 |
let
|
kuncar@51303
|
53 |
val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
|
kuncar@51303
|
54 |
val [rty', qty] = (binder_types o fastype_of) fixed_crel
|
kuncar@51303
|
55 |
val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty'
|
kuncar@51303
|
56 |
val rty_raw = (domain_type o range_type o fastype_of) param_rel
|
kuncar@51242
|
57 |
val thy = Proof_Context.theory_of lthy
|
kuncar@51242
|
58 |
val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty
|
kuncar@51303
|
59 |
val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel
|
kuncar@51303
|
60 |
val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args
|
kuncar@51303
|
61 |
val lthy = Variable.declare_names fixed_crel lthy
|
kuncar@51303
|
62 |
val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy
|
kuncar@51303
|
63 |
val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
|
kuncar@51303
|
64 |
val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
|
kuncar@51303
|
65 |
val rty = (domain_type o fastype_of) param_rel_fixed
|
kuncar@51242
|
66 |
val relcomp_op = Const (@{const_name "relcompp"},
|
kuncar@51242
|
67 |
(rty --> rty' --> HOLogic.boolT) -->
|
kuncar@51242
|
68 |
(rty' --> qty --> HOLogic.boolT) -->
|
kuncar@51242
|
69 |
rty --> qty --> HOLogic.boolT)
|
kuncar@51303
|
70 |
val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
|
kuncar@51242
|
71 |
val qty_name = (fst o dest_Type) qty
|
kuncar@51242
|
72 |
val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
|
kuncar@51303
|
73 |
val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
|
kuncar@52511
|
74 |
val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
|
kuncar@51242
|
75 |
val definition_term = Logic.mk_equals (lhs, rhs)
|
kuncar@51242
|
76 |
val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)),
|
kuncar@51242
|
77 |
((Binding.empty, []), definition_term)) lthy
|
kuncar@51242
|
78 |
in
|
kuncar@51242
|
79 |
(SOME def_thm, lthy)
|
kuncar@51242
|
80 |
end
|
kuncar@51242
|
81 |
handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
|
kuncar@51242
|
82 |
|
kuncar@52511
|
83 |
|
kuncar@52511
|
84 |
local
|
kuncar@52511
|
85 |
val eq_OO_meta = mk_meta_eq @{thm eq_OO}
|
kuncar@52511
|
86 |
|
kuncar@52511
|
87 |
fun print_generate_pcr_cr_eq_error ctxt term =
|
kuncar@52511
|
88 |
let
|
kuncar@52511
|
89 |
val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
|
kuncar@52511
|
90 |
val error_msg = cat_lines
|
kuncar@52511
|
91 |
["Generation of a pcr_cr_eq failed.",
|
kuncar@52511
|
92 |
(Pretty.string_of (Pretty.block
|
kuncar@52511
|
93 |
[Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
|
kuncar@52511
|
94 |
"Most probably a relator_eq rule for one of the involved types is missing."]
|
kuncar@52511
|
95 |
in
|
kuncar@52511
|
96 |
error error_msg
|
kuncar@52511
|
97 |
end
|
kuncar@52511
|
98 |
in
|
kuncar@52511
|
99 |
fun define_pcr_cr_eq lthy pcr_rel_def =
|
kuncar@52511
|
100 |
let
|
kuncar@52511
|
101 |
val lhs = (term_of o Thm.lhs_of) pcr_rel_def
|
kuncar@52511
|
102 |
val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs
|
kuncar@52511
|
103 |
val args = (snd o strip_comb) lhs
|
kuncar@52511
|
104 |
|
kuncar@52511
|
105 |
fun make_inst var ctxt =
|
kuncar@52511
|
106 |
let
|
kuncar@52511
|
107 |
val typ = (snd o relation_types o snd o dest_Var) var
|
kuncar@52511
|
108 |
val sort = Type.sort_of_atyp typ
|
kuncar@52511
|
109 |
val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
|
kuncar@52511
|
110 |
val thy = Proof_Context.theory_of ctxt
|
kuncar@52511
|
111 |
in
|
kuncar@52511
|
112 |
((cterm_of thy var, cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
|
kuncar@52511
|
113 |
end
|
kuncar@52511
|
114 |
|
kuncar@52511
|
115 |
val orig_lthy = lthy
|
kuncar@52511
|
116 |
val (args_inst, lthy) = fold_map make_inst args lthy
|
kuncar@52511
|
117 |
val pcr_cr_eq =
|
kuncar@52511
|
118 |
pcr_rel_def
|
kuncar@52511
|
119 |
|> Drule.cterm_instantiate args_inst
|
kuncar@54020
|
120 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv
|
kuncar@54020
|
121 |
(Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
|
kuncar@52511
|
122 |
in
|
kuncar@52511
|
123 |
case (term_of o Thm.rhs_of) pcr_cr_eq of
|
kuncar@52511
|
124 |
Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ =>
|
kuncar@52511
|
125 |
let
|
kuncar@52511
|
126 |
val thm =
|
kuncar@52511
|
127 |
pcr_cr_eq
|
kuncar@52511
|
128 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
|
kuncar@52511
|
129 |
|> mk_HOL_eq
|
kuncar@52511
|
130 |
|> singleton (Variable.export lthy orig_lthy)
|
kuncar@52511
|
131 |
val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []),
|
kuncar@52511
|
132 |
[thm]) lthy
|
kuncar@52511
|
133 |
in
|
kuncar@52511
|
134 |
(thm, lthy)
|
kuncar@52511
|
135 |
end
|
kuncar@52511
|
136 |
| Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
|
kuncar@52511
|
137 |
| _ => error "generate_pcr_cr_eq: implementation error"
|
kuncar@52511
|
138 |
end
|
kuncar@52511
|
139 |
end
|
kuncar@52511
|
140 |
|
kuncar@48952
|
141 |
fun define_code_constr gen_code quot_thm lthy =
|
kuncar@48952
|
142 |
let
|
kuncar@48966
|
143 |
val abs = quot_thm_abs quot_thm
|
kuncar@48952
|
144 |
in
|
kuncar@52511
|
145 |
if gen_code andalso is_Const abs then
|
kuncar@48952
|
146 |
let
|
kuncar@52511
|
147 |
val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
|
kuncar@48952
|
148 |
in
|
kuncar@52511
|
149 |
Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
|
kuncar@48952
|
150 |
end
|
kuncar@48952
|
151 |
else
|
kuncar@48952
|
152 |
lthy
|
kuncar@48952
|
153 |
end
|
kuncar@48952
|
154 |
|
kuncar@48952
|
155 |
fun define_abs_type gen_code quot_thm lthy =
|
kuncar@48952
|
156 |
if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
|
kuncar@48153
|
157 |
let
|
kuncar@48153
|
158 |
val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
|
kuncar@48153
|
159 |
val add_abstype_attribute =
|
kuncar@48153
|
160 |
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
|
kuncar@52511
|
161 |
val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
|
kuncar@48153
|
162 |
in
|
kuncar@48153
|
163 |
lthy
|
kuncar@48153
|
164 |
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
|
kuncar@48153
|
165 |
end
|
kuncar@48153
|
166 |
else
|
kuncar@48153
|
167 |
lthy
|
kuncar@48153
|
168 |
|
kuncar@54788
|
169 |
local
|
kuncar@54788
|
170 |
exception QUOT_ERROR of Pretty.T list
|
kuncar@54788
|
171 |
in
|
kuncar@48237
|
172 |
fun quot_thm_sanity_check ctxt quot_thm =
|
kuncar@48237
|
173 |
let
|
kuncar@54788
|
174 |
val _ =
|
kuncar@54788
|
175 |
if (nprems_of quot_thm > 0) then
|
kuncar@54788
|
176 |
raise QUOT_ERROR [Pretty.block
|
kuncar@54788
|
177 |
[Pretty.str "The Quotient theorem has extra assumptions:",
|
kuncar@54788
|
178 |
Pretty.brk 1,
|
kuncar@54788
|
179 |
Display.pretty_thm ctxt quot_thm]]
|
kuncar@54788
|
180 |
else ()
|
kuncar@54788
|
181 |
val _ = quot_thm |> concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
|
kuncar@54788
|
182 |
handle TERM _ => raise QUOT_ERROR
|
kuncar@54788
|
183 |
[Pretty.block
|
kuncar@54788
|
184 |
[Pretty.str "The Quotient theorem is not of the right form:",
|
kuncar@54788
|
185 |
Pretty.brk 1,
|
kuncar@54788
|
186 |
Display.pretty_thm ctxt quot_thm]]
|
kuncar@48237
|
187 |
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
|
kuncar@48966
|
188 |
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
|
kuncar@48237
|
189 |
val rty_tfreesT = Term.add_tfree_namesT rty []
|
kuncar@48237
|
190 |
val qty_tfreesT = Term.add_tfree_namesT qty []
|
kuncar@48237
|
191 |
val extra_rty_tfrees =
|
kuncar@48411
|
192 |
case subtract (op =) qty_tfreesT rty_tfreesT of
|
kuncar@48237
|
193 |
[] => []
|
kuncar@48237
|
194 |
| extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
|
kuncar@48237
|
195 |
Pretty.brk 1] @
|
kuncar@48237
|
196 |
((Pretty.commas o map (Pretty.str o quote)) extras) @
|
kuncar@48411
|
197 |
[Pretty.str "."])]
|
kuncar@48237
|
198 |
val not_type_constr =
|
kuncar@48411
|
199 |
case qty of
|
kuncar@48237
|
200 |
Type _ => []
|
kuncar@48237
|
201 |
| _ => [Pretty.block [Pretty.str "The quotient type ",
|
kuncar@48237
|
202 |
Pretty.quote (Syntax.pretty_typ ctxt' qty),
|
kuncar@48237
|
203 |
Pretty.brk 1,
|
kuncar@48411
|
204 |
Pretty.str "is not a type constructor."]]
|
kuncar@48237
|
205 |
val errs = extra_rty_tfrees @ not_type_constr
|
kuncar@48237
|
206 |
in
|
kuncar@54788
|
207 |
if null errs then () else raise QUOT_ERROR errs
|
kuncar@54788
|
208 |
end
|
kuncar@54788
|
209 |
handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"]
|
kuncar@54788
|
210 |
@ (map (Pretty.string_of o Pretty.item o single) errs)))
|
kuncar@54788
|
211 |
end
|
kuncar@54788
|
212 |
|
kuncar@54788
|
213 |
fun lifting_bundle qty_full_name qinfo lthy =
|
kuncar@54788
|
214 |
let
|
kuncar@54788
|
215 |
fun qualify suffix defname = Binding.qualified true suffix defname
|
kuncar@54788
|
216 |
val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
|
kuncar@54788
|
217 |
val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
|
kuncar@54788
|
218 |
val bundle_name = Name_Space.full_name (Name_Space.naming_of
|
kuncar@54788
|
219 |
(Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
|
kuncar@54788
|
220 |
fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
|
kuncar@54788
|
221 |
|
kuncar@54788
|
222 |
val thy = Proof_Context.theory_of lthy
|
kuncar@54788
|
223 |
val dummy_thm = Thm.transfer thy Drule.dummy_thm
|
kuncar@54788
|
224 |
val pointer = Outer_Syntax.scan Position.none bundle_name
|
kuncar@54788
|
225 |
val restore_lifting_att =
|
kuncar@54788
|
226 |
([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
|
kuncar@54788
|
227 |
in
|
kuncar@54788
|
228 |
lthy
|
kuncar@54788
|
229 |
|> Local_Theory.declaration {syntax = false, pervasive = true}
|
kuncar@54788
|
230 |
(fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
|
kuncar@54788
|
231 |
|> Bundle.bundle ((binding, [restore_lifting_att])) []
|
kuncar@48237
|
232 |
end
|
kuncar@48237
|
233 |
|
kuncar@52511
|
234 |
fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
|
kuncar@48153
|
235 |
let
|
kuncar@48237
|
236 |
val _ = quot_thm_sanity_check lthy quot_thm
|
kuncar@48966
|
237 |
val (_, qtyp) = quot_thm_rty_qty quot_thm
|
kuncar@51242
|
238 |
val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy
|
kuncar@52511
|
239 |
(**)
|
kuncar@52511
|
240 |
val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
|
kuncar@52511
|
241 |
(**)
|
kuncar@52511
|
242 |
val (pcr_cr_eq, lthy) = case pcrel_def of
|
kuncar@52511
|
243 |
SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
|
kuncar@52511
|
244 |
| NONE => (NONE, lthy)
|
kuncar@54356
|
245 |
val pcr_info = case pcrel_def of
|
kuncar@52511
|
246 |
SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
|
kuncar@52511
|
247 |
| NONE => NONE
|
kuncar@54356
|
248 |
val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
|
kuncar@51242
|
249 |
val qty_full_name = (fst o dest_Type) qtyp
|
kuncar@54356
|
250 |
fun quot_info phi = Lifting_Info.transform_quotient phi quotients
|
kuncar@53131
|
251 |
val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
|
kuncar@52511
|
252 |
val lthy = case opt_reflp_thm of
|
kuncar@48952
|
253 |
SOME reflp_thm => lthy
|
kuncar@53131
|
254 |
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
|
kuncar@48952
|
255 |
[reflp_thm])
|
kuncar@53131
|
256 |
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
|
kuncar@48997
|
257 |
[[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
|
kuncar@48952
|
258 |
|> define_code_constr gen_code quot_thm
|
kuncar@48952
|
259 |
| NONE => lthy
|
kuncar@48952
|
260 |
|> define_abs_type gen_code quot_thm
|
kuncar@48153
|
261 |
in
|
kuncar@51242
|
262 |
lthy
|
kuncar@48153
|
263 |
|> Local_Theory.declaration {syntax = false, pervasive = true}
|
kuncar@48153
|
264 |
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
|
kuncar@54788
|
265 |
|> lifting_bundle qty_full_name quotients
|
kuncar@48153
|
266 |
end
|
kuncar@48153
|
267 |
|
kuncar@53093
|
268 |
local
|
kuncar@53093
|
269 |
fun importT_inst_exclude exclude ts ctxt =
|
kuncar@53093
|
270 |
let
|
kuncar@54788
|
271 |
val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
|
kuncar@54788
|
272 |
val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
|
kuncar@53093
|
273 |
in (tvars ~~ map TFree tfrees, ctxt') end
|
kuncar@53093
|
274 |
|
kuncar@53093
|
275 |
fun import_inst_exclude exclude ts ctxt =
|
kuncar@53093
|
276 |
let
|
kuncar@53093
|
277 |
val excludeT = fold (Term.add_tvarsT o snd) exclude []
|
kuncar@54788
|
278 |
val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
|
kuncar@53093
|
279 |
val vars = map (apsnd (Term_Subst.instantiateT instT))
|
kuncar@54788
|
280 |
(rev (subtract op= exclude (fold Term.add_vars ts [])))
|
kuncar@54788
|
281 |
val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
|
kuncar@54788
|
282 |
val inst = vars ~~ map Free (xs ~~ map #2 vars)
|
kuncar@53093
|
283 |
in ((instT, inst), ctxt'') end
|
kuncar@53093
|
284 |
|
kuncar@53093
|
285 |
fun import_terms_exclude exclude ts ctxt =
|
kuncar@53093
|
286 |
let val (inst, ctxt') = import_inst_exclude exclude ts ctxt
|
kuncar@53093
|
287 |
in (map (Term_Subst.instantiate inst) ts, ctxt') end
|
kuncar@53093
|
288 |
in
|
kuncar@53093
|
289 |
fun reduce_goal not_fix goal tac ctxt =
|
kuncar@53093
|
290 |
let
|
kuncar@53093
|
291 |
val thy = Proof_Context.theory_of ctxt
|
kuncar@53093
|
292 |
val orig_ctxt = ctxt
|
kuncar@53093
|
293 |
val (fixed_goal, ctxt) = yield_singleton (import_terms_exclude not_fix) goal ctxt
|
kuncar@53093
|
294 |
val init_goal = Goal.init (cterm_of thy fixed_goal)
|
kuncar@53093
|
295 |
in
|
kuncar@53093
|
296 |
(singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
|
kuncar@53093
|
297 |
end
|
kuncar@53093
|
298 |
end
|
kuncar@53093
|
299 |
|
kuncar@52511
|
300 |
local
|
kuncar@52511
|
301 |
val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
|
kuncar@52511
|
302 |
in
|
kuncar@52511
|
303 |
fun parametrize_class_constraint ctxt pcr_def constraint =
|
kuncar@52511
|
304 |
let
|
kuncar@52511
|
305 |
fun generate_transfer_rule pcr_def constraint goal ctxt =
|
kuncar@52511
|
306 |
let
|
kuncar@52511
|
307 |
val thy = Proof_Context.theory_of ctxt
|
kuncar@52511
|
308 |
val orig_ctxt = ctxt
|
kuncar@52511
|
309 |
val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
|
kuncar@52511
|
310 |
val init_goal = Goal.init (cterm_of thy fixed_goal)
|
kuncar@52511
|
311 |
val rules = Transfer.get_transfer_raw ctxt
|
kuncar@52511
|
312 |
val rules = constraint :: OO_rules @ rules
|
kuncar@52511
|
313 |
val tac = K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac rules)
|
kuncar@52511
|
314 |
in
|
kuncar@52511
|
315 |
(singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
|
kuncar@52511
|
316 |
end
|
kuncar@52511
|
317 |
|
kuncar@52511
|
318 |
fun make_goal pcr_def constr =
|
kuncar@52511
|
319 |
let
|
kuncar@52511
|
320 |
val pred_name = (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o prop_of) constr
|
kuncar@52511
|
321 |
val arg = (fst o Logic.dest_equals o prop_of) pcr_def
|
kuncar@52511
|
322 |
in
|
kuncar@52511
|
323 |
HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
|
kuncar@52511
|
324 |
end
|
kuncar@52511
|
325 |
|
kuncar@52511
|
326 |
val check_assms =
|
kuncar@52511
|
327 |
let
|
kuncar@52511
|
328 |
val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
|
kuncar@52511
|
329 |
|
kuncar@52511
|
330 |
fun is_right_name name = member op= right_names (Long_Name.base_name name)
|
kuncar@52511
|
331 |
|
kuncar@52511
|
332 |
fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
|
kuncar@52511
|
333 |
| is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
|
kuncar@52511
|
334 |
| is_trivial_assm _ = false
|
kuncar@52511
|
335 |
in
|
kuncar@52511
|
336 |
fn thm =>
|
kuncar@52511
|
337 |
let
|
kuncar@52511
|
338 |
val prems = map HOLogic.dest_Trueprop (prems_of thm)
|
kuncar@52511
|
339 |
val thm_name = (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o concl_of) thm
|
kuncar@52511
|
340 |
val non_trivial_assms = filter_out is_trivial_assm prems
|
kuncar@52511
|
341 |
in
|
kuncar@52511
|
342 |
if null non_trivial_assms then ()
|
kuncar@52511
|
343 |
else
|
kuncar@52511
|
344 |
let
|
kuncar@52511
|
345 |
val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
|
kuncar@52511
|
346 |
Pretty.str thm_name,
|
kuncar@52511
|
347 |
Pretty.str " transfer rule found:",
|
kuncar@52511
|
348 |
Pretty.brk 1] @
|
kuncar@52511
|
349 |
((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
|
kuncar@52511
|
350 |
[Pretty.str "."])
|
kuncar@52511
|
351 |
in
|
kuncar@52511
|
352 |
warning (Pretty.str_of pretty_msg)
|
kuncar@52511
|
353 |
end
|
kuncar@52511
|
354 |
end
|
kuncar@52511
|
355 |
end
|
kuncar@52511
|
356 |
|
kuncar@52511
|
357 |
val goal = make_goal pcr_def constraint
|
kuncar@52511
|
358 |
val thm = generate_transfer_rule pcr_def constraint goal ctxt
|
kuncar@52511
|
359 |
val _ = check_assms thm
|
kuncar@52511
|
360 |
in
|
kuncar@52511
|
361 |
thm
|
kuncar@52511
|
362 |
end
|
kuncar@52511
|
363 |
end
|
kuncar@52511
|
364 |
|
kuncar@52511
|
365 |
local
|
kuncar@52511
|
366 |
val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
|
kuncar@52511
|
367 |
in
|
kuncar@52511
|
368 |
fun generate_parametric_id lthy rty id_transfer_rule =
|
kuncar@52511
|
369 |
let
|
kuncar@52511
|
370 |
val orig_lthy = lthy
|
kuncar@52511
|
371 |
(* it doesn't raise an exception because it would have already raised it in define_pcrel *)
|
kuncar@52511
|
372 |
val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
|
kuncar@54788
|
373 |
val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
|
kuncar@52511
|
374 |
val lthy = orig_lthy
|
kuncar@52511
|
375 |
val id_transfer =
|
kuncar@52511
|
376 |
@{thm id_transfer}
|
kuncar@52511
|
377 |
|> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
|
kuncar@52511
|
378 |
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
|
kuncar@54788
|
379 |
val var = Var (hd (Term.add_vars (prop_of id_transfer) []))
|
kuncar@54788
|
380 |
val thy = Proof_Context.theory_of lthy
|
kuncar@52511
|
381 |
val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
|
kuncar@54788
|
382 |
val id_par_thm = Drule.cterm_instantiate inst id_transfer
|
kuncar@52511
|
383 |
in
|
kuncar@52511
|
384 |
Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
|
kuncar@52511
|
385 |
end
|
kuncar@52511
|
386 |
handle Lifting_Term.MERGE_TRANSFER_REL msg =>
|
kuncar@52511
|
387 |
let
|
kuncar@52511
|
388 |
val error_msg = cat_lines
|
kuncar@52511
|
389 |
["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
|
kuncar@52511
|
390 |
"A non-parametric version will be used.",
|
kuncar@52511
|
391 |
(Pretty.string_of (Pretty.block
|
kuncar@52511
|
392 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))]
|
kuncar@52511
|
393 |
in
|
kuncar@52511
|
394 |
(warning error_msg; id_transfer_rule)
|
kuncar@52511
|
395 |
end
|
kuncar@52511
|
396 |
end
|
kuncar@52511
|
397 |
|
kuncar@53093
|
398 |
local
|
kuncar@53093
|
399 |
fun rewrite_first_Domainp_arg rewr_thm thm = Conv.fconv_rule (Conv.concl_conv ~1 (HOLogic.Trueprop_conv
|
kuncar@53093
|
400 |
(Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv rewr_thm))))) thm
|
kuncar@53093
|
401 |
|
kuncar@53093
|
402 |
fun fold_Domainp_pcrel pcrel_def thm =
|
kuncar@53093
|
403 |
let
|
kuncar@53093
|
404 |
val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
|
kuncar@53093
|
405 |
val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
|
kuncar@53093
|
406 |
val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
|
kuncar@54788
|
407 |
handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
|
kuncar@53093
|
408 |
in
|
kuncar@53093
|
409 |
rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
|
kuncar@53093
|
410 |
end
|
kuncar@53093
|
411 |
|
kuncar@53093
|
412 |
fun reduce_Domainp ctxt rules thm =
|
kuncar@53093
|
413 |
let
|
kuncar@53093
|
414 |
val goal = thm |> prems_of |> hd
|
kuncar@53093
|
415 |
val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var
|
kuncar@53093
|
416 |
val reduced_assm = reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac rules) 1)) ctxt
|
kuncar@53093
|
417 |
in
|
kuncar@53093
|
418 |
reduced_assm RS thm
|
kuncar@53093
|
419 |
end
|
kuncar@53093
|
420 |
in
|
kuncar@54356
|
421 |
fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt =
|
kuncar@53093
|
422 |
let
|
kuncar@53093
|
423 |
fun reduce_first_assm ctxt rules thm =
|
kuncar@53093
|
424 |
let
|
kuncar@53093
|
425 |
val goal = thm |> prems_of |> hd
|
kuncar@53093
|
426 |
val reduced_assm = reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac rules) 1)) ctxt
|
kuncar@53093
|
427 |
in
|
kuncar@53093
|
428 |
reduced_assm RS thm
|
kuncar@53093
|
429 |
end
|
kuncar@53093
|
430 |
|
kuncar@54356
|
431 |
val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection}
|
kuncar@53093
|
432 |
val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
|
kuncar@54356
|
433 |
val pcrel_def = #pcrel_def pcr_info
|
kuncar@53093
|
434 |
val pcr_Domainp_par_left_total =
|
kuncar@53093
|
435 |
(dom_thm RS @{thm pcr_Domainp_par_left_total})
|
kuncar@53093
|
436 |
|> fold_Domainp_pcrel pcrel_def
|
kuncar@53093
|
437 |
|> reduce_first_assm ctxt (Lifting_Info.get_reflexivity_rules ctxt)
|
kuncar@53093
|
438 |
val pcr_Domainp_par =
|
kuncar@53093
|
439 |
(dom_thm RS @{thm pcr_Domainp_par})
|
kuncar@53093
|
440 |
|> fold_Domainp_pcrel pcrel_def
|
kuncar@53093
|
441 |
|> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
|
kuncar@53093
|
442 |
val pcr_Domainp =
|
kuncar@53093
|
443 |
(dom_thm RS @{thm pcr_Domainp})
|
kuncar@53093
|
444 |
|> fold_Domainp_pcrel pcrel_def
|
kuncar@53093
|
445 |
val thms =
|
kuncar@53093
|
446 |
[("domain", pcr_Domainp),
|
kuncar@53093
|
447 |
("domain_par", pcr_Domainp_par),
|
kuncar@53093
|
448 |
("domain_par_left_total", pcr_Domainp_par_left_total),
|
kuncar@53093
|
449 |
("domain_eq", pcr_Domainp_eq)]
|
kuncar@53093
|
450 |
in
|
kuncar@53093
|
451 |
thms
|
kuncar@53093
|
452 |
end
|
kuncar@53093
|
453 |
|
kuncar@53093
|
454 |
fun parametrize_total_domain bi_total pcrel_def ctxt =
|
kuncar@53093
|
455 |
let
|
kuncar@53093
|
456 |
val thm =
|
kuncar@53093
|
457 |
(bi_total RS @{thm pcr_Domainp_total})
|
kuncar@53093
|
458 |
|> fold_Domainp_pcrel pcrel_def
|
kuncar@53093
|
459 |
|> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
|
kuncar@53093
|
460 |
in
|
kuncar@53093
|
461 |
[("domain", thm)]
|
kuncar@53093
|
462 |
end
|
kuncar@53093
|
463 |
|
kuncar@53093
|
464 |
end
|
kuncar@52511
|
465 |
|
kuncar@52511
|
466 |
fun get_pcrel_info ctxt qty_full_name =
|
kuncar@54356
|
467 |
#pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
|
kuncar@52511
|
468 |
|
kuncar@53093
|
469 |
fun get_Domainp_thm quot_thm =
|
kuncar@53093
|
470 |
the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}])
|
kuncar@53093
|
471 |
|
kuncar@48723
|
472 |
(*
|
kuncar@48723
|
473 |
Sets up the Lifting package by a quotient theorem.
|
kuncar@48723
|
474 |
|
kuncar@48952
|
475 |
gen_code - flag if an abstract type given by quot_thm should be registred
|
kuncar@48723
|
476 |
as an abstract type in the code generator
|
kuncar@48723
|
477 |
quot_thm - a quotient theorem (Quotient R Abs Rep T)
|
kuncar@52511
|
478 |
opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
|
kuncar@48723
|
479 |
(in the form "reflp R")
|
kuncar@48723
|
480 |
*)
|
kuncar@48723
|
481 |
|
kuncar@52511
|
482 |
fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
|
kuncar@48392
|
483 |
let
|
kuncar@52511
|
484 |
(**)
|
kuncar@52511
|
485 |
val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
|
kuncar@52511
|
486 |
(**)
|
kuncar@48392
|
487 |
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
|
kuncar@53093
|
488 |
val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add)
|
kuncar@52511
|
489 |
val (rty, qty) = quot_thm_rty_qty quot_thm
|
huffman@48446
|
490 |
val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
|
kuncar@52511
|
491 |
val qty_full_name = (fst o dest_Type) qty
|
kuncar@52511
|
492 |
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
|
kuncar@48411
|
493 |
fun qualify suffix = Binding.qualified true suffix qty_name
|
kuncar@52511
|
494 |
val lthy = case opt_reflp_thm of
|
kuncar@52511
|
495 |
SOME reflp_thm =>
|
kuncar@52511
|
496 |
let
|
kuncar@52511
|
497 |
val thms =
|
kuncar@52511
|
498 |
[("abs_induct", @{thm Quotient_total_abs_induct}, [induct_attr]),
|
kuncar@52511
|
499 |
("abs_eq_iff", @{thm Quotient_total_abs_eq_iff}, [] )]
|
kuncar@52511
|
500 |
in
|
kuncar@52511
|
501 |
lthy
|
kuncar@52511
|
502 |
|> fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr),
|
kuncar@52511
|
503 |
[[quot_thm, reflp_thm] MRSL thm])) thms
|
kuncar@52511
|
504 |
end
|
kuncar@52511
|
505 |
| NONE =>
|
kuncar@52511
|
506 |
let
|
kuncar@52511
|
507 |
val thms =
|
kuncar@52511
|
508 |
[("abs_induct", @{thm Quotient_abs_induct}, [induct_attr])]
|
kuncar@52511
|
509 |
in
|
kuncar@52511
|
510 |
fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr),
|
kuncar@52511
|
511 |
[quot_thm RS thm])) thms lthy
|
kuncar@52511
|
512 |
end
|
kuncar@53093
|
513 |
val dom_thm = get_Domainp_thm quot_thm
|
kuncar@52511
|
514 |
|
kuncar@52511
|
515 |
fun setup_transfer_rules_nonpar lthy =
|
kuncar@52511
|
516 |
let
|
kuncar@52511
|
517 |
val lthy =
|
kuncar@52511
|
518 |
case opt_reflp_thm of
|
kuncar@52511
|
519 |
SOME reflp_thm =>
|
kuncar@52511
|
520 |
let
|
kuncar@52511
|
521 |
val thms =
|
kuncar@52511
|
522 |
[("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
|
kuncar@52511
|
523 |
("bi_total", @{thm Quotient_bi_total} )]
|
kuncar@52511
|
524 |
in
|
kuncar@52511
|
525 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@52511
|
526 |
[[quot_thm, reflp_thm] MRSL thm])) thms lthy
|
kuncar@52511
|
527 |
end
|
kuncar@52511
|
528 |
| NONE =>
|
kuncar@53093
|
529 |
lthy
|
kuncar@53093
|
530 |
|> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm])
|
kuncar@53093
|
531 |
|
kuncar@52511
|
532 |
val thms =
|
kuncar@52511
|
533 |
[("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}),
|
kuncar@52511
|
534 |
("right_unique", @{thm Quotient_right_unique} ),
|
kuncar@52511
|
535 |
("right_total", @{thm Quotient_right_total} )]
|
kuncar@52511
|
536 |
in
|
kuncar@52511
|
537 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@52511
|
538 |
[quot_thm RS thm])) thms lthy
|
kuncar@52511
|
539 |
end
|
kuncar@52511
|
540 |
|
kuncar@52511
|
541 |
fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
|
kuncar@52511
|
542 |
option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
|
kuncar@52511
|
543 |
handle Lifting_Term.MERGE_TRANSFER_REL msg =>
|
kuncar@52511
|
544 |
let
|
kuncar@52511
|
545 |
val error_msg = cat_lines
|
kuncar@52511
|
546 |
["Generation of a parametric transfer rule for the quotient relation failed.",
|
kuncar@52511
|
547 |
(Pretty.string_of (Pretty.block
|
kuncar@52511
|
548 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))]
|
kuncar@52511
|
549 |
in
|
kuncar@52511
|
550 |
error error_msg
|
kuncar@52511
|
551 |
end
|
kuncar@52511
|
552 |
|
kuncar@52511
|
553 |
fun setup_transfer_rules_par lthy =
|
kuncar@52511
|
554 |
let
|
kuncar@53093
|
555 |
val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
|
kuncar@53093
|
556 |
val pcrel_def = #pcrel_def pcrel_info
|
kuncar@52511
|
557 |
val lthy =
|
kuncar@52511
|
558 |
case opt_reflp_thm of
|
kuncar@52511
|
559 |
SOME reflp_thm =>
|
kuncar@52511
|
560 |
let
|
kuncar@53093
|
561 |
val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
|
kuncar@53093
|
562 |
val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
|
kuncar@52511
|
563 |
val id_abs_transfer = generate_parametric_id lthy rty
|
kuncar@52511
|
564 |
(Lifting_Term.parametrize_transfer_rule lthy
|
kuncar@52511
|
565 |
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
|
kuncar@53093
|
566 |
val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
|
kuncar@52511
|
567 |
val thms =
|
kuncar@52511
|
568 |
[("id_abs_transfer",id_abs_transfer),
|
kuncar@52511
|
569 |
("bi_total", bi_total )]
|
kuncar@52511
|
570 |
in
|
kuncar@53093
|
571 |
lthy
|
kuncar@53093
|
572 |
|> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@53093
|
573 |
[thm])) thms
|
kuncar@53093
|
574 |
|> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
|
kuncar@53093
|
575 |
[thm])) domain_thms
|
kuncar@52511
|
576 |
end
|
kuncar@52511
|
577 |
| NONE =>
|
kuncar@52511
|
578 |
let
|
kuncar@53093
|
579 |
val thms = parametrize_domain dom_thm pcrel_info lthy
|
kuncar@52511
|
580 |
in
|
kuncar@53093
|
581 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
|
kuncar@53093
|
582 |
[thm])) thms lthy
|
kuncar@52511
|
583 |
end
|
kuncar@53093
|
584 |
|
kuncar@52511
|
585 |
val rel_eq_transfer = generate_parametric_rel_eq lthy
|
kuncar@52511
|
586 |
(Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
|
kuncar@52511
|
587 |
opt_par_thm
|
kuncar@52511
|
588 |
val right_unique = parametrize_class_constraint lthy pcrel_def
|
kuncar@52511
|
589 |
(quot_thm RS @{thm Quotient_right_unique})
|
kuncar@52511
|
590 |
val right_total = parametrize_class_constraint lthy pcrel_def
|
kuncar@52511
|
591 |
(quot_thm RS @{thm Quotient_right_total})
|
kuncar@52511
|
592 |
val thms =
|
kuncar@52511
|
593 |
[("rel_eq_transfer", rel_eq_transfer),
|
kuncar@52511
|
594 |
("right_unique", right_unique ),
|
kuncar@52511
|
595 |
("right_total", right_total )]
|
kuncar@52511
|
596 |
in
|
kuncar@52511
|
597 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@52511
|
598 |
[thm])) thms lthy
|
kuncar@52511
|
599 |
end
|
kuncar@52511
|
600 |
|
kuncar@52511
|
601 |
fun setup_transfer_rules lthy =
|
kuncar@52511
|
602 |
if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
|
kuncar@52511
|
603 |
else setup_transfer_rules_nonpar lthy
|
kuncar@48392
|
604 |
in
|
kuncar@51242
|
605 |
lthy
|
kuncar@52511
|
606 |
|> setup_lifting_infr gen_code quot_thm opt_reflp_thm
|
kuncar@52511
|
607 |
|> setup_transfer_rules
|
kuncar@48392
|
608 |
end
|
kuncar@48392
|
609 |
|
kuncar@48723
|
610 |
(*
|
kuncar@48723
|
611 |
Sets up the Lifting package by a typedef theorem.
|
kuncar@48723
|
612 |
|
kuncar@48952
|
613 |
gen_code - flag if an abstract type given by typedef_thm should be registred
|
kuncar@48723
|
614 |
as an abstract type in the code generator
|
kuncar@48723
|
615 |
typedef_thm - a typedef theorem (type_definition Rep Abs S)
|
kuncar@48723
|
616 |
*)
|
kuncar@48723
|
617 |
|
kuncar@48952
|
618 |
fun setup_by_typedef_thm gen_code typedef_thm lthy =
|
kuncar@48153
|
619 |
let
|
kuncar@48392
|
620 |
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
|
kuncar@53093
|
621 |
val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add)
|
kuncar@48392
|
622 |
val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
|
kuncar@52511
|
623 |
val (T_def, lthy) = define_crel rep_fun lthy
|
kuncar@52511
|
624 |
(**)
|
kuncar@52511
|
625 |
val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
|
kuncar@52511
|
626 |
(**)
|
kuncar@48411
|
627 |
val quot_thm = case typedef_set of
|
kuncar@48392
|
628 |
Const ("Orderings.top_class.top", _) =>
|
kuncar@48392
|
629 |
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
|
kuncar@48392
|
630 |
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
|
kuncar@48392
|
631 |
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
|
kuncar@48392
|
632 |
| _ =>
|
kuncar@48411
|
633 |
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
|
kuncar@52511
|
634 |
val (rty, qty) = quot_thm_rty_qty quot_thm
|
kuncar@52511
|
635 |
val qty_full_name = (fst o dest_Type) qty
|
kuncar@52511
|
636 |
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
|
kuncar@48411
|
637 |
fun qualify suffix = Binding.qualified true suffix qty_name
|
kuncar@52511
|
638 |
val opt_reflp_thm =
|
kuncar@52511
|
639 |
case typedef_set of
|
kuncar@52511
|
640 |
Const ("Orderings.top_class.top", _) =>
|
kuncar@52511
|
641 |
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
|
kuncar@52511
|
642 |
| _ => NONE
|
kuncar@53093
|
643 |
val dom_thm = get_Domainp_thm quot_thm
|
kuncar@53131
|
644 |
val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
|
kuncar@48411
|
645 |
|
kuncar@52511
|
646 |
fun setup_transfer_rules_nonpar lthy =
|
kuncar@52511
|
647 |
let
|
kuncar@52511
|
648 |
val lthy =
|
kuncar@52511
|
649 |
case opt_reflp_thm of
|
kuncar@52511
|
650 |
SOME reflp_thm =>
|
kuncar@52511
|
651 |
let
|
kuncar@52511
|
652 |
val thms =
|
kuncar@52511
|
653 |
[("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
|
kuncar@52511
|
654 |
("bi_total", @{thm Quotient_bi_total} )]
|
kuncar@52511
|
655 |
in
|
kuncar@52511
|
656 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@52511
|
657 |
[[quot_thm, reflp_thm] MRSL thm])) thms lthy
|
kuncar@52511
|
658 |
end
|
kuncar@52511
|
659 |
| NONE =>
|
kuncar@53093
|
660 |
lthy
|
kuncar@53093
|
661 |
|> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm])
|
kuncar@52511
|
662 |
val thms =
|
kuncar@52511
|
663 |
[("rep_transfer", @{thm typedef_rep_transfer}),
|
kuncar@52511
|
664 |
("bi_unique", @{thm typedef_bi_unique} ),
|
kuncar@52511
|
665 |
("right_unique", @{thm typedef_right_unique}),
|
kuncar@52511
|
666 |
("right_total", @{thm typedef_right_total} )]
|
kuncar@52511
|
667 |
in
|
kuncar@52511
|
668 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@52511
|
669 |
[[typedef_thm, T_def] MRSL thm])) thms lthy
|
kuncar@52511
|
670 |
end
|
kuncar@52511
|
671 |
|
kuncar@52511
|
672 |
fun setup_transfer_rules_par lthy =
|
kuncar@52511
|
673 |
let
|
kuncar@53093
|
674 |
val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
|
kuncar@53093
|
675 |
val pcrel_def = #pcrel_def pcrel_info
|
kuncar@53093
|
676 |
|
kuncar@52511
|
677 |
val lthy =
|
kuncar@52511
|
678 |
case opt_reflp_thm of
|
kuncar@52511
|
679 |
SOME reflp_thm =>
|
kuncar@52511
|
680 |
let
|
kuncar@53093
|
681 |
val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
|
kuncar@53093
|
682 |
val domain_thms = parametrize_total_domain bi_total pcrel_def lthy
|
kuncar@53093
|
683 |
val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
|
kuncar@52511
|
684 |
val id_abs_transfer = generate_parametric_id lthy rty
|
kuncar@52511
|
685 |
(Lifting_Term.parametrize_transfer_rule lthy
|
kuncar@52511
|
686 |
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
|
kuncar@52511
|
687 |
val thms =
|
kuncar@53093
|
688 |
[("bi_total", bi_total ),
|
kuncar@53093
|
689 |
("id_abs_transfer",id_abs_transfer)]
|
kuncar@52511
|
690 |
in
|
kuncar@53093
|
691 |
lthy
|
kuncar@53093
|
692 |
|> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@53093
|
693 |
[thm])) thms
|
kuncar@53093
|
694 |
|> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
|
kuncar@53093
|
695 |
[thm])) domain_thms
|
kuncar@52511
|
696 |
end
|
kuncar@52511
|
697 |
| NONE =>
|
kuncar@52511
|
698 |
let
|
kuncar@53093
|
699 |
val thms = parametrize_domain dom_thm pcrel_info lthy
|
kuncar@52511
|
700 |
in
|
kuncar@53093
|
701 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]),
|
kuncar@53093
|
702 |
[thm])) thms lthy
|
kuncar@52511
|
703 |
end
|
kuncar@53093
|
704 |
|
kuncar@52511
|
705 |
val thms =
|
kuncar@52511
|
706 |
("rep_transfer", generate_parametric_id lthy rty
|
kuncar@52511
|
707 |
(Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
|
kuncar@52511
|
708 |
::
|
kuncar@52511
|
709 |
(map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
|
kuncar@52511
|
710 |
[("bi_unique", @{thm typedef_bi_unique} ),
|
kuncar@52511
|
711 |
("right_unique", @{thm typedef_right_unique}),
|
kuncar@52511
|
712 |
("right_total", @{thm typedef_right_total} )])
|
kuncar@52511
|
713 |
in
|
kuncar@52511
|
714 |
fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
|
kuncar@52511
|
715 |
[thm])) thms lthy
|
kuncar@52511
|
716 |
end
|
kuncar@52511
|
717 |
|
kuncar@52511
|
718 |
fun setup_transfer_rules lthy =
|
kuncar@52511
|
719 |
if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
|
kuncar@52511
|
720 |
else setup_transfer_rules_nonpar lthy
|
kuncar@52511
|
721 |
|
kuncar@48153
|
722 |
in
|
kuncar@52511
|
723 |
lthy
|
kuncar@48958
|
724 |
|> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []),
|
kuncar@52511
|
725 |
[quot_thm])
|
kuncar@53131
|
726 |
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
|
kuncar@53131
|
727 |
[[typedef_thm, T_def] MRSL @{thm typedef_left_unique}])
|
kuncar@52511
|
728 |
|> setup_lifting_infr gen_code quot_thm opt_reflp_thm
|
kuncar@52511
|
729 |
|> setup_transfer_rules
|
kuncar@48153
|
730 |
end
|
kuncar@48153
|
731 |
|
kuncar@52511
|
732 |
fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
|
kuncar@48392
|
733 |
let
|
kuncar@48392
|
734 |
val input_thm = singleton (Attrib.eval_thms lthy) xthm
|
kuncar@48392
|
735 |
val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
|
kuncar@48437
|
736 |
handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
|
kuncar@48437
|
737 |
|
kuncar@48437
|
738 |
fun sanity_check_reflp_thm reflp_thm =
|
kuncar@48437
|
739 |
let
|
kuncar@48437
|
740 |
val reflp_tm = (HOLogic.dest_Trueprop o prop_of) reflp_thm
|
kuncar@48437
|
741 |
handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
|
kuncar@48437
|
742 |
in
|
kuncar@48437
|
743 |
case reflp_tm of
|
kuncar@48437
|
744 |
Const (@{const_name reflp}, _) $ _ => ()
|
kuncar@48437
|
745 |
| _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
|
kuncar@48437
|
746 |
end
|
kuncar@48437
|
747 |
|
kuncar@48437
|
748 |
fun setup_quotient () =
|
kuncar@52511
|
749 |
let
|
kuncar@52511
|
750 |
val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
|
kuncar@52511
|
751 |
val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
|
kuncar@52511
|
752 |
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
|
kuncar@52511
|
753 |
in
|
kuncar@52511
|
754 |
setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
|
kuncar@52511
|
755 |
end
|
kuncar@52511
|
756 |
|
kuncar@48437
|
757 |
|
kuncar@48437
|
758 |
fun setup_typedef () =
|
kuncar@48437
|
759 |
case opt_reflp_xthm of
|
kuncar@48437
|
760 |
SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
|
kuncar@55221
|
761 |
| NONE => (
|
kuncar@55221
|
762 |
case opt_par_xthm of
|
kuncar@55221
|
763 |
SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
|
kuncar@55221
|
764 |
| NONE => setup_by_typedef_thm gen_code input_thm lthy
|
kuncar@55221
|
765 |
)
|
kuncar@48392
|
766 |
in
|
kuncar@48392
|
767 |
case input_term of
|
kuncar@48437
|
768 |
(Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
|
kuncar@48437
|
769 |
| (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
|
kuncar@48392
|
770 |
| _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
|
kuncar@48392
|
771 |
end
|
kuncar@48153
|
772 |
|
kuncar@48952
|
773 |
val opt_gen_code =
|
kuncar@48952
|
774 |
Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
|
kuncar@48437
|
775 |
|
kuncar@48153
|
776 |
val _ =
|
kuncar@48153
|
777 |
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
|
wenzelm@51229
|
778 |
"setup lifting infrastructure"
|
kuncar@52511
|
779 |
(opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm
|
kuncar@52511
|
780 |
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >>
|
kuncar@52511
|
781 |
(fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) =>
|
kuncar@52511
|
782 |
setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
|
kuncar@54788
|
783 |
|
kuncar@54788
|
784 |
(* restoring lifting infrastructure *)
|
kuncar@54788
|
785 |
|
kuncar@54788
|
786 |
local
|
kuncar@54788
|
787 |
exception PCR_ERROR of Pretty.T list
|
kuncar@54788
|
788 |
in
|
kuncar@54788
|
789 |
|
kuncar@54788
|
790 |
fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
|
kuncar@54788
|
791 |
let
|
kuncar@54788
|
792 |
val quot_thm = (#quot_thm qinfo)
|
kuncar@54788
|
793 |
val _ = quot_thm_sanity_check ctxt quot_thm
|
kuncar@54788
|
794 |
val pcr_info_err =
|
kuncar@54788
|
795 |
(case #pcr_info qinfo of
|
kuncar@54788
|
796 |
SOME pcr =>
|
kuncar@54788
|
797 |
let
|
kuncar@54788
|
798 |
val pcrel_def = #pcrel_def pcr
|
kuncar@54788
|
799 |
val pcr_cr_eq = #pcr_cr_eq pcr
|
kuncar@54788
|
800 |
val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def)
|
kuncar@54788
|
801 |
handle TERM _ => raise PCR_ERROR [Pretty.block
|
kuncar@54788
|
802 |
[Pretty.str "The pcr definiton theorem is not a plain meta equation:",
|
kuncar@54788
|
803 |
Pretty.brk 1,
|
kuncar@54788
|
804 |
Display.pretty_thm ctxt pcrel_def]]
|
kuncar@54788
|
805 |
val pcr_const_def = head_of def_lhs
|
kuncar@54788
|
806 |
val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq))
|
kuncar@54788
|
807 |
handle TERM _ => raise PCR_ERROR [Pretty.block
|
kuncar@54788
|
808 |
[Pretty.str "The pcr_cr equation theorem is not a plain equation:",
|
kuncar@54788
|
809 |
Pretty.brk 1,
|
kuncar@54788
|
810 |
Display.pretty_thm ctxt pcr_cr_eq]]
|
kuncar@54788
|
811 |
val (pcr_const_eq, eqs) = strip_comb eq_lhs
|
kuncar@54788
|
812 |
fun is_eq (Const ("HOL.eq", _)) = true
|
kuncar@54788
|
813 |
| is_eq _ = false
|
kuncar@54788
|
814 |
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
|
kuncar@54788
|
815 |
| eq_Const _ _ = false
|
kuncar@54788
|
816 |
val all_eqs = if not (forall is_eq eqs) then
|
kuncar@54788
|
817 |
[Pretty.block
|
kuncar@54788
|
818 |
[Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
|
kuncar@54788
|
819 |
Pretty.brk 1,
|
kuncar@54788
|
820 |
Display.pretty_thm ctxt pcr_cr_eq]]
|
kuncar@54788
|
821 |
else []
|
kuncar@54788
|
822 |
val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
|
kuncar@54788
|
823 |
[Pretty.block
|
kuncar@54788
|
824 |
[Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
|
kuncar@54788
|
825 |
Pretty.brk 1,
|
kuncar@54788
|
826 |
Syntax.pretty_term ctxt pcr_const_def,
|
kuncar@54788
|
827 |
Pretty.brk 1,
|
kuncar@54788
|
828 |
Pretty.str "vs.",
|
kuncar@54788
|
829 |
Pretty.brk 1,
|
kuncar@54788
|
830 |
Syntax.pretty_term ctxt pcr_const_eq]]
|
kuncar@54788
|
831 |
else []
|
kuncar@54788
|
832 |
val crel = quot_thm_crel quot_thm
|
kuncar@54788
|
833 |
val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
|
kuncar@54788
|
834 |
[Pretty.block
|
kuncar@54788
|
835 |
[Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
|
kuncar@54788
|
836 |
Pretty.brk 1,
|
kuncar@54788
|
837 |
Syntax.pretty_term ctxt crel,
|
kuncar@54788
|
838 |
Pretty.brk 1,
|
kuncar@54788
|
839 |
Pretty.str "vs.",
|
kuncar@54788
|
840 |
Pretty.brk 1,
|
kuncar@54788
|
841 |
Syntax.pretty_term ctxt eq_rhs]]
|
kuncar@54788
|
842 |
else []
|
kuncar@54788
|
843 |
in
|
kuncar@54788
|
844 |
all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
|
kuncar@54788
|
845 |
end
|
kuncar@54788
|
846 |
| NONE => [])
|
kuncar@54788
|
847 |
val errs = pcr_info_err
|
kuncar@54788
|
848 |
in
|
kuncar@54788
|
849 |
if null errs then () else raise PCR_ERROR errs
|
kuncar@54788
|
850 |
end
|
kuncar@54788
|
851 |
handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"]
|
kuncar@54788
|
852 |
@ (map (Pretty.string_of o Pretty.item o single) errs)))
|
kuncar@54788
|
853 |
end
|
kuncar@54788
|
854 |
|
kuncar@54788
|
855 |
fun lifting_restore qinfo ctxt =
|
kuncar@54788
|
856 |
let
|
kuncar@54788
|
857 |
val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
|
kuncar@54788
|
858 |
val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
|
kuncar@54788
|
859 |
val qty_full_name = (fst o dest_Type) qty
|
kuncar@54788
|
860 |
val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
|
kuncar@54788
|
861 |
in
|
kuncar@54788
|
862 |
if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
|
kuncar@54788
|
863 |
then error (Pretty.string_of
|
kuncar@54788
|
864 |
(Pretty.block
|
kuncar@54788
|
865 |
[Pretty.str "Lifting is already setup for the type",
|
kuncar@54788
|
866 |
Pretty.brk 1,
|
kuncar@54788
|
867 |
Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
|
kuncar@54788
|
868 |
else Lifting_Info.update_quotients qty_full_name qinfo ctxt
|
kuncar@54788
|
869 |
end
|
kuncar@54788
|
870 |
|
kuncar@54788
|
871 |
val parse_opt_pcr =
|
kuncar@54788
|
872 |
Scan.optional (Attrib.thm -- Attrib.thm >>
|
kuncar@54788
|
873 |
(fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
|
kuncar@54788
|
874 |
|
kuncar@54788
|
875 |
val lifting_restore_attribute_setup =
|
kuncar@54788
|
876 |
Attrib.setup @{binding lifting_restore}
|
kuncar@54788
|
877 |
((Attrib.thm -- parse_opt_pcr) >>
|
kuncar@54788
|
878 |
(fn (quot_thm, opt_pcr) =>
|
kuncar@54788
|
879 |
let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
|
kuncar@54788
|
880 |
in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
|
kuncar@54788
|
881 |
"restoring lifting infrastructure"
|
kuncar@54788
|
882 |
|
kuncar@54788
|
883 |
val _ = Theory.setup lifting_restore_attribute_setup
|
kuncar@54788
|
884 |
|
kuncar@54788
|
885 |
fun lifting_restore_internal bundle_name ctxt =
|
kuncar@54788
|
886 |
let
|
kuncar@54788
|
887 |
val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
|
kuncar@54788
|
888 |
in
|
kuncar@54788
|
889 |
case restore_info of
|
kuncar@54788
|
890 |
SOME restore_info =>
|
kuncar@54788
|
891 |
ctxt
|
kuncar@54788
|
892 |
|> lifting_restore (#quotient restore_info)
|
kuncar@54788
|
893 |
|> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
|
kuncar@54788
|
894 |
| NONE => ctxt
|
kuncar@54788
|
895 |
end
|
kuncar@54788
|
896 |
|
kuncar@54788
|
897 |
val lifting_restore_internal_attribute_setup =
|
kuncar@54788
|
898 |
Attrib.setup @{binding lifting_restore_internal}
|
kuncar@54788
|
899 |
(Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
|
kuncar@54788
|
900 |
"restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
|
kuncar@54788
|
901 |
|
kuncar@54788
|
902 |
val _ = Theory.setup lifting_restore_internal_attribute_setup
|
kuncar@54788
|
903 |
|
kuncar@54788
|
904 |
(* lifting_forget *)
|
kuncar@54788
|
905 |
|
kuncar@54788
|
906 |
val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
|
kuncar@54788
|
907 |
@{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
|
kuncar@54788
|
908 |
|
kuncar@54788
|
909 |
fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
|
kuncar@54788
|
910 |
| fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $
|
kuncar@54788
|
911 |
(Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
|
kuncar@54788
|
912 |
| fold_transfer_rel f (Const (name, _) $ rel) =
|
kuncar@54788
|
913 |
if member op= monotonicity_names name then f rel else f @{term undefined}
|
kuncar@54788
|
914 |
| fold_transfer_rel f _ = f @{term undefined}
|
kuncar@54788
|
915 |
|
kuncar@54788
|
916 |
fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
|
kuncar@54788
|
917 |
let
|
kuncar@54788
|
918 |
val transfer_rel_name = transfer_rel |> dest_Const |> fst;
|
kuncar@54788
|
919 |
fun has_transfer_rel thm =
|
kuncar@54788
|
920 |
let
|
kuncar@54788
|
921 |
val concl = thm |> concl_of |> HOLogic.dest_Trueprop
|
kuncar@54788
|
922 |
in
|
kuncar@54788
|
923 |
member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
|
kuncar@54788
|
924 |
end
|
kuncar@54788
|
925 |
handle TERM _ => false
|
kuncar@54788
|
926 |
in
|
kuncar@54788
|
927 |
filter has_transfer_rel transfer_rules
|
kuncar@54788
|
928 |
end
|
kuncar@54788
|
929 |
|
kuncar@54788
|
930 |
type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
|
kuncar@54788
|
931 |
|
kuncar@54891
|
932 |
fun get_transfer_rel (qinfo : Lifting_Info.quotient) =
|
kuncar@54788
|
933 |
let
|
kuncar@54788
|
934 |
fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
|
kuncar@54788
|
935 |
in
|
kuncar@54788
|
936 |
if is_some (#pcr_info qinfo)
|
kuncar@54788
|
937 |
then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
|
kuncar@54788
|
938 |
else quot_thm_crel (#quot_thm qinfo)
|
kuncar@54788
|
939 |
end
|
kuncar@54788
|
940 |
|
kuncar@54788
|
941 |
fun pointer_of_bundle_name bundle_name ctxt =
|
kuncar@54788
|
942 |
let
|
kuncar@54788
|
943 |
val bundle_name = Bundle.check ctxt bundle_name
|
kuncar@54788
|
944 |
val bundle = Bundle.the_bundle ctxt bundle_name
|
kuncar@54788
|
945 |
in
|
kuncar@54788
|
946 |
case bundle of
|
kuncar@54788
|
947 |
[(_, [arg_src])] =>
|
kuncar@54788
|
948 |
(let
|
kuncar@54788
|
949 |
val ((_, tokens), _) = Args.dest_src arg_src
|
kuncar@54788
|
950 |
in
|
kuncar@54788
|
951 |
(fst (Args.name tokens))
|
kuncar@54788
|
952 |
handle _ => error "The provided bundle is not a lifting bundle."
|
kuncar@54788
|
953 |
end)
|
kuncar@54788
|
954 |
| _ => error "The provided bundle is not a lifting bundle."
|
kuncar@54788
|
955 |
end
|
kuncar@54788
|
956 |
|
kuncar@54788
|
957 |
fun lifting_forget pointer lthy =
|
kuncar@54788
|
958 |
let
|
kuncar@54788
|
959 |
fun get_transfer_rules_to_delete qinfo ctxt =
|
kuncar@54788
|
960 |
let
|
kuncar@54891
|
961 |
val transfer_rel = get_transfer_rel qinfo
|
kuncar@54788
|
962 |
in
|
kuncar@54788
|
963 |
filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
|
kuncar@54788
|
964 |
end
|
kuncar@54788
|
965 |
in
|
kuncar@54788
|
966 |
case Lifting_Info.lookup_restore_data lthy pointer of
|
kuncar@54788
|
967 |
SOME restore_info =>
|
kuncar@54788
|
968 |
let
|
kuncar@54788
|
969 |
val qinfo = #quotient restore_info
|
kuncar@54788
|
970 |
val quot_thm = #quot_thm qinfo
|
kuncar@54788
|
971 |
val transfer_rules = get_transfer_rules_to_delete qinfo lthy
|
kuncar@54788
|
972 |
in
|
kuncar@54788
|
973 |
Local_Theory.declaration {syntax = false, pervasive = true}
|
kuncar@54788
|
974 |
(K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
|
kuncar@54788
|
975 |
lthy
|
kuncar@54788
|
976 |
end
|
kuncar@54788
|
977 |
| NONE => error "The lifting bundle refers to non-existent restore data."
|
kuncar@54788
|
978 |
end
|
kuncar@54788
|
979 |
|
kuncar@54788
|
980 |
|
kuncar@54788
|
981 |
fun lifting_forget_cmd bundle_name lthy =
|
kuncar@54788
|
982 |
lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
|
kuncar@54788
|
983 |
|
kuncar@54788
|
984 |
|
kuncar@54788
|
985 |
val _ =
|
kuncar@54788
|
986 |
Outer_Syntax.local_theory @{command_spec "lifting_forget"}
|
kuncar@54788
|
987 |
"unsetup Lifting and Transfer for the given lifting bundle"
|
kuncar@54788
|
988 |
(Parse.position Parse.xname >> (lifting_forget_cmd))
|
kuncar@54788
|
989 |
|
kuncar@54788
|
990 |
(* lifting_update *)
|
kuncar@54788
|
991 |
|
kuncar@54788
|
992 |
fun update_transfer_rules pointer lthy =
|
kuncar@54788
|
993 |
let
|
kuncar@54891
|
994 |
fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy =
|
kuncar@54788
|
995 |
let
|
kuncar@54788
|
996 |
val transfer_rel = get_transfer_rel qinfo
|
kuncar@54788
|
997 |
val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
|
kuncar@54788
|
998 |
in
|
kuncar@54788
|
999 |
fn phi => fold_rev
|
kuncar@54788
|
1000 |
(Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
|
kuncar@54788
|
1001 |
end
|
kuncar@54788
|
1002 |
in
|
kuncar@54788
|
1003 |
case Lifting_Info.lookup_restore_data lthy pointer of
|
kuncar@54788
|
1004 |
SOME refresh_data =>
|
kuncar@54788
|
1005 |
Local_Theory.declaration {syntax = false, pervasive = true}
|
kuncar@54788
|
1006 |
(fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer
|
kuncar@54788
|
1007 |
(new_transfer_rules refresh_data lthy phi)) lthy
|
kuncar@54788
|
1008 |
| NONE => error "The lifting bundle refers to non-existent restore data."
|
kuncar@54788
|
1009 |
end
|
kuncar@54788
|
1010 |
|
kuncar@54788
|
1011 |
fun lifting_update_cmd bundle_name lthy =
|
kuncar@54788
|
1012 |
update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
|
kuncar@54788
|
1013 |
|
kuncar@54788
|
1014 |
val _ =
|
kuncar@54788
|
1015 |
Outer_Syntax.local_theory @{command_spec "lifting_update"}
|
kuncar@54788
|
1016 |
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
|
kuncar@54788
|
1017 |
(Parse.position Parse.xname >> lifting_update_cmd)
|
kuncar@54788
|
1018 |
|
kuncar@54788
|
1019 |
end
|