588 val goal = |
588 val goal = |
589 Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, |
589 Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, |
590 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
590 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
591 (map2 (curry (op $)) phis vs))); |
591 (map2 (curry (op $)) phis vs))); |
592 |
592 |
593 fun mk_raw_prem_prems_indices pprems = |
593 val kksss = map (map (map (fst o snd) o #2)) raw_premss; |
594 let |
|
595 fun has_index kk (_, (kk', _)) = kk' = kk; |
|
596 val buckets = Library.partition_list has_index 1 nn pprems; |
|
597 val pps = map length buckets; |
|
598 in |
|
599 map (fn pprem as (xysets, (kk, _)) => |
|
600 ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1), |
|
601 (length xysets, kk))) pprems |
|
602 end; |
|
603 |
|
604 val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss; |
|
605 val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*) |
|
606 |
594 |
607 val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); |
595 val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); |
608 |
596 |
609 val induct_thm = |
597 val induct_thm = |
610 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
598 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
611 mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct' |
599 mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct' |
612 nested_set_natural's pre_set_defss) |
600 nested_set_natural's pre_set_defss) |
613 |> singleton (Proof_Context.export names_lthy lthy) |
601 |> singleton (Proof_Context.export names_lthy lthy) |
614 in |
602 in |
615 `(conj_dests nn) induct_thm |
603 `(conj_dests nn) induct_thm |
616 end; |
604 end; |