343 fun dest_term (a $ b) = (a, b); |
339 fun dest_term (a $ b) = (a, b); |
344 val def_terms = map (snd o Logic.dest_equals o concl_of) defs; |
340 val def_terms = map (snd o Logic.dest_equals o concl_of) defs; |
345 in |
341 in |
346 map (fst o dest_Const o snd o dest_term) def_terms |
342 map (fst o dest_Const o snd o dest_term) def_terms |
347 end |
343 end |
|
344 *} |
|
345 |
|
346 section {* Infrastructure for special quotient identity *} |
|
347 |
|
348 definition |
|
349 "qid TYPE('a) TYPE('b) x \<equiv> x" |
|
350 |
|
351 ML {* |
|
352 fun get_typ1 (Type ("itself", [T])) = T |
|
353 fun get_typ2 (Const ("TYPE", T)) = get_typ1 T |
|
354 fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) = |
|
355 (get_typ2 ty1, get_typ2 ty2) |
|
356 |
|
357 fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true |
|
358 | is_qid _ = false |
|
359 |
|
360 |
|
361 fun mk_itself ty = Type ("itself", [ty]) |
|
362 fun mk_TYPE ty = Const ("TYPE", mk_itself ty) |
|
363 fun mk_qid (rty, qty, trm) = |
|
364 Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) |
|
365 $ mk_TYPE rty $ mk_TYPE qty $ trm |
|
366 *} |
|
367 |
|
368 ML {* |
|
369 fun insertion_aux rtrm qtrm = |
|
370 case (rtrm, qtrm) of |
|
371 (Abs (x, ty, t), Abs (x', ty', t')) => |
|
372 let |
|
373 val (y, s) = Term.dest_abs (x, ty, t) |
|
374 val (_, s') = Term.dest_abs (x', ty', t') |
|
375 val yvar = Free (y, ty) |
|
376 val result = Term.lambda_name (y, yvar) (insertion_aux s s') |
|
377 in |
|
378 if ty = ty' |
|
379 then result |
|
380 else mk_qid (ty, ty', result) |
|
381 end |
|
382 | (t1 $ t2, t1' $ t2') => |
|
383 let |
|
384 val rty = fastype_of rtrm |
|
385 val qty = fastype_of qtrm |
|
386 val subtrm1 = insertion_aux t1 t1' |
|
387 val subtrm2 = insertion_aux t2 t2' |
|
388 in |
|
389 if rty = qty |
|
390 then subtrm1 $ subtrm2 |
|
391 else mk_qid (rty, qty, subtrm1 $ subtrm2) |
|
392 end |
|
393 | (Free (_, ty), Free (_, ty')) => |
|
394 if ty = ty' |
|
395 then rtrm |
|
396 else mk_qid (ty, ty', rtrm) |
|
397 | (Const (s, ty), Const (s', ty')) => |
|
398 if s = s' andalso ty = ty' |
|
399 then rtrm |
|
400 else mk_qid (ty, ty', rtrm) |
|
401 | (_, _) => raise (LIFT_MATCH "insertion") |
348 *} |
402 *} |
349 |
403 |
350 section {* Regularization *} |
404 section {* Regularization *} |
351 |
405 |
352 (* |
406 (* |
468 then Const (@{const_name "op ="}, ty) $ subtrm |
522 then Const (@{const_name "op ="}, ty) $ subtrm |
469 else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm |
523 else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm |
470 end |
524 end |
471 | (t1 $ t2, t1' $ t2') => |
525 | (t1 $ t2, t1' $ t2') => |
472 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
526 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
473 | (Free (x, ty), Free (x', ty')) => |
527 | (Free (x, ty), Free (x', ty')) => |
474 if x = x' |
528 (* this case cannot arrise as we start with two fully atomized terms *) |
475 then rtrm (* FIXME: check whether types corresponds *) |
529 raise (LIFT_MATCH "regularize (frees)") |
476 else raise (LIFT_MATCH "regularize (frees)") |
|
477 | (Bound i, Bound i') => |
530 | (Bound i, Bound i') => |
478 if i = i' |
531 if i = i' |
479 then rtrm |
532 then rtrm |
480 else raise (LIFT_MATCH "regularize (bounds)") |
533 else raise (LIFT_MATCH "regularize (bounds)") |
481 | (Const (s, ty), Const (s', ty')) => |
534 | (Const (s, ty), Const (s', ty')) => |
732 | (Abs (x, T, t), Abs (x', T', t')) => |
785 | (Abs (x, T, t), Abs (x', T', t')) => |
733 let |
786 let |
734 val (y, s) = Term.dest_abs (x, T, t) |
787 val (y, s) = Term.dest_abs (x, T, t) |
735 val (_, s') = Term.dest_abs (x', T', t') |
788 val (_, s') = Term.dest_abs (x', T', t') |
736 val yvar = Free (y, T) |
789 val yvar = Free (y, T) |
737 val result = lambda yvar (inj_repabs_trm lthy (s, s')) |
790 val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) |
738 in |
791 in |
739 if rty = qty |
792 if rty = qty |
740 then result |
793 then result |
741 else mk_repabs lthy (rty, qty) result |
794 else mk_repabs lthy (rty, qty) result |
742 end |
795 end |