Made proofs more concise by replacing calls to spy_analz_tac by uses of
analz_insert_eq in rewriting
--- a/src/HOL/Auth/NS_Shared.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Thu Jun 19 11:31:14 1997 +0200
@@ -221,8 +221,8 @@
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
(*Takes 24 secs*)
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
-(*NS4, Fake*)
-by (EVERY (map spy_analz_tac [3,2]));
+(*Fake*)
+by (spy_analz_tac 2);
(*Base*)
by (Blast_tac 1);
qed_spec_mp "analz_image_freshK";
@@ -283,15 +283,18 @@
by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
+ (!simpset addsimps ([analz_insert_eq, not_parts_not_analz,
+ analz_insert_freshK] @ pushes)
setloop split_tac [expand_if])));
-(*NS4, Fake*)
-by (EVERY (map spy_analz_tac [4,1]));
+(*Oops*)
+by (blast_tac (!claset addDs [unique_session_keys]) 5);
+(*NS4*)
+by (Blast_tac 4);
(*NS2*)
by (blast_tac (!claset addSEs sees_Spy_partsEs
- addIs [parts_insertI, impOfSubs analz_subset_parts]) 1);
-(*Oops*)
-by (blast_tac (!claset addDs [unique_session_keys]) 2);
+ addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
(*NS3*) (**LEVEL 6 **)
by (step_tac (!claset delrules [impCE]) 1);
by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
--- a/src/HOL/Auth/OtwayRees.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Jun 19 11:31:14 1997 +0200
@@ -192,10 +192,10 @@
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Fake*)
+by (spy_analz_tac 2);
(*Base*)
by (Blast_tac 1);
-(*Fake, OR2, OR4*)
-by (REPEAT (spy_analz_tac 1));
qed_spec_mp "analz_image_freshK";
@@ -365,16 +365,18 @@
by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
- addsimps [not_parts_not_analz, analz_insert_freshK]
+ addsimps [analz_insert_eq, not_parts_not_analz,
+ analz_insert_freshK]
setloop split_tac [expand_if])));
+(*Oops*)
+by (blast_tac (!claset addSDs [unique_session_keys]) 4);
+(*OR4*)
+by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset delrules [impCE]
- addSEs sees_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 3);
-(*OR4, OR2, Fake*)
-by (REPEAT_FIRST spy_analz_tac);
-(*Oops*) (** LEVEL 5 **)
-by (blast_tac (!claset addSDs [unique_session_keys]) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Jun 19 11:31:14 1997 +0200
@@ -179,10 +179,9 @@
by analz_sees_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
-(*14 seconds*)
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
-(*OR4, Fake*)
-by (EVERY (map spy_analz_tac [3,2]));
+(*Fake*)
+by (spy_analz_tac 2);
(*Base*)
by (Blast_tac 1);
qed_spec_mp "analz_image_freshK";
@@ -285,16 +284,18 @@
by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
- addsimps [not_parts_not_analz,
- analz_insert_freshK]
+ addsimps [analz_insert_eq, not_parts_not_analz,
+ analz_insert_freshK]
setloop split_tac [expand_if])));
+(*Oops*)
+by (blast_tac (!claset addSDs [unique_session_keys]) 4);
+(*OR4*)
+by (Blast_tac 3);
(*OR3*)
by (blast_tac (!claset addSEs sees_Spy_partsEs
addIs [impOfSubs analz_subset_parts]) 2);
-(*Oops*)
-by (blast_tac (!claset addDs [unique_session_keys]) 3);
-(*OR4, Fake*)
-by (REPEAT_FIRST spy_analz_tac);
+(*Fake*)
+by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Jun 19 11:31:14 1997 +0200
@@ -181,10 +181,10 @@
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Fake*)
+by (spy_analz_tac 2);
(*Base*)
by (Blast_tac 1);
-(*Fake, OR2, OR4*)
-by (REPEAT (spy_analz_tac 1));
qed_spec_mp "analz_image_freshK";
@@ -238,16 +238,18 @@
by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
- addsimps [not_parts_not_analz, analz_insert_freshK]
+ addsimps [analz_insert_eq, not_parts_not_analz,
+ analz_insert_freshK]
setloop split_tac [expand_if])));
+(*Oops*)
+by (blast_tac (!claset addSDs [unique_session_keys]) 4);
+(*OR4*)
+by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset delrules [impCE]
- addSEs sees_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 3);
-(*OR4, OR2, Fake*)
-by (REPEAT_FIRST spy_analz_tac);
-(*Oops*) (** LEVEL 5 **)
-by (blast_tac (!claset addSDs [unique_session_keys]) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
--- a/src/HOL/Auth/Recur.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Thu Jun 19 11:31:14 1997 +0200
@@ -268,8 +268,8 @@
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
(*Base*)
by (Blast_tac 1);
-(*RA4, RA2, Fake*)
-by (REPEAT (spy_analz_tac 1));
+(*Fake*)
+by (spy_analz_tac 1);
val raw_analz_image_freshK = result();
qed_spec_mp "analz_image_freshK";
--- a/src/HOL/Auth/Shared.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Thu Jun 19 11:31:14 1997 +0200
@@ -388,10 +388,14 @@
by (Blast_tac 1);
qed "insert_Key_image";
+(*Reverse the normal simplification of "image" to build up (not break down)
+ the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to
+ erase occurrences of forwarded message components (X).*)
val analz_image_freshK_ss =
!simpset delsimps [image_insert, image_Un]
- addsimps ([image_insert RS sym, image_Un RS sym,
- Key_not_used,
+ addsimps ([analz_insert_eq, Key_not_used,
+ impOfSubs (Un_upper2 RS analz_mono),
+ image_insert RS sym, image_Un RS sym,
insert_Key_singleton, subset_Compl_range,
insert_Key_image, Un_assoc RS sym]
@disj_comms)
--- a/src/Provers/blast.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/Provers/blast.ML Thu Jun 19 11:31:14 1997 +0200
@@ -1112,8 +1112,7 @@
| cell => Sequence.seqof(fn()=> cell))
in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
end
- handle Subscript => Sequence.null
- | PROVE => Sequence.null);
+ handle PROVE => Sequence.null);
fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0);