421 let |
421 let |
422 val m = the_single ms; |
422 val m = the_single ms; |
423 val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); |
423 val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs); |
424 in |
424 in |
425 Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) |
425 Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm) |
|
426 |> Thm.close_derivation |
426 |> singleton (Proof_Context.export names_lthy lthy) |
427 |> singleton (Proof_Context.export names_lthy lthy) |
427 |> Thm.close_derivation |
|
428 end; |
428 end; |
429 |
429 |
430 fun mk_alternate_disc_def k = |
430 fun mk_alternate_disc_def k = |
431 let |
431 let |
432 val goal = |
432 val goal = |
434 nth exist_xs_u_eq_ctrs (k - 1)); |
434 nth exist_xs_u_eq_ctrs (k - 1)); |
435 in |
435 in |
436 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
436 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
437 mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) |
437 mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) |
438 (nth distinct_thms (2 - k)) uexhaust_thm) |
438 (nth distinct_thms (2 - k)) uexhaust_thm) |
|
439 |> Thm.close_derivation |
439 |> singleton (Proof_Context.export names_lthy lthy) |
440 |> singleton (Proof_Context.export names_lthy lthy) |
440 |> Thm.close_derivation |
|
441 end; |
441 end; |
442 |
442 |
443 val has_alternate_disc_def = |
443 val has_alternate_disc_def = |
444 exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs; |
444 exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs; |
445 |
445 |
549 in |
549 in |
550 [Skip_Proof.prove lthy [] [] goal (fn _ => |
550 [Skip_Proof.prove lthy [] [] goal (fn _ => |
551 mk_expand_tac n ms (inst_thm u disc_exhaust_thm) |
551 mk_expand_tac n ms (inst_thm u disc_exhaust_thm) |
552 (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss |
552 (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss |
553 disc_exclude_thmsss')] |
553 disc_exclude_thmsss')] |
|
554 |> map Thm.close_derivation |
554 |> Proof_Context.export names_lthy lthy |
555 |> Proof_Context.export names_lthy lthy |
555 |> map Thm.close_derivation |
|
556 end; |
556 end; |
557 |
557 |
558 val case_conv_thms = |
558 val case_conv_thms = |
559 let |
559 let |
560 fun mk_body f usels = Term.list_comb (f, usels); |
560 fun mk_body f usels = Term.list_comb (f, usels); |
561 val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss)); |
561 val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss)); |
562 in |
562 in |
563 [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
563 [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
564 mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] |
564 mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] |
|
565 |> map Thm.close_derivation |
565 |> Proof_Context.export names_lthy lthy |
566 |> Proof_Context.export names_lthy lthy |
566 |> map Thm.close_derivation |
|
567 end; |
567 end; |
568 in |
568 in |
569 (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, |
569 (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, |
570 [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms) |
570 [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms) |
571 end; |
571 end; |
581 mk_Trueprop_eq (ufcase, vgcase)); |
581 mk_Trueprop_eq (ufcase, vgcase)); |
582 val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); |
582 val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); |
583 in |
583 in |
584 (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms), |
584 (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms), |
585 Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1))) |
585 Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1))) |
586 |> pairself (singleton (Proof_Context.export names_lthy lthy) #> Thm.close_derivation) |
586 |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy)) |
587 end; |
587 end; |
588 |
588 |
589 val (split_thm, split_asm_thm) = |
589 val (split_thm, split_asm_thm) = |
590 let |
590 let |
591 fun mk_conjunct xctr xs f_xs = |
591 fun mk_conjunct xctr xs f_xs = |
603 (map3 mk_disjunct xctrs xss xfs))); |
603 (map3 mk_disjunct xctrs xss xfs))); |
604 |
604 |
605 val split_thm = |
605 val split_thm = |
606 Skip_Proof.prove lthy [] [] goal |
606 Skip_Proof.prove lthy [] [] goal |
607 (fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss) |
607 (fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss) |
608 |> singleton (Proof_Context.export names_lthy lthy) |
608 |> Thm.close_derivation |
609 |> Thm.close_derivation; |
609 |> singleton (Proof_Context.export names_lthy lthy); |
610 val split_asm_thm = |
610 val split_asm_thm = |
611 Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} => |
611 Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} => |
612 mk_split_asm_tac ctxt split_thm) |
612 mk_split_asm_tac ctxt split_thm) |
613 |> singleton (Proof_Context.export names_lthy lthy) |
613 |> Thm.close_derivation |
614 |> Thm.close_derivation; |
614 |> singleton (Proof_Context.export names_lthy lthy); |
615 in |
615 in |
616 (split_thm, split_asm_thm) |
616 (split_thm, split_asm_thm) |
617 end; |
617 end; |
618 |
618 |
619 val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); |
619 val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); |