tweaked proofs to handle new freeness reasoning for data c onstructors
authorpaulson
Wed Jul 21 15:22:11 1999 +0200 (1999-07-21)
changeset 7057b9ddbb925939
parent 7056 522a7013d7df
child 7058 8dfea70eb6b7
tweaked proofs to handle new freeness reasoning for data c onstructors
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
src/HOL/Auth/Recur.ML
src/HOL/Auth/TLS.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Wed Jul 21 15:20:26 1999 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Wed Jul 21 15:22:11 1999 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  by (Blast_tac 1);
     1.5  Addsimps [result()];
     1.6  
     1.7 -AddIffs atomic.inject;
     1.8  AddIffs msg.inject;
     1.9  
    1.10  (*Equations hold because constructors are injective; cannot prove for all f*)
    1.11 @@ -63,27 +62,27 @@
    1.12  qed "keysFor_mono";
    1.13  
    1.14  Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    1.15 -by (Blast_tac 1);
    1.16 +by Auto_tac;
    1.17  qed "keysFor_insert_Agent";
    1.18  
    1.19  Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    1.20 -by (Blast_tac 1);
    1.21 +by Auto_tac;
    1.22  qed "keysFor_insert_Nonce";
    1.23  
    1.24  Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
    1.25 -by (Blast_tac 1);
    1.26 +by Auto_tac;
    1.27  qed "keysFor_insert_Number";
    1.28  
    1.29  Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    1.30 -by (Blast_tac 1);
    1.31 +by Auto_tac;
    1.32  qed "keysFor_insert_Key";
    1.33  
    1.34  Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    1.35 -by (Blast_tac 1);
    1.36 +by Auto_tac;
    1.37  qed "keysFor_insert_Hash";
    1.38  
    1.39  Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    1.40 -by (Blast_tac 1);
    1.41 +by Auto_tac;
    1.42  qed "keysFor_insert_MPair";
    1.43  
    1.44  Goalw [keysFor_def]
    1.45 @@ -250,7 +249,7 @@
    1.46  fun parts_tac i =
    1.47    EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
    1.48           etac parts.induct i,
    1.49 -         REPEAT (Blast_tac i)];
    1.50 +         Auto_tac];
    1.51  
    1.52  Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
    1.53  by (parts_tac 1);
    1.54 @@ -308,7 +307,6 @@
    1.55  (*In any message, there is an upper bound N on its greatest nonce.*)
    1.56  Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
    1.57  by (induct_tac "msg" 1);
    1.58 -by (induct_tac "atomic" 1);
    1.59  by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
    1.60  (*MPair case: blast_tac works out the necessary sum itself!*)
    1.61  by (blast_tac (claset() addSEs [add_leE]) 2);
    1.62 @@ -395,7 +393,7 @@
    1.63  fun analz_tac i =
    1.64    EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
    1.65           etac analz.induct i,
    1.66 -         REPEAT (Blast_tac i)];
    1.67 +         Auto_tac];
    1.68  
    1.69  Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
    1.70  by (analz_tac 1);
    1.71 @@ -442,7 +440,7 @@
    1.72  \              insert (Crypt K X) (analz (insert X H))";
    1.73  by (rtac subsetI 1);
    1.74  by (eres_inst_tac [("xa","x")] analz.induct 1);
    1.75 -by (ALLGOALS (Blast_tac));
    1.76 +by Auto_tac;
    1.77  val lemma1 = result();
    1.78  
    1.79  Goal "Key (invKey K) : analz H ==>  \
     2.1 --- a/src/HOL/Auth/Message.thy	Wed Jul 21 15:20:26 1999 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Wed Jul 21 15:22:11 1999 +0200
     2.3 @@ -28,36 +28,15 @@
     2.4  datatype  (*We allow any number of friendly agents*)
     2.5    agent = Server | Friend nat | Spy
     2.6  
     2.7 -
     2.8 -(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
     2.9 -  expressed using natural numbers.*)
    2.10 -datatype  
    2.11 -  atomic = AGENT  agent	(*Agent names*)
    2.12 -         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
    2.13 -         | NONCE  nat   (*Unguessable nonces*)
    2.14 -         | KEY    key   (*Crypto keys*)
    2.15 -
    2.16  datatype
    2.17 -     msg = Atomic atomic
    2.18 +     msg = Agent  agent	    (*Agent names*)
    2.19 +         | Number nat       (*Ordinary integers, timestamps, ...*)
    2.20 +         | Nonce  nat       (*Unguessable nonces*)
    2.21 +         | Key    key       (*Crypto keys*)
    2.22  	 | Hash   msg       (*Hashing*)
    2.23  	 | MPair  msg msg   (*Compound messages*)
    2.24  	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    2.25  
    2.26 -(*These translations complete the illustion that "msg" has seven constructors*)
    2.27 -syntax
    2.28 -  Agent       :: agent => msg
    2.29 -  Number      :: nat   => msg
    2.30 -  Nonce       :: nat   => msg
    2.31 -  Key         :: key   => msg
    2.32 -
    2.33 -translations
    2.34 -  "Agent x"   == "Atomic (AGENT x)"
    2.35 -  "Number x"  == "Atomic (NUMBER x)"
    2.36 -  "Nonce x"   == "Atomic (NONCE x)"
    2.37 -  "Nonce``x"  == "Atomic `` (NONCE `` x)"
    2.38 -  "Key x"     == "Atomic (KEY x)"
    2.39 -  "Key``x"    == "Atomic `` (KEY `` x)"
    2.40 -
    2.41  
    2.42  (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    2.43  syntax
     3.1 --- a/src/HOL/Auth/Recur.ML	Wed Jul 21 15:20:26 1999 +0200
     3.2 +++ b/src/HOL/Auth/Recur.ML	Wed Jul 21 15:22:11 1999 +0200
     3.3 @@ -368,8 +368,8 @@
     3.4  by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
     3.5  by (ALLGOALS Clarify_tac);
     3.6  by (blast_tac (claset() addSDs  [resp_analz_insert]
     3.7 - 		        addIs  [impOfSubs analz_subset_parts]) 2);
     3.8 -by (blast_tac (claset() addSDs [respond_certificate]) 1);
     3.9 + 		        addIs  [impOfSubs analz_subset_parts]) 3);
    3.10 +by (blast_tac (claset() addSDs [respond_certificate]) 2);
    3.11  by (Asm_full_simp_tac 1);
    3.12  (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
    3.13  by (blast_tac
    3.14 @@ -395,7 +395,7 @@
    3.15  (*Fake*)
    3.16  by (spy_analz_tac 2);
    3.17  (*Base*)
    3.18 -by (Blast_tac 1);
    3.19 +by (Force_tac 1);
    3.20  (*RA3 remains*)
    3.21  by (simp_tac (simpset() addsimps [parts_insert_spies]) 1);
    3.22  by (safe_tac (claset() delrules [impCE]));
     4.1 --- a/src/HOL/Auth/TLS.ML	Wed Jul 21 15:20:26 1999 +0200
     4.2 +++ b/src/HOL/Auth/TLS.ML	Wed Jul 21 15:22:11 1999 +0200
     4.3 @@ -410,10 +410,10 @@
     4.4  by (blast_tac (claset() addIs [parts_insertI]) 2);
     4.5  (** LEVEL 6 **)
     4.6  (*Oops*)
     4.7 -by (Force_tac 6);
     4.8  by (REPEAT 
     4.9 -    (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
    4.10 -				 Notes_master_imp_Crypt_PMS]) 1));
    4.11 +    (force_tac (claset() addSDs [Notes_Crypt_parts_spies, 
    4.12 +				 Notes_master_imp_Crypt_PMS],
    4.13 +		simpset()) 1));
    4.14  val lemma = result();
    4.15  
    4.16  Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \