tweaked proofs to handle new freeness reasoning for data c onstructors

--- a/src/HOL/Auth/Message.ML	Wed Jul 21 15:20:26 1999 +0200
+++ b/src/HOL/Auth/Message.ML	Wed Jul 21 15:22:11 1999 +0200
@@ -13,7 +13,6 @@
 by (Blast_tac 1);
 Addsimps [result()];
 
-AddIffs atomic.inject;
 AddIffs msg.inject;
 
 (*Equations hold because constructors are injective; cannot prove for all f*)
@@ -63,27 +62,27 @@
 qed "keysFor_mono";
 
 Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
-by (Blast_tac 1);
+by Auto_tac;
 qed "keysFor_insert_Agent";
 
 Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
-by (Blast_tac 1);
+by Auto_tac;
 qed "keysFor_insert_Nonce";
 
 Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
-by (Blast_tac 1);
+by Auto_tac;
 qed "keysFor_insert_Number";
 
 Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
-by (Blast_tac 1);
+by Auto_tac;
 qed "keysFor_insert_Key";
 
 Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
-by (Blast_tac 1);
+by Auto_tac;
 qed "keysFor_insert_Hash";
 
 Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
-by (Blast_tac 1);
+by Auto_tac;
 qed "keysFor_insert_MPair";
 
 Goalw [keysFor_def]
@@ -250,7 +249,7 @@
 fun parts_tac i =
   EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
          etac parts.induct i,
-         REPEAT (Blast_tac i)];
+         Auto_tac];
 
 Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
 by (parts_tac 1);
@@ -308,7 +307,6 @@
 (*In any message, there is an upper bound N on its greatest nonce.*)
 Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
 by (induct_tac "msg" 1);
-by (induct_tac "atomic" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
 (*MPair case: blast_tac works out the necessary sum itself!*)
 by (blast_tac (claset() addSEs [add_leE]) 2);
@@ -395,7 +393,7 @@
 fun analz_tac i =
   EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
          etac analz.induct i,
-         REPEAT (Blast_tac i)];
+         Auto_tac];
 
 Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
 by (analz_tac 1);
@@ -442,7 +440,7 @@
 \              insert (Crypt K X) (analz (insert X H))";
 by (rtac subsetI 1);
 by (eres_inst_tac [("xa","x")] analz.induct 1);
-by (ALLGOALS (Blast_tac));
+by Auto_tac;
 val lemma1 = result();
 
 Goal "Key (invKey K) : analz H ==>  \

--- a/src/HOL/Auth/Message.thy	Wed Jul 21 15:20:26 1999 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Jul 21 15:22:11 1999 +0200
@@ -28,36 +28,15 @@
 datatype  (*We allow any number of friendly agents*)
   agent = Server | Friend nat | Spy
 
-
-(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
-  expressed using natural numbers.*)
-datatype  
-  atomic = AGENT  agent	(*Agent names*)
-         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
-         | NONCE  nat   (*Unguessable nonces*)
-         | KEY    key   (*Crypto keys*)
-
 datatype
-     msg = Atomic atomic
+     msg = Agent  agent	    (*Agent names*)
+         | Number nat       (*Ordinary integers, timestamps, ...*)
+         | Nonce  nat       (*Unguessable nonces*)
+         | Key    key       (*Crypto keys*)
 	 | Hash   msg       (*Hashing*)
 	 | MPair  msg msg   (*Compound messages*)
 	 | Crypt  key msg   (*Encryption, public- or shared-key*)
 
-(*These translations complete the illustion that "msg" has seven constructors*)
-syntax
-  Agent       :: agent => msg
-  Number      :: nat   => msg
-  Nonce       :: nat   => msg
-  Key         :: key   => msg
-
-translations
-  "Agent x"   == "Atomic (AGENT x)"
-  "Number x"  == "Atomic (NUMBER x)"
-  "Nonce x"   == "Atomic (NONCE x)"
-  "Nonce``x"  == "Atomic `` (NONCE `` x)"
-  "Key x"     == "Atomic (KEY x)"
-  "Key``x"    == "Atomic `` (KEY `` x)"
-
 
 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
 syntax

--- a/src/HOL/Auth/Recur.ML	Wed Jul 21 15:20:26 1999 +0200
+++ b/src/HOL/Auth/Recur.ML	Wed Jul 21 15:22:11 1999 +0200
@@ -368,8 +368,8 @@
 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
 by (ALLGOALS Clarify_tac);
 by (blast_tac (claset() addSDs  [resp_analz_insert]
- 		        addIs  [impOfSubs analz_subset_parts]) 2);
-by (blast_tac (claset() addSDs [respond_certificate]) 1);
+ 		        addIs  [impOfSubs analz_subset_parts]) 3);
+by (blast_tac (claset() addSDs [respond_certificate]) 2);
 by (Asm_full_simp_tac 1);
 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
 by (blast_tac
@@ -395,7 +395,7 @@
 (*Fake*)
 by (spy_analz_tac 2);
 (*Base*)
-by (Blast_tac 1);
+by (Force_tac 1);
 (*RA3 remains*)
 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1);
 by (safe_tac (claset() delrules [impCE]));

--- a/src/HOL/Auth/TLS.ML	Wed Jul 21 15:20:26 1999 +0200
+++ b/src/HOL/Auth/TLS.ML	Wed Jul 21 15:22:11 1999 +0200
@@ -410,10 +410,10 @@
 by (blast_tac (claset() addIs [parts_insertI]) 2);
 (** LEVEL 6 **)
 (*Oops*)
-by (Force_tac 6);
 by (REPEAT 
-    (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
-				 Notes_master_imp_Crypt_PMS]) 1));
+    (force_tac (claset() addSDs [Notes_Crypt_parts_spies, 
+				 Notes_master_imp_Crypt_PMS],
+		simpset()) 1));
 val lemma = result();
 
 Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \