unbreak "only" option of Sledgehammer
authorblanchet
Fri Aug 20 16:44:48 2010 +0200 (2010-08-20)
changeset 38617f7b32911340b
parent 38616 d22c111837ad
child 38618 5536897d04c2
unbreak "only" option of Sledgehammer
src/HOL/Auth/NS_Shared.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 20 16:28:53 2010 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Aug 20 16:44:48 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
     1.6  
     1.7 -theory NS_Shared imports Public begin
     1.8 +theory NS_Shared imports Sledgehammer2d(*###*) Public begin
     1.9  
    1.10  text{*
    1.11  From page 247 of
    1.12 @@ -311,6 +311,8 @@
    1.13        Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
    1.14        Says B A (Crypt K (Nonce NB)) \<in> set evs"
    1.15  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.16 +sledgehammer [atp = e, overlord] (Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
    1.17 +apply (metis Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
    1.18  apply (analz_mono_contra, simp_all, blast)
    1.19  txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
    1.20      @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 16:28:53 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 16:44:48 2010 +0200
     2.3 @@ -12,6 +12,8 @@
     2.4  
     2.5    val trace : bool Unsynchronized.ref
     2.6    val chained_prefix : string
     2.7 +  val name_thms_pair_from_ref :
     2.8 +    Proof.context -> thm list -> Facts.ref -> string * thm list
     2.9    val relevant_facts :
    2.10      bool -> real -> real -> bool -> int -> bool -> relevance_override
    2.11      -> Proof.context * (thm list * 'a) -> term list -> term
    2.12 @@ -35,6 +37,14 @@
    2.13  (* Used to label theorems chained into the goal. *)
    2.14  val chained_prefix = sledgehammer_prefix ^ "chained_"
    2.15  
    2.16 +fun name_thms_pair_from_ref ctxt chained_ths xref =
    2.17 +  let
    2.18 +    val ths = ProofContext.get_fact ctxt xref
    2.19 +    val name = Facts.string_of_ref xref
    2.20 +               |> forall (member Thm.eq_thm chained_ths) ths
    2.21 +                  ? prefix chained_prefix
    2.22 +  in (name, ths) end
    2.23 +
    2.24  
    2.25  (***************************************************************)
    2.26  (* Relevance Filtering                                         *)
    2.27 @@ -565,7 +575,8 @@
    2.28      val add_thms = maps (ProofContext.get_fact ctxt) add
    2.29      val axioms =
    2.30        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
    2.31 -          (if only then [] else all_name_thms_pairs ctxt add_thms chained_ths)
    2.32 +          (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
    2.33 +           else all_name_thms_pairs ctxt add_thms chained_ths)
    2.34        |> make_unique
    2.35        |> map (apsnd Clausifier.transform_elim_theorem)
    2.36        |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Fri Aug 20 16:28:53 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Fri Aug 20 16:44:48 2010 +0200
     3.3 @@ -154,14 +154,6 @@
     3.4      handle ERROR msg => (NONE, "Error: " ^ msg)
     3.5    end
     3.6  
     3.7 -fun name_thms_pair_from_ref ctxt chained_ths xref =
     3.8 -  let
     3.9 -    val ths = ProofContext.get_fact ctxt xref
    3.10 -    val name = Facts.string_of_ref xref
    3.11 -               |> forall (member Thm.eq_thm chained_ths) ths
    3.12 -                  ? prefix chained_prefix
    3.13 -  in (name, ths) end
    3.14 -
    3.15  fun run_minimize params i refs state =
    3.16    let
    3.17      val ctxt = Proof.context_of state