src/HOL/Auth/Message.thy
changeset 11192 5fd02b905a9a
parent 11189 1ea763a5d186
child 11230 756c5034f08b
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 02 13:26:55 2001 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Mar 05 12:31:31 2001 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  files ("Message_lemmas.ML"):
     1.5  
     1.6  (*Eliminates a commonly-occurring expression*)
     1.7 -lemma [simp] : "~ (ALL x. x~=y)"
     1.8 +lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
     1.9  by blast
    1.10  
    1.11  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.12 @@ -66,17 +66,17 @@
    1.13  
    1.14    (*Keys useful to decrypt elements of a message set*)
    1.15    keysFor :: "msg set => key set"
    1.16 -  "keysFor H == invKey ` {K. EX X. Crypt K X : H}"
    1.17 +  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    1.18  
    1.19  (** Inductive definition of all "parts" of a message.  **)
    1.20  
    1.21  consts  parts   :: "msg set => msg set"
    1.22  inductive "parts H"
    1.23    intros 
    1.24 -    Inj [intro]          : "X: H  ==> X : parts H"
    1.25 -    Fst:     "{|X,Y|}   : parts H ==> X : parts H"
    1.26 -    Snd:     "{|X,Y|}   : parts H ==> Y : parts H"
    1.27 -    Body:    "Crypt K X : parts H ==> X : parts H"
    1.28 +    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    1.29 +    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    1.30 +    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    1.31 +    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    1.32  
    1.33  
    1.34  (*Monotonicity*)
    1.35 @@ -94,11 +94,11 @@
    1.36  consts  analz   :: "msg set => msg set"
    1.37  inductive "analz H"
    1.38    intros 
    1.39 -    Inj [intro,simp] :    "X: H ==> X: analz H"
    1.40 -    Fst:     "{|X,Y|} : analz H ==> X : analz H"
    1.41 -    Snd:     "{|X,Y|} : analz H ==> Y : analz H"
    1.42 +    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
    1.43 +    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    1.44 +    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    1.45      Decrypt [dest]: 
    1.46 -             "[|Crypt K X : analz H; Key(invKey K): analz H|] ==> X : analz H"
    1.47 +             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
    1.48  
    1.49  
    1.50  (*Monotonicity; Lemma 1 of Lowe's paper*)
    1.51 @@ -116,12 +116,12 @@
    1.52  consts  synth   :: "msg set => msg set"
    1.53  inductive "synth H"
    1.54    intros 
    1.55 -    Inj    [intro]:   "X: H ==> X: synth H"
    1.56 -    Agent  [intro]:   "Agent agt : synth H"
    1.57 -    Number [intro]:   "Number n  : synth H"
    1.58 -    Hash   [intro]:   "X: synth H ==> Hash X : synth H"
    1.59 -    MPair  [intro]:   "[|X: synth H;  Y: synth H|] ==> {|X,Y|} : synth H"
    1.60 -    Crypt  [intro]:   "[|X: synth H;  Key(K) : H|] ==> Crypt K X : synth H"
    1.61 +    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
    1.62 +    Agent  [intro]:   "Agent agt \<in> synth H"
    1.63 +    Number [intro]:   "Number n  \<in> synth H"
    1.64 +    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
    1.65 +    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    1.66 +    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    1.67  
    1.68  (*Monotonicity*)
    1.69  lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
    1.70 @@ -131,11 +131,11 @@
    1.71  done
    1.72  
    1.73  (*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
    1.74 -inductive_cases Nonce_synth [elim!]: "Nonce n : synth H"
    1.75 -inductive_cases Key_synth   [elim!]: "Key K : synth H"
    1.76 -inductive_cases Hash_synth  [elim!]: "Hash X : synth H"
    1.77 -inductive_cases MPair_synth [elim!]: "{|X,Y|} : synth H"
    1.78 -inductive_cases Crypt_synth [elim!]: "Crypt K X : synth H"
    1.79 +inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
    1.80 +inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
    1.81 +inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
    1.82 +inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
    1.83 +inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
    1.84  
    1.85  use "Message_lemmas.ML"
    1.86