# HG changeset patch # User wenzelm # Date 1441395659 -7200 # Node ID 6189d179c2b515fe90a81b908868797019089732 # Parent 3a44009857801a5a7e907170cdbe24176252be9f close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance; diff -r 3a4400985780 -r 6189d179c2b5 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 04 19:22:13 2015 +0200 +++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 04 21:40:59 2015 +0200 @@ -86,9 +86,10 @@ fun mk_wit_thms set_maps = Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) + |> Thm.close_derivation |> Conjunction.elim_balanced (length wit_goals) |> map2 (Conjunction.elim_balanced o length) wit_goalss - |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + |> (map o map) (Thm.forall_elim_vars 0); val phi = Proof_Context.export_morphism lthy_old lthy; val thms = unflat all_goalss (Morphism.fact phi raw_thms); diff -r 3a4400985780 -r 6189d179c2b5 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 04 19:22:13 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 04 21:40:59 2015 +0200 @@ -1484,9 +1484,9 @@ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map)) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; val set_transfer = Lazy.lazy mk_set_transfer; @@ -1566,9 +1566,10 @@ fun mk_wit_thms set_maps = Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) + |> Thm.close_derivation |> Conjunction.elim_balanced (length wit_goals) |> map2 (Conjunction.elim_balanced o length) wit_goalss - |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + |> (map o map) (Thm.forall_elim_vars 0); in map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] []) goals (map (fn tac => fn {context = ctxt, prems = _} => @@ -1585,9 +1586,10 @@ fun mk_triv_wit_thms tac set_maps = Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps) + |> Thm.close_derivation |> Conjunction.elim_balanced (length wit_goals) |> map2 (Conjunction.elim_balanced o length) wit_goalss - |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + |> (map o map) (Thm.forall_elim_vars 0); val (mk_wit_thms, nontriv_wit_goals) = (case triv_tac_opt of NONE => (fn _ => [], map (map (rpair [])) wit_goalss) diff -r 3a4400985780 -r 6189d179c2b5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 04 19:22:13 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 04 21:40:59 2015 +0200 @@ -680,9 +680,9 @@ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; val (set_cases_thms, set_cases_attrss) = @@ -785,9 +785,9 @@ else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation) + |> Proof_Context.export names_lthy lthy) end; val rel_sel_thms = @@ -884,9 +884,9 @@ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; val disc_transfer_thms = @@ -897,9 +897,9 @@ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt (the_single rel_sel_thms) (the_single exhaust_discs) (flat (flat distinct_discsss))) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; val map_disc_iff_thms = @@ -921,9 +921,9 @@ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; val (map_sel_thmss, map_sel_thms) = @@ -956,9 +956,9 @@ (fn {context = ctxt, prems = _} => mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms (flat sel_thmss) live_nesting_map_id0s) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation) + |> Proof_Context.export names_lthy lthy) end; val (set_sel_thmssss, set_sel_thms) = @@ -1015,9 +1015,9 @@ (fn {context = ctxt, prems = _} => mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) (flat sel_thmss) set0_thms) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation) + |> Proof_Context.export names_lthy lthy) end; val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; @@ -2256,9 +2256,9 @@ (fn {context = ctxt, prems = _} => mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs) + |> Thm.close_derivation |> Conjunction.elim_balanced nn |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; fun derive_rec_o_map_thmss lthy recs rec_defs = @@ -2408,9 +2408,9 @@ mk_corec_transfer_tac ctxt (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs (flat pgss) pss qssss gssss) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs = diff -r 3a4400985780 -r 6189d179c2b5 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 04 19:22:13 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 04 21:40:59 2015 +0200 @@ -1017,9 +1017,9 @@ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Thm.cterm_of ctxt u) exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms) + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation end; in (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, diff -r 3a4400985780 -r 6189d179c2b5 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Sep 04 19:22:13 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Sep 04 21:40:59 2015 +0200 @@ -76,6 +76,7 @@ fun proves goals = goals |> Logic.mk_conjunction_balanced |> prove + |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) |> map Simpdata.mk_eq; in