510 val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] |
510 val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] |
511 (Const (\<^const_name>\<open>The\<close>, (B --> HOLogic.boolT) --> B) $ |
511 (Const (\<^const_name>\<open>The\<close>, (B --> HOLogic.boolT) --> B) $ |
512 Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss))); |
512 Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss))); |
513 |
513 |
514 val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy |
514 val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy |
515 |> Local_Theory.open_target |
515 |> (snd o Local_Theory.begin_nested) |
516 |> Local_Theory.define ((case_binding, NoSyn), |
516 |> Local_Theory.define ((case_binding, NoSyn), |
517 ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs)) |
517 ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs)) |
518 ||> `Local_Theory.close_target; |
518 ||> `Local_Theory.end_nested; |
519 |
519 |
520 val phi = Proof_Context.export_morphism lthy_old lthy; |
520 val phi = Proof_Context.export_morphism lthy_old lthy; |
521 |
521 |
522 val case_def = Morphism.thm phi raw_case_def; |
522 val case_def = Morphism.thm phi raw_case_def; |
523 |
523 |
617 |
617 |
618 fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; |
618 fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; |
619 |
619 |
620 val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = |
620 val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = |
621 lthy |
621 lthy |
622 |> Local_Theory.open_target |
622 |> (snd o Local_Theory.begin_nested) |
623 |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b => |
623 |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b => |
624 if Binding.is_empty b then |
624 if Binding.is_empty b then |
625 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) |
625 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) |
626 else pair (alternate_disc k, alternate_disc_no_def) |
626 else pair (alternate_disc k, alternate_disc_no_def) |
627 else if Binding.eq_name (b, equal_binding) then |
627 else if Binding.eq_name (b, equal_binding) then |
631 ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd) |
631 ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd) |
632 ks exist_xs_u_eq_ctrs disc_bindings |
632 ks exist_xs_u_eq_ctrs disc_bindings |
633 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
633 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
634 Specification.definition (SOME (b, NONE, NoSyn)) [] [] |
634 Specification.definition (SOME (b, NONE, NoSyn)) [] [] |
635 ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos |
635 ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos |
636 ||> `Local_Theory.close_target; |
636 ||> `Local_Theory.end_nested; |
637 |
637 |
638 val phi = Proof_Context.export_morphism lthy lthy'; |
638 val phi = Proof_Context.export_morphism lthy lthy'; |
639 |
639 |
640 val disc_defs = map (Morphism.thm phi) raw_disc_defs; |
640 val disc_defs = map (Morphism.thm phi) raw_disc_defs; |
641 val sel_defs = map (Morphism.thm phi) raw_sel_defs; |
641 val sel_defs = map (Morphism.thm phi) raw_sel_defs; |