# HG changeset patch
# User paulson
# Date 849174074 -3600
# Node ID f298678bd54a9b6d9ae1809d217d10b2107c6ef2
# Parent  c741309167bf29870f59fdda78d4bda0037b4ce6
Weaking of injectivity assumptions for newK and newN:
they are no longer assumed injective over all traces, merely over the
length of a trace

diff -r c741309167bf -r f298678bd54a src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -114,7 +114,8 @@
 \                length evs <= length evs' --> \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
-by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (ALLGOALS (fast_tac (!claset addEs [leD RS notE]
+				addDs [impOfSubs analz_subset_parts,
                                        impOfSubs parts_insert_subset_Un,
                                        Suc_leD]
                                 addss (!simpset))));
@@ -144,7 +145,8 @@
 by (REPEAT_FIRST
     (fast_tac (!claset addSEs partsEs
                        addSDs  [Says_imp_sees_Spy RS parts.Inj]
-                       addDs  [impOfSubs analz_subset_parts,
+                       addEs [leD RS notE]
+				addDs  [impOfSubs analz_subset_parts,
                                impOfSubs parts_insert_subset_Un, Suc_leD]
                        addss (!simpset))));
 qed_spec_mp "new_nonces_not_seen";
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -136,7 +136,8 @@
 \                length evs <= length evs' --> \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
+				    addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
@@ -165,7 +166,8 @@
 by (REPEAT_FIRST (fast_tac (!claset 
                               addSEs partsEs
                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
-                              addDs  [impOfSubs analz_subset_parts,
+                              addEs [leD RS notE]
+			      addDs  [impOfSubs analz_subset_parts,
                                       impOfSubs parts_insert_subset_Un,
                                       Suc_leD]
                               addss (!simpset))));
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -124,7 +124,8 @@
 \                length evs <= length evs' --> \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
+				    addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
@@ -135,7 +136,7 @@
 goal thy 
  "!!evs. [| Says A B X : set_of_list evs;  \
 \           Key (newK evt) : parts {X};    \
-\           evs : otway lost                 \
+\           evs : otway lost               \
 \        |] ==> length evt < length evs";
 by (rtac ccontr 1);
 by (dtac leI 1);
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -136,7 +136,8 @@
 \                length evs <= length evs' --> \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
+				    addDs [impOfSubs analz_subset_parts,
 					   impOfSubs parts_insert_subset_Un,
 					   Suc_leD]
                                 addss (!simpset))));
@@ -165,6 +166,7 @@
 by (REPEAT_FIRST
     (fast_tac (!claset addSEs partsEs
 	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
+		       addEs [leD RS notE]
 		       addDs  [impOfSubs analz_subset_parts,
 			       impOfSubs parts_insert_subset_Un, Suc_leD]
 		       addss (!simpset))));
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/Shared.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -56,7 +56,8 @@
 
 
 (*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
+AddIffs [inj_shrK RS inj_eq];
+AddSDs  [newN_length, newK_length];
 
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/Shared.thy	Thu Nov 28 10:41:14 1996 +0100
@@ -54,9 +54,9 @@
 rules
   inj_shrK      "inj shrK"
 
-  inj_newN      "inj newN"
+  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
+  newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
 
-  inj_newK      "inj newK"
   newK_neq_shrK "newK evs ~= shrK A" 
   isSym_newK    "isSymKey (newK evs)"
 
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -123,7 +123,8 @@
 \                length evs <= length evs' --> \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
+				    addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
diff -r c741309167bf -r f298678bd54a src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Thu Nov 28 10:41:14 1996 +0100
@@ -131,7 +131,8 @@
 \                length evs <= length evs' --> \
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
+				    addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));