take intersection rather than union of methods when merging steps -- more efficient and natural
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 552474aa3e1c6222c
parent 55246 e9fba9767d92
child 55248 235205726737
take intersection rather than union of methods when merging steps -- more efficient and natural
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -81,13 +81,15 @@
     1.4  
     1.5  fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1)))
     1.6        (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) =
     1.7 -    let
     1.8 -      val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
     1.9 -      val gfs = union (op =) gfs1 gfs2
    1.10 -      val meths = fold_rev (insert (op =)) meths1 meths2
    1.11 -    in
    1.12 -      SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
    1.13 -    end
    1.14 +    (case inter (op =) meths1 meths2 of
    1.15 +      [] => NONE
    1.16 +    | meths =>
    1.17 +      let
    1.18 +        val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
    1.19 +        val gfs = union (op =) gfs1 gfs2
    1.20 +      in
    1.21 +        SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
    1.22 +      end)
    1.23    | try_merge _ _ = NONE
    1.24  
    1.25  val compress_degree = 2
    1.26 @@ -237,7 +239,7 @@
    1.27                val play_outcomes = map2 preplay_quietly timeouts succs'
    1.28  
    1.29                (* ensure none of the modified successors timed out *)
    1.30 -              val true = List.all (fn Played _ => true) play_outcomes
    1.31 +              val true = forall (fn Played _ => true) play_outcomes
    1.32  
    1.33                val (steps1, _ :: steps2) = chop i steps
    1.34                (* replace successors with their modified versions *)