moved code around
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 552209d833fe96c51
parent 55219 6fe9fd75f9d7
child 55221 ee90eebb8b73
moved code around
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -103,89 +103,6 @@
     1.4          add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
     1.5      end
     1.6  
     1.7 -val add_labels_of_proof =
     1.8 -  steps_of_proof
     1.9 -  #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
    1.10 -
    1.11 -fun kill_useless_labels_in_proof proof =
    1.12 -  let
    1.13 -    val used_ls = add_labels_of_proof proof []
    1.14 -
    1.15 -    fun kill_label l = if member (op =) used_ls l then l else no_label
    1.16 -    fun kill_assms assms = map (apfst kill_label) assms
    1.17 -
    1.18 -    fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
    1.19 -        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
    1.20 -      | kill_step step = step
    1.21 -    and kill_proof (Proof (fix, assms, steps)) =
    1.22 -      Proof (fix, kill_assms assms, map kill_step steps)
    1.23 -  in
    1.24 -    kill_proof proof
    1.25 -  end
    1.26 -
    1.27 -val assume_prefix = "a"
    1.28 -val have_prefix = "f"
    1.29 -
    1.30 -val relabel_proof =
    1.31 -  let
    1.32 -    fun fresh_label depth prefix (accum as (l, subst, next)) =
    1.33 -      if l = no_label then
    1.34 -        accum
    1.35 -      else
    1.36 -        let val l' = (replicate_string (depth + 1) prefix, next) in
    1.37 -          (l', (l, l') :: subst, next + 1)
    1.38 -        end
    1.39 -
    1.40 -    fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
    1.41 -
    1.42 -    fun relabel_assm depth (l, t) (subst, next) =
    1.43 -      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
    1.44 -        ((l, t), (subst, next))
    1.45 -      end
    1.46 -
    1.47 -    fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
    1.48 -
    1.49 -    fun relabel_steps _ _ _ [] = []
    1.50 -      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
    1.51 -        let
    1.52 -          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
    1.53 -          val sub = relabel_proofs subst depth sub
    1.54 -          val by = apfst (relabel_facts subst) by
    1.55 -        in
    1.56 -          Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
    1.57 -        end
    1.58 -      | relabel_steps subst depth next (step :: steps) =
    1.59 -        step :: relabel_steps subst depth next steps
    1.60 -    and relabel_proof subst depth (Proof (fix, assms, steps)) =
    1.61 -      let val (assms, subst) = relabel_assms subst depth assms in
    1.62 -        Proof (fix, assms, relabel_steps subst depth 1 steps)
    1.63 -      end
    1.64 -    and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
    1.65 -  in
    1.66 -    relabel_proof [] 0
    1.67 -  end
    1.68 -
    1.69 -val chain_direct_proof =
    1.70 -  let
    1.71 -    fun chain_qs_lfs NONE lfs = ([], lfs)
    1.72 -      | chain_qs_lfs (SOME l0) lfs =
    1.73 -        if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
    1.74 -    fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
    1.75 -        let val (qs', lfs) = chain_qs_lfs lbl lfs in
    1.76 -          Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
    1.77 -        end
    1.78 -      | chain_step _ step = step
    1.79 -    and chain_steps _ [] = []
    1.80 -      | chain_steps (prev as SOME _) (i :: is) =
    1.81 -        chain_step prev i :: chain_steps (label_of_step i) is
    1.82 -      | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
    1.83 -    and chain_proof (Proof (fix, assms, steps)) =
    1.84 -      Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
    1.85 -    and chain_proofs proofs = map (chain_proof) proofs
    1.86 -  in
    1.87 -    chain_proof
    1.88 -  end
    1.89 -
    1.90  type isar_params =
    1.91    bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
    1.92  
    1.93 @@ -378,7 +295,9 @@
    1.94                 (try0_isar ? minimize_isar_step_dependencies preplay_data)
    1.95            |> tap (trace_isar_proof "Minimized")
    1.96            |> `overall_preplay_outcome
    1.97 -          ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
    1.98 +          ||> chain_isar_proof
    1.99 +          ||> kill_useless_labels_in_isar_proof
   1.100 +          ||> relabel_isar_proof_finally
   1.101        in
   1.102          (case string_of_isar_proof false isar_proof of
   1.103            "" =>
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     2.3 @@ -42,7 +42,11 @@
     2.4    structure Canonical_Label_Tab : TABLE
     2.5  
     2.6    val canonical_label_ord : (label * label) -> order
     2.7 +
     2.8 +  val chain_isar_proof : isar_proof -> isar_proof
     2.9 +  val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
    2.10    val relabel_isar_proof_canonically : isar_proof -> isar_proof
    2.11 +  val relabel_isar_proof_finally : isar_proof -> isar_proof
    2.12  
    2.13    val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> bool ->
    2.14      isar_proof -> string
    2.15 @@ -127,6 +131,38 @@
    2.16    type key = label
    2.17    val ord = canonical_label_ord)
    2.18  
    2.19 +fun chain_qs_lfs NONE lfs = ([], lfs)
    2.20 +  | chain_qs_lfs (SOME l0) lfs =
    2.21 +    if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
    2.22 +fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
    2.23 +    let val (qs', lfs) = chain_qs_lfs lbl lfs in
    2.24 +      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), methss))
    2.25 +    end
    2.26 +  | chain_isar_step _ step = step
    2.27 +and chain_isar_steps _ [] = []
    2.28 +  | chain_isar_steps (prev as SOME _) (i :: is) =
    2.29 +    chain_isar_step prev i :: chain_isar_steps (label_of_step i) is
    2.30 +  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_step i) is
    2.31 +and chain_isar_proof (Proof (fix, assms, steps)) =
    2.32 +  Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
    2.33 +
    2.34 +fun kill_useless_labels_in_isar_proof proof =
    2.35 +  let
    2.36 +    val used_ls =
    2.37 +      fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
    2.38 +        (steps_of_proof proof) []
    2.39 +
    2.40 +    fun kill_label l = if member (op =) used_ls l then l else no_label
    2.41 +
    2.42 +    fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
    2.43 +        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
    2.44 +      | kill_step step = step
    2.45 +    and kill_proof (Proof (fix, assms, steps)) =
    2.46 +      Proof (fix, map (apfst kill_label) assms, map kill_step steps)
    2.47 +  in
    2.48 +    kill_proof proof
    2.49 +  end
    2.50 +
    2.51  fun relabel_isar_proof_canonically proof =
    2.52    let
    2.53      fun next_label l (next, subst) =
    2.54 @@ -162,6 +198,48 @@
    2.55      fst (do_proof proof (0, []))
    2.56    end
    2.57  
    2.58 +val assume_prefix = "a"
    2.59 +val have_prefix = "f"
    2.60 +
    2.61 +val relabel_isar_proof_finally =
    2.62 +  let
    2.63 +    fun fresh_label depth prefix (accum as (l, subst, next)) =
    2.64 +      if l = no_label then
    2.65 +        accum
    2.66 +      else
    2.67 +        let val l' = (replicate_string (depth + 1) prefix, next) in
    2.68 +          (l', (l, l') :: subst, next + 1)
    2.69 +        end
    2.70 +
    2.71 +    fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
    2.72 +
    2.73 +    fun relabel_assm depth (l, t) (subst, next) =
    2.74 +      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
    2.75 +        ((l, t), (subst, next))
    2.76 +      end
    2.77 +
    2.78 +    fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
    2.79 +
    2.80 +    fun relabel_steps _ _ _ [] = []
    2.81 +      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
    2.82 +        let
    2.83 +          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
    2.84 +          val sub = relabel_proofs subst depth sub
    2.85 +          val by = apfst (relabel_facts subst) by
    2.86 +        in
    2.87 +          Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
    2.88 +        end
    2.89 +      | relabel_steps subst depth next (step :: steps) =
    2.90 +        step :: relabel_steps subst depth next steps
    2.91 +    and relabel_proof subst depth (Proof (fix, assms, steps)) =
    2.92 +      let val (assms, subst) = relabel_assms subst depth assms in
    2.93 +        Proof (fix, assms, relabel_steps subst depth 1 steps)
    2.94 +      end
    2.95 +    and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
    2.96 +  in
    2.97 +    relabel_proof [] 0
    2.98 +  end
    2.99 +
   2.100  val indent_size = 2
   2.101  
   2.102  fun string_of_isar_proof ctxt type_enc lam_trans i n all_methods proof =