Moved some declarations to Message from Public and Shared
authorpaulson
Fri Jul 11 13:28:53 1997 +0200 (1997-07-11)
changeset 3514eb16b8e8d872
parent 3513 4d4f8c18255e
child 3515 d8a71f6eaf40
Moved some declarations to Message from Public and Shared
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Jul 11 13:27:15 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Jul 11 13:28:53 1997 +0200
     1.3 @@ -11,6 +11,13 @@
     1.4  
     1.5  AddIffs (msg.inject);
     1.6  
     1.7 +(*Holds because Friend is injective: thus cannot prove for all f*)
     1.8 +goal thy "(Friend x : Friend``A) = (x:A)";
     1.9 +by (Auto_tac());
    1.10 +qed "Friend_image_eq";
    1.11 +Addsimps [Friend_image_eq];
    1.12 +
    1.13 +
    1.14  (** Inverse of keys **)
    1.15  
    1.16  goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
    1.17 @@ -73,6 +80,11 @@
    1.18  AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
    1.19  	keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
    1.20  
    1.21 +goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    1.22 +by (Auto_tac ());
    1.23 +qed "keysFor_image_Key";
    1.24 +Addsimps [keysFor_image_Key];
    1.25 +
    1.26  goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    1.27  by (Blast_tac 1);
    1.28  qed "Crypt_imp_invKey_keysFor";
    1.29 @@ -272,8 +284,19 @@
    1.30  by (etac parts.induct 1);
    1.31  by (Auto_tac());
    1.32  qed "parts_image_Key";
    1.33 +Addsimps [parts_image_Key];
    1.34  
    1.35 -Addsimps [parts_image_Key];
    1.36 +
    1.37 +(*In any message, there is an upper bound N on its greatest nonce.*)
    1.38 +goal thy "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
    1.39 +by (msg.induct_tac "msg" 1);
    1.40 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
    1.41 +(*MPair case: blast_tac works out the necessary sum itself!*)
    1.42 +by (blast_tac (!claset addSEs [add_leE]) 2);
    1.43 +(*Nonce case*)
    1.44 +by (res_inst_tac [("x","N + Suc nat")] exI 1);
    1.45 +by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
    1.46 +qed "msg_Nonce_supply";
    1.47  
    1.48  
    1.49  (**** Inductive relation "analz" ****)
    1.50 @@ -884,3 +907,10 @@
    1.51  by (Blast_tac 1);
    1.52  val Un_absorb3 = result();
    1.53  Addsimps [Un_absorb3];
    1.54 +
    1.55 +Addsimps [Un_insert_left, Un_insert_right];
    1.56 +
    1.57 +(*By default only o_apply is built-in.  But in the presence of eta-expansion
    1.58 +  this means that some terms displayed as (f o g) will be rewritten, and others
    1.59 +  will not!*)
    1.60 +Addsimps [o_def];