700 Quotient_Def.get_fun repF lthy (T, T') |
698 Quotient_Def.get_fun repF lthy (T, T') |
701 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
699 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
702 *} |
700 *} |
703 |
701 |
704 ML {* |
702 ML {* |
|
703 fun strip_combn n u = |
|
704 let fun stripc 0 x = x |
|
705 | stripc n (f $ t, ts) = stripc (n - 1) (f, t::ts) |
|
706 | stripc _ x = x |
|
707 in stripc n (u, []) end |
|
708 *} |
|
709 |
|
710 |
|
711 ML {* |
705 (* bound variables need to be treated properly, *) |
712 (* bound variables need to be treated properly, *) |
706 (* as the type of subterms need to be calculated *) |
713 (* as the type of subterms need to be calculated *) |
707 |
714 |
708 fun inj_repabs_trm lthy (rtrm, qtrm) = |
715 fun inj_repabs_trm lthy (rtrm, qtrm) = |
709 let |
716 let |
711 val qty = fastype_of qtrm |
718 val qty = fastype_of qtrm |
712 in |
719 in |
713 case (rtrm, qtrm) of |
720 case (rtrm, qtrm) of |
714 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
721 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
715 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
722 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
723 |
716 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
724 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
717 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
725 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
718 | (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
726 |
|
727 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
719 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
728 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
729 |
720 | (Abs (x, T, t), Abs (x', T', t')) => |
730 | (Abs (x, T, t), Abs (x', T', t')) => |
721 let |
731 let |
722 val (y, s) = Term.dest_abs (x, T, t) |
732 val (y, s) = Term.dest_abs (x, T, t) |
723 val (_, s') = Term.dest_abs (x', T', t') |
733 val (_, s') = Term.dest_abs (x', T', t') |
724 val yvar = Free (y, T) |
734 val yvar = Free (y, T) |
728 then result |
738 then result |
729 else mk_repabs lthy (rty, qty) result |
739 else mk_repabs lthy (rty, qty) result |
730 end |
740 end |
731 | _ => |
741 | _ => |
732 let |
742 let |
733 val (rhead, rargs) = strip_comb rtrm |
|
734 val (qhead, qargs) = strip_comb qtrm |
743 val (qhead, qargs) = strip_comb qtrm |
|
744 val (rhead, rargs) = strip_combn (length qargs) rtrm |
735 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
745 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
736 in |
746 in |
737 case (rhead, qhead) of |
747 case (rhead, qhead) of |
738 (Const (s, T), Const (s', T')) => |
748 (Const (s, T), Const (s', T')) => |
739 if T = T' |
749 if T = T' |
743 if T = T' |
753 if T = T' |
744 then list_comb (rhead, rargs') |
754 then list_comb (rhead, rargs') |
745 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
755 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
746 | (Abs _, Abs _) => |
756 | (Abs _, Abs _) => |
747 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
757 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
748 | _ => raise (LIFT_MATCH "injection") |
758 |
|
759 (* FIXME: when there is an (op =), then lhs might have been a term *) |
|
760 | (_, Const (@{const_name "op ="}, T)) => |
|
761 list_comb (rhead, rargs') |
|
762 | _ => raise (LIFT_MATCH ("injection: rhead: " ^ (Syntax.string_of_term lthy rhead) |
|
763 ^ " qhead: " ^ (Syntax.string_of_term lthy qhead))) |
749 end |
764 end |
750 end |
765 end |
751 *} |
766 *} |
752 |
767 |
753 section {* RepAbs Injection Tactic *} |
768 section {* RepAbs Injection Tactic *} |
1218 val rtrm' = HOLogic.dest_Trueprop rtrm |
1233 val rtrm' = HOLogic.dest_Trueprop rtrm |
1219 val qtrm' = HOLogic.dest_Trueprop qtrm |
1234 val qtrm' = HOLogic.dest_Trueprop qtrm |
1220 val reg_goal = |
1235 val reg_goal = |
1221 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1236 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1222 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1237 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
1238 val _ = tracing "Regularization done." |
1223 val inj_goal = |
1239 val inj_goal = |
1224 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1240 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1225 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1241 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
1242 val _ = tracing "RepAbs Injection done." |
1226 in |
1243 in |
1227 Drule.instantiate' [] |
1244 Drule.instantiate' [] |
1228 [SOME (cterm_of thy rtrm'), |
1245 [SOME (cterm_of thy rtrm'), |
1229 SOME (cterm_of thy reg_goal), |
1246 SOME (cterm_of thy reg_goal), |
1230 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1247 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |