# HG changeset patch # User blanchet # Date 1412266209 -7200 # Node ID 64f6b4bd52a7ccfd2683c73a3a15a0e7fcbaafd3 # Parent 1edba015249185ddcfed8b59b5677fb0a55cdcdd more precise lemma insertion diff -r 1edba0152491 -r 64f6b4bd52a7 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 02 17:40:46 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 02 18:10:09 2014 +0200 @@ -139,7 +139,7 @@ basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods -val skolem_methods = Moura_Method :: basic_systematic_methods +val skolem_methods = Moura_Method :: systematic_methods fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = @@ -230,10 +230,31 @@ and is_referenced_in_proof l (Proof (_, _, steps)) = exists (is_referenced_in_step l) steps - fun insert_lemma lem [] = [lem] - | insert_lemma lem (steps as step :: steps') = - if is_referenced_in_step (the (label_of_isar_step lem)) step then lem :: steps - else step :: insert_lemma lem steps' + fun insert_lemma_in_step lem + (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) = + let val l' = the (label_of_isar_step lem) in + if member (op =) ls l' then + [lem, step] + else + let val refs = map (is_referenced_in_proof l') subs in + if length (filter I refs) = 1 then + let + val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs + in + [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] + end + else + [lem, step] + end + end + and insert_lemma_in_steps lem [] = [lem] + | insert_lemma_in_steps lem (step :: steps) = + if is_referenced_in_step (the (label_of_isar_step lem)) step then + insert_lemma_in_step lem step @ steps + else + step :: insert_lemma_in_steps lem steps + and insert_lemma_in_proof lem (Proof (fix, assms, steps)) = + Proof (fix, assms, insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst @@ -320,7 +341,7 @@ isar_steps outer (SOME l) (step :: accum) infs end and isar_proof outer fix assms lems infs = - Proof (fix, assms, fold_rev insert_lemma lems (isar_steps outer NONE [] infs)) + Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) val trace = Config.get ctxt trace