equal
deleted
inserted
replaced
619 (case dest_predicate cs params s of |
619 (case dest_predicate cs params s of |
620 SOME (_, i, ys, (_, Ts)) => |
620 SOME (_, i, ys, (_, Ts)) => |
621 let |
621 let |
622 val k = length Ts; |
622 val k = length Ts; |
623 val bs = map Bound (k - 1 downto 0); |
623 val bs = map Bound (k - 1 downto 0); |
624 val P = list_comb (List.nth (preds, i), |
624 val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); |
625 map (incr_boundvars k) ys @ bs); |
|
626 val Q = list_abs (mk_names "x" k ~~ Ts, |
625 val Q = list_abs (mk_names "x" k ~~ Ts, |
627 HOLogic.mk_binop inductive_conj_name |
626 HOLogic.mk_binop inductive_conj_name |
628 (list_comb (incr_boundvars k s, bs), P)) |
627 (list_comb (incr_boundvars k s, bs), P)) |
629 in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end |
628 in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end |
630 | NONE => |
629 | NONE => |
639 | (t, _) => t :: prems); |
638 | (t, _) => t :: prems); |
640 |
639 |
641 val SOME (_, i, ys, _) = dest_predicate cs params |
640 val SOME (_, i, ys, _) = dest_predicate cs params |
642 (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) |
641 (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) |
643 |
642 |
644 in list_all_free (Logic.strip_params r, |
643 in |
645 Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem |
644 list_all_free (Logic.strip_params r, |
646 (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), |
645 Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem |
647 HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys)))) |
646 (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), |
|
647 HOLogic.mk_Trueprop (list_comb (nth preds i, ys)))) |
648 end; |
648 end; |
649 |
649 |
650 val ind_prems = map mk_ind_prem intr_ts; |
650 val ind_prems = map mk_ind_prem intr_ts; |
651 |
651 |
652 |
652 |