701 Quotient_Def.get_fun repF lthy (T, T') |
701 Quotient_Def.get_fun repF lthy (T, T') |
702 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
702 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
703 *} |
703 *} |
704 |
704 |
705 ML {* |
705 ML {* |
706 fun strip_combn n u = |
706 (* bound variables need to be treated properly, *) |
707 let fun stripc 0 x = x |
707 (* as the type of subterms need to be calculated *) |
708 | stripc n (f $ t, ts) = stripc (n - 1) (f, t::ts) |
708 (* in the abstraction case *) |
709 | stripc _ x = x |
|
710 in stripc n (u, []) end |
|
711 *} |
|
712 |
|
713 |
|
714 ML {* |
|
715 (* bound variables need to be treated properly, *) |
|
716 (* as the type of subterms need to be calculated *) |
|
717 |
709 |
718 fun inj_repabs_trm lthy (rtrm, qtrm) = |
710 fun inj_repabs_trm lthy (rtrm, qtrm) = |
719 let |
711 case (rtrm, qtrm) of |
720 val rty = fastype_of rtrm |
|
721 val qty = fastype_of qtrm |
|
722 in |
|
723 case (rtrm, qtrm) of |
|
724 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
712 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
725 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
713 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
726 |
714 |
727 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
715 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
728 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
716 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
730 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
718 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
731 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
719 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
732 |
720 |
733 | (Abs (x, T, t), Abs (x', T', t')) => |
721 | (Abs (x, T, t), Abs (x', T', t')) => |
734 let |
722 let |
|
723 val rty = fastype_of rtrm |
|
724 val qty = fastype_of qtrm |
735 val (y, s) = Term.dest_abs (x, T, t) |
725 val (y, s) = Term.dest_abs (x, T, t) |
736 val (_, s') = Term.dest_abs (x', T', t') |
726 val (_, s') = Term.dest_abs (x', T', t') |
737 val yvar = Free (y, T) |
727 val yvar = Free (y, T) |
738 val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) |
728 val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) |
739 in |
729 in |
743 end |
733 end |
744 |
734 |
745 | (t $ s, t' $ s') => |
735 | (t $ s, t' $ s') => |
746 (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) |
736 (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) |
747 |
737 |
748 | (Free (x, T), Free (x', T')) => |
738 | (Free (_, T), Free (_, T')) => |
749 if T = T' |
739 if T = T' |
750 then rtrm |
740 then rtrm |
751 else mk_repabs lthy (T, T') rtrm |
741 else mk_repabs lthy (T, T') rtrm |
752 |
742 |
753 | (Const (s, T), Const (s', T')) => |
743 | (Const (_, T), Const (_, T')) => |
754 if T = T' |
744 if T = T' |
755 then rtrm |
745 then rtrm |
756 else mk_repabs lthy (T, T') rtrm |
746 else mk_repabs lthy (T, T') rtrm |
757 |
747 |
758 | (_, Const (@{const_name "op ="}, _)) => rtrm |
748 | (_, Const (@{const_name "op ="}, _)) => rtrm |
759 |
749 |
760 | _ => raise (LIFT_MATCH "injection") |
750 | _ => raise (LIFT_MATCH "injection") |
761 end |
|
762 *} |
751 *} |
763 |
752 |
764 section {* RepAbs Injection Tactic *} |
753 section {* RepAbs Injection Tactic *} |
765 |
754 |
766 (* Not used anymore *) |
755 (* Not used anymore *) |