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