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