put shrink in own structure
authorsmolkas
Wed Nov 28 12:22:17 2012 +0100 (2012-11-28)
changeset 502599c64a52ae499
parent 50258 1c708d7728c7
child 50260 87ddf7eddfc9
put shrink in own structure
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Wed Nov 28 12:22:05 2012 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Nov 28 12:22:17 2012 +0100
     1.3 @@ -14,7 +14,9 @@
     1.4  ML_file "Tools/Sledgehammer/async_manager.ML"
     1.5  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
     1.6  ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
     1.7 +ML_file "Tools/Sledgehammer/sledgehammer_isar_reconstruct.ML"
     1.8  ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
     1.9 +ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
    1.10  ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" 
    1.11  ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
    1.12  ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed Nov 28 12:22:05 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Wed Nov 28 12:22:17 2012 +0100
     2.3 @@ -28,7 +28,6 @@
     2.4  
     2.5  (* Data structures, orders *)
     2.6  val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
     2.7 -
     2.8  structure Var_Set_Tab = Table(
     2.9    type key = indexname list
    2.10    val ord = list_ord Term_Ord.fast_indexname_ord)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML	Wed Nov 28 12:22:17 2012 +0100
     3.3 @@ -0,0 +1,46 @@
     3.4 +signature SLEDGEHAMMER_ISAR =
     3.5 +sig
     3.6 +	val annotate_types : Proof.context -> term -> term
     3.7 +end
     3.8 +
     3.9 +structure Sledgehammer_Isar_Reconstruct (* : SLEDGEHAMMER_Isar *) =
    3.10 +struct
    3.11 +
    3.12 +type label = string * int
    3.13 +type facts = label list * string list
    3.14 +
    3.15 +datatype isar_qualifier = Show | Then | Moreover | Ultimately
    3.16 +
    3.17 +datatype isar_step =
    3.18 +  Fix of (string * typ) list |
    3.19 +  Let of term * term |
    3.20 +  Assume of label * term |
    3.21 +  Prove of isar_qualifier list * label * term * byline
    3.22 +and byline =
    3.23 +  By_Metis of facts |
    3.24 +  Case_Split of isar_step list list * facts
    3.25 +
    3.26 +fun string_for_label (s, num) = s ^ string_of_int num
    3.27 +
    3.28 +fun thms_of_name ctxt name =
    3.29 +  let
    3.30 +    val lex = Keyword.get_lexicons
    3.31 +    val get = maps (Proof_Context.get_fact ctxt o fst)
    3.32 +  in
    3.33 +    Source.of_string name
    3.34 +    |> Symbol.source
    3.35 +    |> Token.source {do_recover = SOME false} lex Position.start
    3.36 +    |> Token.source_proper
    3.37 +    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    3.38 +    |> Source.exhaust
    3.39 +  end
    3.40 +
    3.41 +val inc = curry op+
    3.42 +fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
    3.43 +fun metis_steps_recursive proof = 
    3.44 +  fold (fn Prove (_,_,_, By_Metis _) => inc 1
    3.45 +         | Prove (_,_,_, Case_Split (cases, _)) => 
    3.46 +           inc (fold (inc o metis_steps_recursive) cases 1)
    3.47 +         | _ => I) proof 0
    3.48 +
    3.49 +end
    3.50 \ No newline at end of file
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:22:05 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:22:17 2012 +0100
     4.3 @@ -53,7 +53,9 @@
     4.4  open ATP_Problem_Generate
     4.5  open ATP_Proof_Reconstruct
     4.6  open Sledgehammer_Util
     4.7 +open Sledgehammer_Isar_Reconstruct
     4.8  open Sledgehammer_Annotate
     4.9 +open Sledgehammer_Shrink
    4.10  
    4.11  structure String_Redirect = ATP_Proof_Redirect(
    4.12    type key = step_name
    4.13 @@ -281,20 +283,6 @@
    4.14  
    4.15  (** Isar proof construction and manipulation **)
    4.16  
    4.17 -type label = string * int
    4.18 -type facts = label list * string list
    4.19 -
    4.20 -datatype isar_qualifier = Show | Then | Moreover | Ultimately
    4.21 -
    4.22 -datatype isar_step =
    4.23 -  Fix of (string * typ) list |
    4.24 -  Let of term * term |
    4.25 -  Assume of label * term |
    4.26 -  Prove of isar_qualifier list * label * term * byline
    4.27 -and byline =
    4.28 -  By_Metis of facts |
    4.29 -  Case_Split of isar_step list list * facts
    4.30 -
    4.31  val assume_prefix = "a"
    4.32  val have_prefix = "f"
    4.33  val raw_prefix = "x"
    4.34 @@ -598,179 +586,6 @@
    4.35          step :: aux subst depth nextp proof
    4.36    in aux [] 0 (1, 1) end
    4.37  
    4.38 -val merge_timeout_slack = 1.2
    4.39 -
    4.40 -val label_ord = prod_ord int_ord fast_string_ord o pairself swap
    4.41 -
    4.42 -structure Label_Table = Table(
    4.43 -  type key = label
    4.44 -  val ord = label_ord)
    4.45 -
    4.46 -fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
    4.47 -                 isar_shrink proof =
    4.48 -  let
    4.49 -    (* clean vector interface *)
    4.50 -    fun get i v = Vector.sub (v, i)
    4.51 -    fun replace x i v = Vector.update (v, i, x)
    4.52 -    fun update f i v = replace (get i v |> f) i v
    4.53 -    fun v_fold_index f v s =
    4.54 -      Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
    4.55 -
    4.56 -    (* Queue interface to table *)
    4.57 -    fun pop tab key =
    4.58 -      let val v = hd (Inttab.lookup_list tab key) in
    4.59 -        (v, Inttab.remove_list (op =) (key, v) tab)
    4.60 -      end
    4.61 -    fun pop_max tab = pop tab (the (Inttab.max_key tab))
    4.62 -    val is_empty = Inttab.is_empty
    4.63 -    fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
    4.64 -
    4.65 -    (* proof vector *)
    4.66 -    val proof_vect = proof |> map SOME |> Vector.fromList
    4.67 -    val n = Vector.length proof_vect
    4.68 -    val n_target = Real.fromInt n / isar_shrink |> Real.round
    4.69 -
    4.70 -    (* table for mapping from label to proof position *)
    4.71 -    fun update_table (i, Assume (label, _)) = 
    4.72 -        Label_Table.update_new (label, i)
    4.73 -      | update_table (i, Prove (_, label, _, _)) =
    4.74 -        Label_Table.update_new (label, i)
    4.75 -      | update_table _ = I
    4.76 -    val label_index_table = fold_index update_table proof Label_Table.empty
    4.77 -
    4.78 -    (* proof references *)
    4.79 -    fun refs (Prove (_, _, _, By_Metis (refs, _))) =
    4.80 -        map (the o Label_Table.lookup label_index_table) refs
    4.81 -      | refs _ = []
    4.82 -    val refed_by_vect =
    4.83 -      Vector.tabulate (n, (fn _ => []))
    4.84 -      |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
    4.85 -      |> Vector.map rev (* after rev, indices are sorted in ascending order *)
    4.86 -
    4.87 -    (* candidates for elimination, use table as priority queue (greedy
    4.88 -       algorithm) *)
    4.89 -    fun add_if_cand proof_vect (i, [j]) =
    4.90 -        (case (the (get i proof_vect), the (get j proof_vect)) of
    4.91 -          (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
    4.92 -            cons (Term.size_of_term t, i)
    4.93 -        | _ => I)
    4.94 -      | add_if_cand _ _ = I
    4.95 -    val cand_tab = 
    4.96 -      v_fold_index (add_if_cand proof_vect) refed_by_vect []
    4.97 -      |> Inttab.make_list
    4.98 -
    4.99 -    (* Enrich context with local facts *)
   4.100 -    val thy = Proof_Context.theory_of ctxt
   4.101 -    fun enrich_ctxt (Assume (label, t)) ctxt = 
   4.102 -        Proof_Context.put_thms false
   4.103 -            (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
   4.104 -      | enrich_ctxt (Prove (_, label, t, _)) ctxt =
   4.105 -        Proof_Context.put_thms false
   4.106 -            (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
   4.107 -      | enrich_ctxt _ ctxt = ctxt
   4.108 -    val rich_ctxt = fold enrich_ctxt proof ctxt
   4.109 -
   4.110 -    (* Timing *)
   4.111 -    fun take_time timeout tac arg =
   4.112 -      let val timing = Timing.start () in
   4.113 -        (TimeLimit.timeLimit timeout tac arg;
   4.114 -         Timing.result timing |> #cpu |> SOME)
   4.115 -        handle _ => NONE
   4.116 -      end
   4.117 -    val sum_up_time =
   4.118 -      Vector.foldl
   4.119 -        ((fn (SOME t, (b, s)) => (b, Time.+ (t, s))
   4.120 -           | (NONE, (_, s)) => (true, Time.+ (preplay_timeout, s))) o apfst Lazy.force)
   4.121 -        (false, seconds 0.0)
   4.122 -
   4.123 -    (* Metis preplaying *)
   4.124 -    fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) =
   4.125 -      if not preplay then (fn () => SOME (seconds 0.0)) else
   4.126 -        let
   4.127 -          val facts =
   4.128 -            fact_names
   4.129 -            |>> map string_for_label 
   4.130 -            |> op @
   4.131 -            |> map (the_single o thms_of_name rich_ctxt)
   4.132 -          val goal =
   4.133 -            Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
   4.134 -          fun tac {context = ctxt, prems = _} =
   4.135 -            Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
   4.136 -        in
   4.137 -          take_time timeout (fn () => goal tac)
   4.138 -        end
   4.139 -      (*| try_metis timeout (Prove (_, _, t, Case_Split _)) = *) (*FIXME: Yet to be implemented *)
   4.140 -      | try_metis _ _ = (fn () => SOME (seconds 0.0) )
   4.141 -
   4.142 -    (* Lazy metis time vector, cache *)
   4.143 -    val metis_time =
   4.144 -      Vector.map (Lazy.lazy o try_metis preplay_timeout o the) proof_vect
   4.145 -
   4.146 -    (* Merging *)
   4.147 -    fun merge (Prove (qs1, label1, _, By_Metis (lfs1, gfs1)))
   4.148 -              (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) =
   4.149 -      let
   4.150 -        val qs = inter (op =) qs1 qs2 (* FIXME: Is this correct? *)
   4.151 -          |> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately
   4.152 -          |> member (op =) qs2 Show ? cons Show
   4.153 -        val ls = remove (op =) label1 lfs2 |> union (op =) lfs1
   4.154 -        val ss = union (op =) gfs1 gfs2
   4.155 -      in Prove (qs, label2, t, By_Metis (ls, ss)) end
   4.156 -    fun try_merge metis_time (s1, i) (s2, j) =
   4.157 -      (case get i metis_time |> Lazy.force of
   4.158 -        NONE => (NONE, metis_time)
   4.159 -      | SOME t1 =>
   4.160 -        (case get j metis_time |> Lazy.force of
   4.161 -          NONE => (NONE, metis_time)
   4.162 -        | SOME t2 =>
   4.163 -          let
   4.164 -            val s12 = merge s1 s2
   4.165 -            val timeout =
   4.166 -              Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack
   4.167 -                      |> Time.fromReal
   4.168 -          in
   4.169 -            case try_metis timeout s12 () of
   4.170 -              NONE => (NONE, metis_time)
   4.171 -            | some_t12 =>
   4.172 -              (SOME s12, metis_time
   4.173 -                         |> replace (seconds 0.0 |> SOME |> Lazy.value) i
   4.174 -                         |> replace (Lazy.value some_t12) j)
   4.175 -
   4.176 -          end))
   4.177 -
   4.178 -    fun merge_steps metis_time proof_vect refed_by cand_tab n' =
   4.179 -      if is_empty cand_tab orelse n' <= n_target orelse n'<3 then
   4.180 -        (Vector.foldr
   4.181 -           (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
   4.182 -           [] proof_vect,
   4.183 -         sum_up_time metis_time)
   4.184 -      else
   4.185 -        let
   4.186 -          val (i, cand_tab) = pop_max cand_tab
   4.187 -          val j = get i refed_by |> the_single
   4.188 -          val s1 = get i proof_vect |> the
   4.189 -          val s2 = get j proof_vect |> the
   4.190 -        in
   4.191 -          case try_merge metis_time (s1, i) (s2, j) of
   4.192 -            (NONE, metis_time) =>
   4.193 -            merge_steps metis_time proof_vect refed_by cand_tab n'
   4.194 -          | (s, metis_time) => let
   4.195 -            val refs = refs s1
   4.196 -            val refed_by = refed_by |> fold
   4.197 -              (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
   4.198 -            val new_candidates =
   4.199 -              fold (add_if_cand proof_vect)
   4.200 -                (map (fn i => (i, get i refed_by)) refs) []
   4.201 -            val cand_tab = add_list cand_tab new_candidates
   4.202 -            val proof_vect = proof_vect |> replace NONE i |> replace s j
   4.203 -          in
   4.204 -            merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
   4.205 -          end
   4.206 -        end
   4.207 -  in
   4.208 -    merge_steps metis_time proof_vect refed_by_vect cand_tab n
   4.209 -  end
   4.210 -
   4.211  val chain_direct_proof =
   4.212    let
   4.213      fun succedent_of_step (Prove (_, label, _, _)) = SOME label
   4.214 @@ -905,7 +720,7 @@
   4.215            |>> kill_useless_labels_in_proof
   4.216            |>> relabel_proof
   4.217            |>> not (null params) ? cons (Fix params)
   4.218 -        val num_steps = length isar_proof
   4.219 +        val num_steps = metis_steps_recursive isar_proof
   4.220          val isar_text =
   4.221            string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
   4.222                             isar_proof
   4.223 @@ -919,7 +734,7 @@
   4.224          | _ =>
   4.225            "\n\nStructured proof" ^
   4.226            (if verbose then
   4.227 -             " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^
   4.228 +             " (" ^ string_of_int num_steps ^ " metis step" ^ plural_s num_steps ^
   4.229               (if preplay then ", " ^ string_from_ext_time ext_time
   4.230                else "") ^ ")"
   4.231             else if preplay then
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:22:17 2012 +0100
     5.3 @@ -0,0 +1,226 @@
     5.4 +signature SLEDGEHAMMER_SHRINK =
     5.5 +sig
     5.6 +  type isar_step = Sledgehammer_Isar_Reconstruct.isar_step
     5.7 +	val shrink_proof : 
     5.8 +    bool -> Proof.context -> string -> string -> bool -> Time.time -> real
     5.9 +    -> isar_step list -> isar_step list * (bool * Time.time)
    5.10 +end
    5.11 +
    5.12 +structure Sledgehammer_Shrink (* : SLEDGEHAMMER_SHRINK *) =
    5.13 +struct
    5.14 +
    5.15 +open Sledgehammer_Isar_Reconstruct
    5.16 +
    5.17 +(* Parameters *)
    5.18 +val merge_timeout_slack = 1.2
    5.19 +
    5.20 +(* Data structures, orders *)
    5.21 +val label_ord = prod_ord int_ord fast_string_ord o pairself swap
    5.22 +structure Label_Table = Table(
    5.23 +  type key = label
    5.24 +  val ord = label_ord)
    5.25 +
    5.26 +(* Timing *)
    5.27 +type ext_time = bool * Time.time
    5.28 +fun ext_time_add (b1, t1) (b2, t2) : ext_time = (b1 orelse b2, t1+t2)
    5.29 +val no_time = (false, seconds 0.0)
    5.30 +fun take_time timeout tac arg =
    5.31 +  let val timing = Timing.start () in
    5.32 +    (TimeLimit.timeLimit timeout tac arg;
    5.33 +     Timing.result timing |> #cpu |> SOME)
    5.34 +    handle _ => NONE
    5.35 +  end
    5.36 +fun sum_up_time timeout =
    5.37 +  Vector.foldl
    5.38 +    ((fn (SOME t, (b, ts)) => (b, t+ts)
    5.39 +       | (NONE, (_, ts)) => (true, ts+timeout)) o apfst Lazy.force)
    5.40 +    no_time
    5.41 +
    5.42 +(* clean vector interface *)
    5.43 +fun get i v = Vector.sub (v, i)
    5.44 +fun replace x i v = Vector.update (v, i, x)
    5.45 +fun update f i v = replace (get i v |> f) i v
    5.46 +fun v_fold_index f v s =
    5.47 +  Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
    5.48 +
    5.49 +(* Queue interface to table *)
    5.50 +fun pop tab key =
    5.51 +  let val v = hd (Inttab.lookup_list tab key) in
    5.52 +    (v, Inttab.remove_list (op =) (key, v) tab)
    5.53 +  end
    5.54 +fun pop_max tab = pop tab (the (Inttab.max_key tab))
    5.55 +fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
    5.56 +
    5.57 +(* Main function for shrinking proofs *)
    5.58 +fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
    5.59 +                 isar_shrink proof =
    5.60 +let
    5.61 +  fun shrink_top_level top_level ctxt proof =
    5.62 +  let
    5.63 +    (* proof vector *)
    5.64 +    val proof_vect = proof |> map SOME |> Vector.fromList
    5.65 +    val n = metis_steps_top_level proof
    5.66 +    val n_target = Real.fromInt n / isar_shrink |> Real.round
    5.67 +
    5.68 +    (* table for mapping from (top-level-)label to proof position *)
    5.69 +    fun update_table (i, Assume (label, _)) = 
    5.70 +        Label_Table.update_new (label, i)
    5.71 +      | update_table (i, Prove (_, label, _, _)) =
    5.72 +        Label_Table.update_new (label, i)
    5.73 +      | update_table _ = I
    5.74 +    val label_index_table = fold_index update_table proof Label_Table.empty
    5.75 +
    5.76 +    (* proof references *)
    5.77 +    fun refs (Prove (_, _, _, By_Metis (lfs, _))) =
    5.78 +        maps (the_list o Label_Table.lookup label_index_table) lfs
    5.79 +      | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
    5.80 +        maps (the_list o Label_Table.lookup label_index_table) lfs 
    5.81 +          @ maps (maps refs) cases
    5.82 +      | refs _ = []
    5.83 +    val refed_by_vect =
    5.84 +      Vector.tabulate (Vector.length proof_vect, (fn _ => []))
    5.85 +      |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
    5.86 +      |> Vector.map rev (* after rev, indices are sorted in ascending order *)
    5.87 +
    5.88 +    (* candidates for elimination, use table as priority queue (greedy
    5.89 +       algorithm) *)
    5.90 +    fun add_if_cand proof_vect (i, [j]) =
    5.91 +        (case (the (get i proof_vect), the (get j proof_vect)) of
    5.92 +          (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
    5.93 +            cons (Term.size_of_term t, i)
    5.94 +        | _ => I)
    5.95 +      | add_if_cand _ _ = I
    5.96 +    val cand_tab = 
    5.97 +      v_fold_index (add_if_cand proof_vect) refed_by_vect []
    5.98 +      |> Inttab.make_list
    5.99 +
   5.100 +    (* Metis Preplaying *)
   5.101 +    fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) =
   5.102 +      if not preplay then (fn () => SOME (seconds 0.0)) else
   5.103 +        let
   5.104 +          val facts =
   5.105 +            fact_names
   5.106 +            |>> map string_for_label 
   5.107 +            |> op @
   5.108 +            |> map (the_single o thms_of_name ctxt) (* FIXME: maps (the o thms_of_name ctxt) *)
   5.109 +          val goal =
   5.110 +            Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
   5.111 +          fun tac {context = ctxt, prems = _} =
   5.112 +            Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
   5.113 +        in
   5.114 +          take_time timeout (fn () => goal tac)
   5.115 +        end
   5.116 +      | try_metis _ _ = (fn () => SOME (seconds 0.0) )
   5.117 +
   5.118 +    (* Lazy metis time vector, cache *)
   5.119 +    val metis_time =
   5.120 +      Vector.map (Lazy.lazy o try_metis preplay_timeout o the) proof_vect
   5.121 +
   5.122 +    (* Merging *)
   5.123 +    fun merge (Prove (qs1, label1, _, By_Metis (lfs1, gfs1)))
   5.124 +              (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) =
   5.125 +      let
   5.126 +        val qs = inter (op =) qs1 qs2 (* FIXME: Is this correct? *)
   5.127 +          |> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately
   5.128 +          |> member (op =) qs2 Show ? cons Show
   5.129 +        val ls = remove (op =) label1 lfs2 |> union (op =) lfs1
   5.130 +        val ss = union (op =) gfs1 gfs2
   5.131 +      in Prove (qs, label2, t, By_Metis (ls, ss)) end
   5.132 +    fun try_merge metis_time (s1, i) (s2, j) =
   5.133 +      (case get i metis_time |> Lazy.force of
   5.134 +        NONE => (NONE, metis_time)
   5.135 +      | SOME t1 =>
   5.136 +        (case get j metis_time |> Lazy.force of
   5.137 +          NONE => (NONE, metis_time)
   5.138 +        | SOME t2 =>
   5.139 +          let
   5.140 +            val s12 = merge s1 s2
   5.141 +            val timeout =
   5.142 +              Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack
   5.143 +                      |> Time.fromReal
   5.144 +          in
   5.145 +            case try_metis timeout s12 () of
   5.146 +              NONE => (NONE, metis_time)
   5.147 +            | some_t12 =>
   5.148 +              (SOME s12, metis_time
   5.149 +                         |> replace (seconds 0.0 |> SOME |> Lazy.value) i
   5.150 +                         |> replace (Lazy.value some_t12) j)
   5.151 +
   5.152 +          end))
   5.153 +
   5.154 +    fun merge_steps metis_time proof_vect refed_by cand_tab n' =
   5.155 +      if Inttab.is_empty cand_tab 
   5.156 +        orelse n' <= n_target 
   5.157 +        orelse (top_level andalso Vector.length proof_vect<3)
   5.158 +      then
   5.159 +        (Vector.foldr
   5.160 +           (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
   5.161 +           [] proof_vect,
   5.162 +         sum_up_time preplay_timeout metis_time)
   5.163 +      else
   5.164 +        let
   5.165 +          val (i, cand_tab) = pop_max cand_tab
   5.166 +          val j = get i refed_by |> the_single
   5.167 +          val s1 = get i proof_vect |> the
   5.168 +          val s2 = get j proof_vect |> the
   5.169 +        in
   5.170 +          case try_merge metis_time (s1, i) (s2, j) of
   5.171 +            (NONE, metis_time) =>
   5.172 +            merge_steps metis_time proof_vect refed_by cand_tab n'
   5.173 +          | (s, metis_time) => 
   5.174 +          let
   5.175 +            val refs = refs s1
   5.176 +            val refed_by = refed_by |> fold
   5.177 +              (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
   5.178 +            val new_candidates =
   5.179 +              fold (add_if_cand proof_vect)
   5.180 +                (map (fn i => (i, get i refed_by)) refs) []
   5.181 +            val cand_tab = add_list cand_tab new_candidates
   5.182 +            val proof_vect = proof_vect |> replace NONE i |> replace s j
   5.183 +          in
   5.184 +            merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
   5.185 +          end
   5.186 +        end
   5.187 +  in
   5.188 +    merge_steps metis_time proof_vect refed_by_vect cand_tab n
   5.189 +  end
   5.190 +  
   5.191 +  fun shrink_proof' top_level ctxt proof = 
   5.192 +    let
   5.193 +      (* Enrich context with top-level facts *)
   5.194 +      val thy = Proof_Context.theory_of ctxt
   5.195 +      fun enrich_ctxt (Assume (label, t)) ctxt = 
   5.196 +          Proof_Context.put_thms false
   5.197 +            (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
   5.198 +        | enrich_ctxt (Prove (_, label, t, _)) ctxt =
   5.199 +          Proof_Context.put_thms false
   5.200 +            (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
   5.201 +        | enrich_ctxt _ ctxt = ctxt
   5.202 +      val rich_ctxt = fold enrich_ctxt proof ctxt
   5.203 +
   5.204 +      (* Shrink case_splits and top-levl *)
   5.205 +      val ((proof, top_level_time), lower_level_time) = 
   5.206 +        proof |> shrink_case_splits rich_ctxt
   5.207 +              |>> shrink_top_level top_level rich_ctxt
   5.208 +    in
   5.209 +      (proof, ext_time_add lower_level_time top_level_time)
   5.210 +    end
   5.211 +
   5.212 +  and shrink_case_splits ctxt proof =
   5.213 +    let
   5.214 +      fun shrink_and_collect_time shrink candidates =
   5.215 +            let fun f_m cand time = shrink cand ||> ext_time_add time
   5.216 +            in fold_map f_m candidates no_time end
   5.217 +      val shrink_case_split = shrink_and_collect_time (shrink_proof' false ctxt)
   5.218 +      fun shrink (Prove (qs, lbl, t, Case_Split (cases, facts))) =
   5.219 +          let val (cases, time) = shrink_case_split cases
   5.220 +          in (Prove (qs, lbl, t, Case_Split (cases, facts)), time) end
   5.221 +        | shrink step = (step, no_time)
   5.222 +    in 
   5.223 +      shrink_and_collect_time shrink proof
   5.224 +    end
   5.225 +in
   5.226 +  shrink_proof' true ctxt proof
   5.227 +end
   5.228 +
   5.229 +end