357 (* the major type of All and Ex quantifiers *) |
357 (* the major type of All and Ex quantifiers *) |
358 fun qnt_typ ty = domain_type (domain_type ty) |
358 fun qnt_typ ty = domain_type (domain_type ty) |
359 *} |
359 *} |
360 |
360 |
361 ML {* |
361 ML {* |
362 (* produces a regularized version of rtm *) |
362 (* produces a regularized version of rtrm *) |
363 (* - the result is still not completely typed *) |
363 (* - the result is contains dummyT *) |
364 (* - does not need any special treatment of *) |
364 (* - does not need any special treatment of *) |
365 (* bound variables *) |
365 (* bound variables *) |
366 |
366 |
367 fun regularize_trm lthy rtrm qtrm = |
367 fun regularize_trm lthy rtrm qtrm = |
368 case (rtrm, qtrm) of |
368 case (rtrm, qtrm) of |
369 (Abs (x, ty, t), Abs (x', ty', t')) => |
369 (Abs (x, ty, t), Abs (x', ty', t')) => |
370 let |
370 let |
371 val subtrm = Abs(x, ty, regularize_trm lthy t t') |
371 val subtrm = Abs(x, ty, regularize_trm lthy t t') |
372 in |
372 in |
373 if ty = ty' |
373 if ty = ty' then subtrm |
374 then subtrm |
|
375 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
374 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
376 end |
375 end |
377 |
376 |
378 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
377 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
379 let |
378 let |
393 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
392 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
394 end |
393 end |
395 |
394 |
396 | (* equalities need to be replaced by appropriate equivalence relations *) |
395 | (* equalities need to be replaced by appropriate equivalence relations *) |
397 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
396 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
398 if ty = ty' |
397 if ty = ty' then rtrm |
399 then rtrm |
|
400 else mk_resp_arg lthy (domain_type ty, domain_type ty') |
398 else mk_resp_arg lthy (domain_type ty, domain_type ty') |
401 |
399 |
402 | (* in this case we check whether the given equivalence relation is correct *) |
400 | (* in this case we check whether the given equivalence relation is correct *) |
403 (rel, Const (@{const_name "op ="}, ty')) => |
401 (rel, Const (@{const_name "op ="}, ty')) => |
404 let |
402 let |
405 val exc = LIFT_MATCH "regularise (relation mismatch)" |
403 val exc = LIFT_MATCH "regularise (relation mismatch)" |
406 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
404 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
407 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
405 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
408 in |
406 in |
409 if rel' = rel |
407 if rel' = rel |
410 then rtrm |
408 then rtrm else raise exc |
411 else raise exc |
|
412 end |
409 end |
413 | (_, Const (s, _)) => |
410 | (_, Const (s, _)) => |
414 let |
411 let |
415 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
412 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
416 | same_name _ _ = false |
413 | same_name _ _ = false |
436 | (Free (x, ty), Free (x', ty')) => |
433 | (Free (x, ty), Free (x', ty')) => |
437 (* this case cannot arrise as we start with two fully atomized terms *) |
434 (* this case cannot arrise as we start with two fully atomized terms *) |
438 raise (LIFT_MATCH "regularize (frees)") |
435 raise (LIFT_MATCH "regularize (frees)") |
439 |
436 |
440 | (Bound i, Bound i') => |
437 | (Bound i, Bound i') => |
441 if i = i' |
438 if i = i' then rtrm |
442 then rtrm |
|
443 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
439 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
444 |
440 |
445 | (rt, qt) => |
441 | (rt, qt) => |
446 raise (LIFT_MATCH "regularize (default)") |
442 raise (LIFT_MATCH "regularize failed (default)") |
447 *} |
443 *} |
448 |
444 |
449 section {* Regularize Tactic *} |
445 section {* Regularize Tactic *} |
450 |
446 |
451 ML {* |
447 ML {* |
1187 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1183 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1188 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1184 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1189 (clean_tac ctxt, "Cleaning proof failed.")] |
1185 (clean_tac ctxt, "Cleaning proof failed.")] |
1190 *} |
1186 *} |
1191 |
1187 |
|
1188 ML {* |
|
1189 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm |
|
1190 |
|
1191 (* FIXME: if the argument order changes then this can be just one function *) |
|
1192 fun mk_method1 tac thm ctxt = |
|
1193 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
|
1194 |
|
1195 fun mk_method2 tac ctxt = |
|
1196 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
|
1197 *} |
|
1198 |
|
1199 method_setup lifting = |
|
1200 {* rule_spec >> (mk_method1 lift_tac) *} |
|
1201 {* Lifting of theorems to quotient types. *} |
|
1202 |
|
1203 method_setup lifting_setup = |
|
1204 {* rule_spec >> (mk_method1 procedure_tac) *} |
|
1205 {* Sets up the three goals for the lifting procedure. *} |
|
1206 |
|
1207 method_setup regularize = |
|
1208 {* Scan.succeed (mk_method2 regularize_tac) *} |
|
1209 {* Proves automatically the regularization goals from the lifting procedure. *} |
|
1210 |
|
1211 method_setup injection = |
|
1212 {* Scan.succeed (mk_method2 all_inj_repabs_tac) *} |
|
1213 {* Proves automatically the rep/abs injection goals from the lifting procedure. *} |
|
1214 |
|
1215 method_setup cleaning = |
|
1216 {* Scan.succeed (mk_method2 clean_tac) *} |
|
1217 {* Proves automatically the cleaning goals from the lifting procedure. *} |
|
1218 |
1192 end |
1219 end |
1193 |
1220 |