better treatment of methods: uses Method.ctxt_args to refer to current
simpset and claset. Needed to fix problems with Recur.thy
--- a/src/HOL/Auth/Message.thy Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Message.thy Fri Apr 27 17:16:21 2001 +0200
@@ -143,15 +143,23 @@
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
method_setup spy_analz = {*
- Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_spy_analz_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1)) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *}
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ atomic_spy_analz_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1)) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *}
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
"for debugging spy_analz"
end
--- a/src/HOL/Auth/Message_lemmas.ML Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Message_lemmas.ML Fri Apr 27 17:16:21 2001 +0200
@@ -865,8 +865,8 @@
impOfSubs Fake_parts_insert] THEN'
eresolve_tac [asm_rl, synth.Inj];
-fun Fake_insert_simp_tac i =
- REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i;
+fun Fake_insert_simp_tac ss i =
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
@@ -874,14 +874,15 @@
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
-val atomic_spy_analz_tac = SELECT_GOAL
- (Fake_insert_simp_tac 1
+fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
+ (Fake_insert_simp_tac ss 1
THEN
IF_UNSOLVED (Blast.depth_tac
- (claset() addIs [analz_insertI,
+ (cs addIs [analz_insertI,
impOfSubs analz_subset_parts]) 4 1));
-fun spy_analz_tac i =
+(*The explicit claset and simpset arguments help it work with Isar*)
+fun gen_spy_analz_tac (cs,ss) i =
DETERM
(SELECT_GOAL
(EVERY
@@ -889,9 +890,11 @@
(REPEAT o CHANGED)
(res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
- Simp_tac 1,
+ simp_tac ss 1,
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
+ DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i);
+
+fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i;
(*By default only o_apply is built-in. But in the presence of eta-expansion
this means that some terms displayed as (f o g) will be rewritten, and others
--- a/src/HOL/Auth/Public.thy Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Public.thy Fri Apr 27 17:16:21 2001 +0200
@@ -40,7 +40,9 @@
(*Specialized methods*)
method_setup possibility = {*
- Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
"for proving possibility theorems"
end
--- a/src/HOL/Auth/Public_lemmas.ML Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Public_lemmas.ML Fri Apr 27 17:16:21 2001 +0200
@@ -139,14 +139,16 @@
by (Fast_tac 1);
qed "Nonce_supply";
-(*Tactic for possibility theorems*)
-fun possibility_tac st = st |>
+(*Tactic for possibility theorems (Isar interface)*)
+fun gen_possibility_tac ss state = state |>
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
+ (ALLGOALS (simp_tac (ss delsimps [used_Says]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply]));
+(*Tactic for possibility theorems (ML script version)*)
+fun possibility_tac state = gen_possibility_tac (simpset()) state;
(*** Specialized rewriting for the analz_image_... theorems ***)
--- a/src/HOL/Auth/Recur.thy Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Apr 27 17:16:21 2001 +0200
@@ -127,38 +127,44 @@
done
-(*Case two: Alice, Bob and the server
-WHY WON'T INSERT LET VARS REMAIN???
+(*Case two: Alice, Bob and the server*)
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-apply (insert Nonce_supply2 Key_supply2)
+apply (tactic "cut_facts_tac [Nonce_supply2, Key_supply2] 1")
apply clarify
apply (intro exI bexI)
-apply (rule_tac [2] recur.Nil [THEN recur.RA1, THEN recur.RA2,
- THEN recur.RA3 [OF _ _ respond.One]])
-apply possibility
-apply (DEPTH_SOLVE (erule asm_rl less_not_refl2 less_not_refl3))
+apply (rule_tac [2]
+ recur.Nil [THEN recur.RA1,
+ THEN recur.RA2,
+ THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
+ THEN recur.RA4])
+apply (tactic "basic_possibility_tac")
+apply (tactic
+ "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
done
-*)
(*Case three: Alice, Bob, Charlie and the server
- TOO SLOW to run every time!
-Goal "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
+ Rather slow (16 seconds) to run every time...
+lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
-by (REPEAT (eresolve_tac [exE, conjE] 1));
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
- (respond.One RS respond.Cons RS respond.Cons RSN
- (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
-by basic_possibility_tac;
-by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
- ORELSE
- eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
-result();
-****)
+apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
+apply clarify
+apply (intro exI bexI)
+apply (rule_tac [2]
+ recur.Nil [THEN recur.RA1,
+ THEN recur.RA2, THEN recur.RA2,
+ THEN recur.RA3
+ [OF _ _ respond.One
+ [THEN respond.Cons, THEN respond.Cons]],
+ THEN recur.RA4, THEN recur.RA4])
+apply (tactic "basic_possibility_tac")
+apply (tactic
+ "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \
+\ eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
+done
+*)
(**** Inductive proofs about recur ****)
@@ -274,7 +280,8 @@
(*Everything that's hashed is already in past traffic. *)
-lemma Hash_imp_body: "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
+lemma Hash_imp_body:
+ "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)"
apply (erule rev_mp)
apply (erule recur.induct,
@@ -405,11 +412,6 @@
done
-(*WHAT'S GOING ON??*)
-method_setup newbla = {*
- Method.no_args (Method.METHOD (fn facts => Blast_tac 1)) *}
- "for debugging spy_analz"
-
lemma Spy_not_see_session_key:
"[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs);
A \<notin> bad; A' \<notin> bad; evs \<in> recur |]
@@ -423,12 +425,7 @@
(*Base*)
apply force
(*Fake*)
-apply (intro allI impI notI conjI iffI)
-apply Fake_insert_simp
-apply (blast );
-(*???ASK MARKUS WHY METHOD_SETUP DOESN'T WORK. Should be just
apply spy_analz
-*)
(*RA2*)
apply blast
(*RA3 remains*)
@@ -496,7 +493,8 @@
apply blast
(*RA2: it cannot be a new Nonce, contradiction.*)
apply blast
-(*RA3*)
+(*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting,
+ which however would break all other steps.*)
apply (simp add: parts_insert_spies, blast)
(*RA4*)
apply blast
--- a/src/HOL/Auth/Shared.thy Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Shared.thy Fri Apr 27 17:16:21 2001 +0200
@@ -15,7 +15,7 @@
shrK :: "agent => key" (*symmetric keys*)
axioms
- isSym_keys: "K \\<in> symKeys" (*All keys are symmetric*)
+ isSym_keys: "K \<in> symKeys" (*All keys are symmetric*)
inj_shrK: "inj shrK" (*No two agents have the same long-term key*)
primrec
@@ -38,7 +38,7 @@
(*Lets blast_tac perform this step without needing the simplifier*)
lemma invKey_shrK_iff [iff]:
- "(Key (invKey K) \\<in> X) = (Key K \\<in> X)"
+ "(Key (invKey K) \<in> X) = (Key K \<in> X)"
by auto;
(*Specialized methods*)
@@ -52,7 +52,9 @@
"for proving the Session Key Compromise theorem"
method_setup possibility = {*
- Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
"for proving possibility theorems"
end
--- a/src/HOL/Auth/Shared_lemmas.ML Wed Apr 25 10:31:39 2001 +0200
+++ b/src/HOL/Auth/Shared_lemmas.ML Fri Apr 27 17:16:21 2001 +0200
@@ -201,14 +201,17 @@
(*Omitting used_Says makes the tactic much faster: it leaves expressions
such as Nonce ?N \\<notin> used evs that match Nonce_supply*)
-fun possibility_tac st = st |>
+fun gen_possibility_tac ss state = state |>
(REPEAT
- (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets]
+ (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets]
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
+(*Tactic for possibility theorems (ML script version)*)
+fun possibility_tac state = gen_possibility_tac (simpset()) state;
+
(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
fun basic_possibility_tac st = st |>