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