handle Vampire's definitions smoothly
authorblanchet
Wed Jun 02 17:19:44 2010 +0200 (2010-06-02)
changeset 373232f2f0d246d0f
parent 37322 0347b1a16682
child 37324 d77250dd2416
handle Vampire's definitions smoothly
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 17:06:28 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 17:19:44 2010 +0200
     1.3 @@ -487,8 +487,8 @@
     1.4  fun decode_lines ctxt full_types tfrees lines =
     1.5    fst (fold_map (decode_line full_types tfrees) lines ctxt)
     1.6  
     1.7 -fun aint_inference _ (Definition _) = true
     1.8 -  | aint_inference t (Inference (_, t', _)) = not (t aconv t')
     1.9 +fun aint_actual_inference _ (Definition _) = true
    1.10 +  | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
    1.11  
    1.12  (* No "real" literals means only type information (tfree_tcs, clsrel, or
    1.13     clsarity). *)
    1.14 @@ -510,7 +510,7 @@
    1.15        if is_only_type_information t then
    1.16          map (replace_deps_in_line (num, [])) lines
    1.17        (* Is there a repetition? If so, replace later line by earlier one. *)
    1.18 -      else case take_prefix (aint_inference t) lines of
    1.19 +      else case take_prefix (aint_actual_inference t) lines of
    1.20          (_, []) => lines (*no repetition of proof line*)
    1.21        | (pre, Inference (num', _, _) :: post) =>
    1.22          pre @ map (replace_deps_in_line (num', [num])) post
    1.23 @@ -523,7 +523,7 @@
    1.24      if is_only_type_information t then
    1.25        Inference (num, t, deps) :: lines
    1.26      (* Is there a repetition? If so, replace later line by earlier one. *)
    1.27 -    else case take_prefix (aint_inference t) lines of
    1.28 +    else case take_prefix (aint_actual_inference t) lines of
    1.29        (* FIXME: Doesn't this code risk conflating proofs involving different
    1.30           types?? *)
    1.31         (_, []) => Inference (num, t, deps) :: lines
    1.32 @@ -539,8 +539,8 @@
    1.33  and delete_dep num lines =
    1.34    fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
    1.35  
    1.36 -(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
    1.37 -   removing the offending lines often does the trick. *)
    1.38 +(* ATPs sometimes reuse free variable names in the strangest ways. Removing
    1.39 +   offending lines often does the trick. *)
    1.40  fun is_bad_free frees (Free x) = not (member (op =) frees x)
    1.41    | is_bad_free _ _ = false
    1.42  
    1.43 @@ -549,8 +549,8 @@
    1.44                                          $ t1 $ t2)) = (t1 aconv t2)
    1.45    | is_trivial_formula t = false
    1.46  
    1.47 -fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
    1.48 -    (j, line :: lines)
    1.49 +fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
    1.50 +    (j, line :: map (replace_deps_in_line (num, [])) lines)
    1.51    | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
    1.52                       (Inference (num, t, deps)) (j, lines) =
    1.53      (j + 1,