kuncar@48153
|
1 |
(* Title: HOL/Tools/Lifting/lifting_def.ML
|
kuncar@48153
|
2 |
Author: Ondrej Kuncar
|
kuncar@48153
|
3 |
|
kuncar@48153
|
4 |
Definitions for constants on quotient types.
|
kuncar@48153
|
5 |
*)
|
kuncar@48153
|
6 |
|
kuncar@48153
|
7 |
signature LIFTING_DEF =
|
kuncar@48153
|
8 |
sig
|
kuncar@48153
|
9 |
val add_lift_def:
|
kuncar@48153
|
10 |
(binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
|
kuncar@48153
|
11 |
|
kuncar@48153
|
12 |
val lift_def_cmd:
|
kuncar@48153
|
13 |
(binding * string option * mixfix) * string -> local_theory -> Proof.state
|
kuncar@48153
|
14 |
|
kuncar@48153
|
15 |
val can_generate_code_cert: thm -> bool
|
kuncar@48153
|
16 |
end;
|
kuncar@48153
|
17 |
|
kuncar@48153
|
18 |
structure Lifting_Def: LIFTING_DEF =
|
kuncar@48153
|
19 |
struct
|
kuncar@48153
|
20 |
|
kuncar@48153
|
21 |
(** Interface and Syntax Setup **)
|
kuncar@48153
|
22 |
|
kuncar@48153
|
23 |
(* Generation of the code certificate from the rsp theorem *)
|
kuncar@48153
|
24 |
|
kuncar@48153
|
25 |
infix 0 MRSL
|
kuncar@48153
|
26 |
|
kuncar@48153
|
27 |
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
|
kuncar@48153
|
28 |
|
kuncar@48153
|
29 |
fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
|
kuncar@48153
|
30 |
| get_body_types (U, V) = (U, V)
|
kuncar@48153
|
31 |
|
kuncar@48153
|
32 |
fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
|
kuncar@48153
|
33 |
| get_binder_types _ = []
|
kuncar@48153
|
34 |
|
kuncar@48153
|
35 |
fun force_rty_type ctxt rty rhs =
|
kuncar@48153
|
36 |
let
|
kuncar@48153
|
37 |
val thy = Proof_Context.theory_of ctxt
|
kuncar@48153
|
38 |
val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
|
kuncar@48153
|
39 |
val rty_schematic = fastype_of rhs_schematic
|
kuncar@48153
|
40 |
val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty
|
kuncar@48153
|
41 |
in
|
kuncar@48153
|
42 |
Envir.subst_term_types match rhs_schematic
|
kuncar@48153
|
43 |
end
|
kuncar@48153
|
44 |
|
kuncar@48153
|
45 |
fun unabs_def ctxt def =
|
kuncar@48153
|
46 |
let
|
kuncar@48153
|
47 |
val (_, rhs) = Thm.dest_equals (cprop_of def)
|
kuncar@48153
|
48 |
fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
|
kuncar@48153
|
49 |
| dest_abs tm = raise TERM("get_abs_var",[tm])
|
kuncar@48153
|
50 |
val (var_name, T) = dest_abs (term_of rhs)
|
kuncar@48153
|
51 |
val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
|
kuncar@48153
|
52 |
val thy = Proof_Context.theory_of ctxt'
|
kuncar@48153
|
53 |
val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
|
kuncar@48153
|
54 |
in
|
kuncar@48153
|
55 |
Thm.combination def refl_thm |>
|
kuncar@48153
|
56 |
singleton (Proof_Context.export ctxt' ctxt)
|
kuncar@48153
|
57 |
end
|
kuncar@48153
|
58 |
|
kuncar@48153
|
59 |
fun unabs_all_def ctxt def =
|
kuncar@48153
|
60 |
let
|
kuncar@48153
|
61 |
val (_, rhs) = Thm.dest_equals (cprop_of def)
|
kuncar@48153
|
62 |
val xs = strip_abs_vars (term_of rhs)
|
kuncar@48153
|
63 |
in
|
kuncar@48153
|
64 |
fold (K (unabs_def ctxt)) xs def
|
kuncar@48153
|
65 |
end
|
kuncar@48153
|
66 |
|
kuncar@48153
|
67 |
val map_fun_unfolded =
|
kuncar@48153
|
68 |
@{thm map_fun_def[abs_def]} |>
|
kuncar@48153
|
69 |
unabs_def @{context} |>
|
kuncar@48153
|
70 |
unabs_def @{context} |>
|
kuncar@48153
|
71 |
Local_Defs.unfold @{context} [@{thm comp_def}]
|
kuncar@48153
|
72 |
|
kuncar@48153
|
73 |
fun unfold_fun_maps ctm =
|
kuncar@48153
|
74 |
let
|
kuncar@48153
|
75 |
fun unfold_conv ctm =
|
kuncar@48153
|
76 |
case (Thm.term_of ctm) of
|
kuncar@48153
|
77 |
Const (@{const_name "map_fun"}, _) $ _ $ _ =>
|
kuncar@48153
|
78 |
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
|
kuncar@48153
|
79 |
| _ => Conv.all_conv ctm
|
kuncar@48153
|
80 |
val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
|
kuncar@48153
|
81 |
in
|
kuncar@48153
|
82 |
(Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
|
kuncar@48153
|
83 |
end
|
kuncar@48153
|
84 |
|
kuncar@48153
|
85 |
fun prove_rel ctxt rsp_thm (rty, qty) =
|
kuncar@48153
|
86 |
let
|
kuncar@48153
|
87 |
val ty_args = get_binder_types (rty, qty)
|
kuncar@48153
|
88 |
fun disch_arg args_ty thm =
|
kuncar@48153
|
89 |
let
|
kuncar@48375
|
90 |
val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty
|
kuncar@48153
|
91 |
in
|
kuncar@48153
|
92 |
[quot_thm, thm] MRSL @{thm apply_rsp''}
|
kuncar@48153
|
93 |
end
|
kuncar@48153
|
94 |
in
|
kuncar@48153
|
95 |
fold disch_arg ty_args rsp_thm
|
kuncar@48153
|
96 |
end
|
kuncar@48153
|
97 |
|
kuncar@48153
|
98 |
exception CODE_CERT_GEN of string
|
kuncar@48153
|
99 |
|
kuncar@48153
|
100 |
fun simplify_code_eq ctxt def_thm =
|
kuncar@48153
|
101 |
Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
|
kuncar@48153
|
102 |
|
kuncar@48153
|
103 |
fun can_generate_code_cert quot_thm =
|
kuncar@48153
|
104 |
case Lifting_Term.quot_thm_rel quot_thm of
|
kuncar@48153
|
105 |
Const (@{const_name HOL.eq}, _) => true
|
kuncar@48153
|
106 |
| Const (@{const_name invariant}, _) $ _ => true
|
kuncar@48153
|
107 |
| _ => false
|
kuncar@48153
|
108 |
|
kuncar@48153
|
109 |
fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
|
kuncar@48153
|
110 |
let
|
kuncar@48153
|
111 |
val thy = Proof_Context.theory_of ctxt
|
kuncar@48375
|
112 |
val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
|
kuncar@48153
|
113 |
val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
|
kuncar@48153
|
114 |
val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
|
kuncar@48153
|
115 |
val abs_rep_eq =
|
kuncar@48153
|
116 |
case (HOLogic.dest_Trueprop o prop_of) fun_rel of
|
kuncar@48153
|
117 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
|
kuncar@48153
|
118 |
| Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
|
kuncar@48153
|
119 |
| _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
|
kuncar@48153
|
120 |
val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
|
kuncar@48153
|
121 |
val unabs_def = unabs_all_def ctxt unfolded_def
|
kuncar@48153
|
122 |
val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
|
kuncar@48153
|
123 |
val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
|
kuncar@48153
|
124 |
val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
|
kuncar@48153
|
125 |
val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
|
kuncar@48153
|
126 |
in
|
kuncar@48153
|
127 |
simplify_code_eq ctxt code_cert
|
kuncar@48153
|
128 |
end
|
kuncar@48153
|
129 |
|
kuncar@48437
|
130 |
fun is_abstype ctxt typ =
|
kuncar@48437
|
131 |
let
|
kuncar@48437
|
132 |
val thy = Proof_Context.theory_of ctxt
|
kuncar@48437
|
133 |
val type_name = (fst o dest_Type) typ
|
kuncar@48437
|
134 |
in
|
kuncar@48437
|
135 |
(snd oo Code.get_type) thy type_name
|
kuncar@48437
|
136 |
end
|
kuncar@48437
|
137 |
|
kuncar@48437
|
138 |
|
kuncar@48153
|
139 |
fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
|
kuncar@48153
|
140 |
let
|
kuncar@48437
|
141 |
val (rty_body, qty_body) = get_body_types (rty, qty)
|
kuncar@48437
|
142 |
val quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
|
kuncar@48153
|
143 |
in
|
kuncar@48153
|
144 |
if can_generate_code_cert quot_thm then
|
kuncar@48153
|
145 |
let
|
kuncar@48153
|
146 |
val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
|
kuncar@48153
|
147 |
val add_abs_eqn_attribute =
|
kuncar@48153
|
148 |
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
|
kuncar@48153
|
149 |
val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
|
kuncar@48437
|
150 |
val lthy' =
|
kuncar@48437
|
151 |
(snd oo Local_Theory.note) ((code_eqn_thm_name, []), [code_cert]) lthy
|
kuncar@48153
|
152 |
in
|
kuncar@48437
|
153 |
if is_abstype lthy qty_body then
|
kuncar@48437
|
154 |
(snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) lthy'
|
kuncar@48437
|
155 |
else
|
kuncar@48437
|
156 |
lthy'
|
kuncar@48153
|
157 |
end
|
kuncar@48153
|
158 |
else
|
kuncar@48153
|
159 |
lthy
|
kuncar@48153
|
160 |
end
|
kuncar@48153
|
161 |
|
kuncar@48153
|
162 |
fun define_code_eq code_eqn_thm_name def_thm lthy =
|
kuncar@48153
|
163 |
let
|
kuncar@48153
|
164 |
val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
|
kuncar@48153
|
165 |
val code_eq = unabs_all_def lthy unfolded_def
|
kuncar@48153
|
166 |
val simp_code_eq = simplify_code_eq lthy code_eq
|
kuncar@48153
|
167 |
in
|
kuncar@48153
|
168 |
lthy
|
kuncar@48153
|
169 |
|> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
|
kuncar@48153
|
170 |
end
|
kuncar@48153
|
171 |
|
kuncar@48153
|
172 |
fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
|
kuncar@48153
|
173 |
if body_type rty = body_type qty then
|
kuncar@48153
|
174 |
define_code_eq code_eqn_thm_name def_thm lthy
|
kuncar@48153
|
175 |
else
|
kuncar@48153
|
176 |
define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
|
kuncar@48153
|
177 |
|
kuncar@48153
|
178 |
|
kuncar@48153
|
179 |
fun add_lift_def var qty rhs rsp_thm lthy =
|
kuncar@48153
|
180 |
let
|
kuncar@48153
|
181 |
val rty = fastype_of rhs
|
kuncar@48375
|
182 |
val quotient_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
|
huffman@48209
|
183 |
val absrep_trm = Lifting_Term.quot_thm_abs quotient_thm
|
kuncar@48153
|
184 |
val rty_forced = (domain_type o fastype_of) absrep_trm
|
kuncar@48153
|
185 |
val forced_rhs = force_rty_type lthy rty_forced rhs
|
kuncar@48153
|
186 |
val lhs = Free (Binding.print (#1 var), qty)
|
kuncar@48153
|
187 |
val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
|
kuncar@48153
|
188 |
val (_, prop') = Local_Defs.cert_def lthy prop
|
kuncar@48153
|
189 |
val (_, newrhs) = Local_Defs.abs_def prop'
|
kuncar@48153
|
190 |
|
kuncar@48153
|
191 |
val ((_, (_ , def_thm)), lthy') =
|
kuncar@48153
|
192 |
Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
|
kuncar@48153
|
193 |
|
kuncar@48219
|
194 |
val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
|
huffman@48374
|
195 |
|> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
|
huffman@48209
|
196 |
|
kuncar@48411
|
197 |
fun qualify defname suffix = Binding.qualified true suffix defname
|
kuncar@48153
|
198 |
|
kuncar@48411
|
199 |
val lhs_name = (#1 var)
|
kuncar@48153
|
200 |
val rsp_thm_name = qualify lhs_name "rsp"
|
kuncar@48153
|
201 |
val code_eqn_thm_name = qualify lhs_name "rep_eq"
|
huffman@48209
|
202 |
val transfer_thm_name = qualify lhs_name "transfer"
|
huffman@48231
|
203 |
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
|
kuncar@48153
|
204 |
in
|
kuncar@48153
|
205 |
lthy'
|
kuncar@48153
|
206 |
|> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
|
huffman@48231
|
207 |
|> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
|
kuncar@48153
|
208 |
|> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
|
kuncar@48153
|
209 |
end
|
kuncar@48153
|
210 |
|
kuncar@48153
|
211 |
fun mk_readable_rsp_thm_eq tm lthy =
|
kuncar@48153
|
212 |
let
|
kuncar@48153
|
213 |
val ctm = cterm_of (Proof_Context.theory_of lthy) tm
|
kuncar@48153
|
214 |
|
kuncar@48153
|
215 |
fun norm_fun_eq ctm =
|
kuncar@48153
|
216 |
let
|
kuncar@48153
|
217 |
fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
|
kuncar@48153
|
218 |
fun erase_quants ctm' =
|
kuncar@48153
|
219 |
case (Thm.term_of ctm') of
|
kuncar@48153
|
220 |
Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm'
|
kuncar@48153
|
221 |
| _ => (Conv.binder_conv (K erase_quants) lthy then_conv
|
kuncar@48153
|
222 |
Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
|
kuncar@48153
|
223 |
in
|
kuncar@48153
|
224 |
(abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
|
kuncar@48153
|
225 |
end
|
kuncar@48153
|
226 |
|
kuncar@48153
|
227 |
fun simp_arrows_conv ctm =
|
kuncar@48153
|
228 |
let
|
kuncar@48153
|
229 |
val unfold_conv = Conv.rewrs_conv
|
kuncar@48153
|
230 |
[@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]},
|
kuncar@48153
|
231 |
@{thm fun_rel_def[THEN eq_reflection]}]
|
kuncar@48153
|
232 |
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
|
kuncar@48153
|
233 |
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
|
kuncar@48153
|
234 |
in
|
kuncar@48153
|
235 |
case (Thm.term_of ctm) of
|
kuncar@48153
|
236 |
Const (@{const_name "fun_rel"}, _) $ _ $ _ =>
|
kuncar@48153
|
237 |
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
|
kuncar@48153
|
238 |
| _ => Conv.all_conv ctm
|
kuncar@48153
|
239 |
end
|
kuncar@48153
|
240 |
|
kuncar@48153
|
241 |
val unfold_ret_val_invs = Conv.bottom_conv
|
kuncar@48153
|
242 |
(K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
|
kuncar@48153
|
243 |
val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
|
kuncar@48153
|
244 |
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
|
kuncar@48153
|
245 |
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
|
kuncar@48153
|
246 |
val beta_conv = Thm.beta_conversion true
|
kuncar@48153
|
247 |
val eq_thm =
|
kuncar@48153
|
248 |
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
|
kuncar@48153
|
249 |
in
|
kuncar@48153
|
250 |
Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
|
kuncar@48153
|
251 |
end
|
kuncar@48153
|
252 |
|
kuncar@48153
|
253 |
|
kuncar@48153
|
254 |
|
kuncar@48153
|
255 |
fun lift_def_cmd (raw_var, rhs_raw) lthy =
|
kuncar@48153
|
256 |
let
|
kuncar@48375
|
257 |
val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy
|
kuncar@48375
|
258 |
val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw
|
kuncar@48153
|
259 |
|
kuncar@48153
|
260 |
fun try_to_prove_refl thm =
|
kuncar@48153
|
261 |
let
|
kuncar@48153
|
262 |
val lhs_eq =
|
kuncar@48153
|
263 |
thm
|
kuncar@48153
|
264 |
|> prop_of
|
kuncar@48153
|
265 |
|> Logic.dest_implies
|
kuncar@48153
|
266 |
|> fst
|
kuncar@48153
|
267 |
|> strip_all_body
|
kuncar@48153
|
268 |
|> try HOLogic.dest_Trueprop
|
kuncar@48153
|
269 |
in
|
kuncar@48153
|
270 |
case lhs_eq of
|
kuncar@48153
|
271 |
SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
|
kuncar@48153
|
272 |
| _ => NONE
|
kuncar@48153
|
273 |
end
|
kuncar@48153
|
274 |
|
kuncar@48375
|
275 |
val rsp_rel = Lifting_Term.equiv_relation lthy' (fastype_of rhs, qty)
|
kuncar@48153
|
276 |
val rty_forced = (domain_type o fastype_of) rsp_rel;
|
kuncar@48375
|
277 |
val forced_rhs = force_rty_type lthy' rty_forced rhs;
|
kuncar@48153
|
278 |
val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
|
kuncar@48375
|
279 |
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
|
kuncar@48153
|
280 |
val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
|
kuncar@48153
|
281 |
val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
|
kuncar@48153
|
282 |
|
kuncar@48153
|
283 |
fun after_qed thm_list lthy =
|
kuncar@48153
|
284 |
let
|
kuncar@48153
|
285 |
val internal_rsp_thm =
|
kuncar@48153
|
286 |
case thm_list of
|
kuncar@48153
|
287 |
[] => the maybe_proven_rsp_thm
|
kuncar@48375
|
288 |
| [[thm]] => Goal.prove lthy [] [] internal_rsp_tm
|
kuncar@48153
|
289 |
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
|
kuncar@48153
|
290 |
in
|
kuncar@48153
|
291 |
add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy
|
kuncar@48153
|
292 |
end
|
kuncar@48153
|
293 |
|
kuncar@48153
|
294 |
in
|
kuncar@48153
|
295 |
case maybe_proven_rsp_thm of
|
kuncar@48375
|
296 |
SOME _ => Proof.theorem NONE after_qed [] lthy'
|
kuncar@48375
|
297 |
| NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy'
|
kuncar@48153
|
298 |
end
|
kuncar@48153
|
299 |
|
kuncar@48237
|
300 |
fun quot_thm_err ctxt (rty, qty) pretty_msg =
|
kuncar@48237
|
301 |
let
|
kuncar@48237
|
302 |
val error_msg = cat_lines
|
kuncar@48237
|
303 |
["Lifting failed for the following types:",
|
kuncar@48237
|
304 |
Pretty.string_of (Pretty.block
|
kuncar@48237
|
305 |
[Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
|
kuncar@48237
|
306 |
Pretty.string_of (Pretty.block
|
kuncar@48237
|
307 |
[Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
|
kuncar@48237
|
308 |
"",
|
kuncar@48237
|
309 |
(Pretty.string_of (Pretty.block
|
kuncar@48237
|
310 |
[Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
|
kuncar@48237
|
311 |
in
|
kuncar@48237
|
312 |
error error_msg
|
kuncar@48237
|
313 |
end
|
kuncar@48237
|
314 |
|
kuncar@48375
|
315 |
fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
|
kuncar@48237
|
316 |
let
|
kuncar@48375
|
317 |
val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
|
kuncar@48375
|
318 |
val rhs = (Syntax.check_term ctxt' o Syntax.parse_term ctxt') rhs_raw
|
kuncar@48237
|
319 |
val error_msg = cat_lines
|
kuncar@48237
|
320 |
["Lifting failed for the following term:",
|
kuncar@48237
|
321 |
Pretty.string_of (Pretty.block
|
kuncar@48237
|
322 |
[Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
|
kuncar@48237
|
323 |
Pretty.string_of (Pretty.block
|
kuncar@48375
|
324 |
[Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty_schematic]),
|
kuncar@48237
|
325 |
"",
|
kuncar@48237
|
326 |
(Pretty.string_of (Pretty.block
|
kuncar@48237
|
327 |
[Pretty.str "Reason:",
|
kuncar@48237
|
328 |
Pretty.brk 2,
|
kuncar@48237
|
329 |
Pretty.str "The type of the term cannot be instancied to",
|
kuncar@48237
|
330 |
Pretty.brk 1,
|
kuncar@48375
|
331 |
Pretty.quote (Syntax.pretty_typ ctxt rty_forced),
|
kuncar@48237
|
332 |
Pretty.str "."]))]
|
kuncar@48237
|
333 |
in
|
kuncar@48237
|
334 |
error error_msg
|
kuncar@48237
|
335 |
end
|
kuncar@48237
|
336 |
|
kuncar@48237
|
337 |
fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy =
|
kuncar@48237
|
338 |
(lift_def_cmd (raw_var, rhs_raw) lthy
|
kuncar@48237
|
339 |
handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
|
kuncar@48375
|
340 |
handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) =>
|
kuncar@48375
|
341 |
check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw)
|
kuncar@48237
|
342 |
|
kuncar@48153
|
343 |
(* parser and command *)
|
kuncar@48153
|
344 |
val liftdef_parser =
|
kuncar@48153
|
345 |
((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
|
kuncar@48153
|
346 |
--| @{keyword "is"} -- Parse.term
|
kuncar@48153
|
347 |
|
kuncar@48153
|
348 |
val _ =
|
kuncar@48153
|
349 |
Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
|
kuncar@48153
|
350 |
"definition for constants over the quotient type"
|
kuncar@48237
|
351 |
(liftdef_parser >> lift_def_cmd_with_err_handling)
|
kuncar@48153
|
352 |
|
kuncar@48153
|
353 |
|
kuncar@48153
|
354 |
end; (* structure *)
|