Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Yahalom_Bad.thy
changeset 14200 d8598e24f8fa
parent 13956 8fe7e12290e1
child 14207 f20fbb141673 
--- a/src/HOL/Auth/Yahalom_Bad.thy	Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Tue Sep 23 15:41:33 2003 +0200
@@ -70,15 +70,16 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-lemma "A \<noteq> Server
-      ==> \<exists>X NB K. \<exists>evs \<in> yahalom.
-             Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
+       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
+              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] yahalom.Nil
                     [THEN yahalom.YM1, THEN yahalom.Reception,
                      THEN yahalom.YM2, THEN yahalom.Reception,
                      THEN yahalom.YM3, THEN yahalom.Reception,
-                     THEN yahalom.YM4], possibility)
+                     THEN yahalom.YM4])
+apply (possibility, simp add: used_Cons) 
 done
 
 lemma Gets_imp_Says:
isabelle