# HG changeset patch
# User paulson
# Date 866712277 -7200
# Node ID 6b17f82bbf01a2615a4b18b1701c27f6f9147e8d
# Parent  8a79e27ac53b039f28f2f978fd1283bcbc421e8c
New comments; a tidied proof

diff -r 8a79e27ac53b -r 6b17f82bbf01 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Jun 19 11:23:31 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Jun 19 11:24:37 1997 +0200
@@ -405,8 +405,7 @@
 by (Auto_tac());
 by (eres_inst_tac [("za","x")] analz.induct 1);
 by (Auto_tac());
-by (blast_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
-                             analz.Decrypt]) 1);
+by (blast_tac (!claset addIs [analz_insertI, analz.Decrypt]) 1);
 val lemma2 = result();
 
 goal thy "!!H. Key (invKey K) : analz H ==>  \
@@ -477,6 +476,9 @@
    "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H"
 *)
 
+(*This rewrite rule helps in the simplification of messages that involve
+  the forwarding of unknown components (X).  Without it, removing occurrences
+  of X can be very complicated. *)
 goal thy "!!H. X: analz H ==> analz (insert X H) = analz H";
 by (blast_tac (!claset addIs [analz_cut, analz_insertI]) 1);
 qed "analz_insert_eq";
@@ -839,7 +841,8 @@
                   impOfSubs Fake_parts_insert] THEN'
     eresolve_tac [asm_rl, synth.Inj];
 
-(*Analysis of Fake cases and of messages that forward unknown parts.
+(*Analysis of Fake cases.  Also works for messages that forward unknown parts,
+  but this application is no longer necessary if analz_insert_eq is used.
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 fun spy_analz_tac i =