79 |
79 |
80 fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; |
80 fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; |
81 val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; |
81 val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; |
82 val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); |
82 val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); |
83 |
83 |
84 val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result |
84 val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result |
85 (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy |
85 (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy; |
86 ||> `Local_Theory.reset; |
|
87 |
86 |
88 fun mk_wit_thms set_maps = |
87 fun mk_wit_thms set_maps = |
89 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) |
88 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) |
90 (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) |
89 (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) |
91 |> Thm.close_derivation |
90 |> Thm.close_derivation |
92 |> Conjunction.elim_balanced (length wit_goals) |
91 |> Conjunction.elim_balanced (length wit_goals) |
93 |> map2 (Conjunction.elim_balanced o length) wit_goalss |
92 |> map2 (Conjunction.elim_balanced o length) wit_goalss |
94 |> (map o map) (Thm.forall_elim_vars 0); |
93 |> (map o map) (Thm.forall_elim_vars 0); |
95 val phi = Proof_Context.export_morphism lthy_old lthy; |
94 val phi = Local_Theory.target_morphism lthy; |
96 val thms = unflat all_goalss (Morphism.fact phi raw_thms); |
95 val thms = unflat all_goalss (Morphism.fact phi raw_thms); |
97 |
96 |
98 val (bnf, lthy') = after_qed mk_wit_thms thms lthy |
97 val (bnf, lthy') = after_qed mk_wit_thms thms lthy |
99 in |
98 in |
100 (bnf, register_bnf plugins key bnf lthy') |
99 (bnf, register_bnf plugins key bnf lthy') |