Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
authorwenzelm
Fri, 04 Sep 2015 21:40:59 +0200
changeset 61116 6189d179c2b5
parent 61115 3a4400985780
child 61117 4b5872b9d783
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
src/HOL/Library/bnf_axiomatization.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/BNF/bnf_def.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML file | annotate | diff | comparison | revisions 
--- 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);
 
--- 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)
--- 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 =
--- 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,
--- 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
isabelle