# HG changeset patch
# User paulson
# Date 866712674 -7200
# Node ID d10f100676d85f941f0c11246fe888b2eb9f4692
# Parent  cd73bc206d87cb5c22d6da737fdf575558816ba3
Made proofs more concise by replacing calls to spy_analz_tac by uses of
analz_insert_eq in rewriting

diff -r cd73bc206d87 -r d10f100676d8 src/HOL/Auth/NS_Shared.ML
--- 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);
diff -r cd73bc206d87 -r d10f100676d8 src/HOL/Auth/OtwayRees.ML
--- 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 
diff -r cd73bc206d87 -r d10f100676d8 src/HOL/Auth/OtwayRees_AN.ML
--- 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 
diff -r cd73bc206d87 -r d10f100676d8 src/HOL/Auth/OtwayRees_Bad.ML
--- 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 
diff -r cd73bc206d87 -r d10f100676d8 src/HOL/Auth/Recur.ML
--- 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";
 
diff -r cd73bc206d87 -r d10f100676d8 src/HOL/Auth/Shared.ML
--- 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)
diff -r cd73bc206d87 -r d10f100676d8 src/Provers/blast.ML
--- 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);