339 fun dest_term (a $ b) = (a, b); |
339 fun dest_term (a $ b) = (a, b); |
340 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; |
341 in |
341 in |
342 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 |
343 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") |
|
402 *} |
344 *} |
403 |
345 |
404 section {* Regularization *} |
346 section {* Regularization *} |
405 |
347 |
406 (* |
348 (* |
792 if rty = qty |
734 if rty = qty |
793 then result |
735 then result |
794 else mk_repabs lthy (rty, qty) result |
736 else mk_repabs lthy (rty, qty) result |
795 end |
737 end |
796 | _ => |
738 | _ => |
797 (* FIXME / TODO: this is a case that needs to be looked at *) |
739 (**************************************************) |
798 (* - variables get a rep-abs insde and outside an application *) |
740 (* new |
799 (* - constants only get a rep-abs on the outside of the application *) |
741 let |
800 (* - applications get a rep-abs insde and outside an application *) |
742 val (rhead, rargs) = strip_comb rtrm |
|
743 val (qhead, qargs) = strip_comb qtrm |
|
744 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
|
745 in |
|
746 case (rhead, qhead, length rargs') of |
|
747 (Const (_, T), Const (_, T'), 0) => |
|
748 if T = T' |
|
749 then rhead |
|
750 else mk_repabs lthy (T, T') rhead |
|
751 | (Free (_, T), Free (_, T'), 0) => |
|
752 if T = T' |
|
753 then rhead |
|
754 else mk_repabs lthy (T, T') rhead |
|
755 | (Const (_, T), Const (_, T'), _) => (* FIXME/TODO: check this case exactly*) |
|
756 if rty = qty |
|
757 then list_comb (rhead, rargs') |
|
758 else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
|
759 | (Free (x, T), Free (x', T'), _) => |
|
760 if T = T' |
|
761 then list_comb (rhead, rargs') |
|
762 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
|
763 | (Abs _, Abs _, _ ) => |
|
764 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
|
765 | _ => raise (LIFT_MATCH "injection") |
|
766 end |
|
767 *) |
|
768 |
|
769 (*************************************************) |
|
770 (* old *) |
801 let |
771 let |
802 val (rhead, rargs) = strip_comb rtrm |
772 val (rhead, rargs) = strip_comb rtrm |
803 val (qhead, qargs) = strip_comb qtrm |
773 val (qhead, qargs) = strip_comb qtrm |
804 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
774 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
805 in |
775 in |
819 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
789 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
820 | (Abs _, Abs _, _ ) => |
790 | (Abs _, Abs _, _ ) => |
821 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
791 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
822 | _ => raise (LIFT_MATCH "injection") |
792 | _ => raise (LIFT_MATCH "injection") |
823 end |
793 end |
|
794 (**) |
824 end |
795 end |
825 *} |
796 *} |
826 |
797 |
827 section {* RepAbs Injection Tactic *} |
798 section {* RepAbs Injection Tactic *} |
828 |
799 |