call Goal.prove only once for a quadratic number of theorems
authortraytel
Mon Apr 13 13:03:41 2015 +0200 (2015-04-13)
changeset 60046894d6d863823
parent 60045 cd2b6debac18
child 60056 71c1b9b9e937
child 60057 86fa63ce8156
call Goal.prove only once for a quadratic number of theorems
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Apr 13 12:15:29 2015 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Apr 13 13:03:41 2015 +0200
     1.3 @@ -68,12 +68,18 @@
     1.4  
     1.5      fun prove goal =
     1.6        Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
     1.7 +        HEADGOAL Goal.conjunction_tac THEN
     1.8          ALLGOALS (simp_tac
     1.9            (put_simpset HOL_basic_ss ctxt
    1.10 -            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))))
    1.11 -      |> Simpdata.mk_eq;
    1.12 +            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))));
    1.13 +
    1.14 +    fun proves goals = goals
    1.15 +      |> Logic.mk_conjunction_balanced
    1.16 +      |> prove
    1.17 +      |> Conjunction.elim_balanced (length goals)
    1.18 +      |> map Simpdata.mk_eq;
    1.19    in
    1.20 -    (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
    1.21 +    (proves (triv_inject_goals @ inject_goals @ distinct_goals), Simpdata.mk_eq (prove refl_goal))
    1.22    end;
    1.23  
    1.24  fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =