--- a/src/HOL/Auth/NS_Shared.thy Fri Aug 20 16:28:53 2010 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Fri Aug 20 16:44:48 2010 +0200
@@ -5,7 +5,7 @@
header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
-theory NS_Shared imports Public begin
+theory NS_Shared imports Sledgehammer2d(*###*) Public begin
text{*
From page 247 of
@@ -311,6 +311,8 @@
Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
Says B A (Crypt K (Nonce NB)) \<in> set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+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)
+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)
apply (analz_mono_contra, simp_all, blast)
txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
@{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 16:28:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 16:44:48 2010 +0200
@@ -12,6 +12,8 @@
val trace : bool Unsynchronized.ref
val chained_prefix : string
+ val name_thms_pair_from_ref :
+ Proof.context -> thm list -> Facts.ref -> string * thm list
val relevant_facts :
bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
@@ -35,6 +37,14 @@
(* Used to label theorems chained into the goal. *)
val chained_prefix = sledgehammer_prefix ^ "chained_"
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix
+ in (name, ths) end
+
(***************************************************************)
(* Relevance Filtering *)
@@ -565,7 +575,8 @@
val add_thms = maps (ProofContext.get_fact ctxt) add
val axioms =
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
- (if only then [] else all_name_thms_pairs ctxt add_thms chained_ths)
+ (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
+ else all_name_thms_pairs ctxt add_thms chained_ths)
|> make_unique
|> map (apsnd Clausifier.transform_elim_theorem)
|> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 20 16:28:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Fri Aug 20 16:44:48 2010 +0200
@@ -154,14 +154,6 @@
handle ERROR msg => (NONE, "Error: " ^ msg)
end
-fun name_thms_pair_from_ref ctxt chained_ths xref =
- let
- val ths = ProofContext.get_fact ctxt xref
- val name = Facts.string_of_ref xref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
-
fun run_minimize params i refs state =
let
val ctxt = Proof.context_of state