src/HOL/SET-Protocol/MessageSET.thy
changeset 23755 1c4672d130b1
parent 22843 189e214845dd
child 24123 a0fc58900606
     1.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -100,13 +100,14 @@
     1.4  
     1.5  subsubsection{*Inductive definition of all "parts" of a message.*}
     1.6  
     1.7 -consts  parts   :: "msg set => msg set"
     1.8 -inductive "parts H"
     1.9 -  intros
    1.10 +inductive_set
    1.11 +  parts :: "msg set => msg set"
    1.12 +  for H :: "msg set"
    1.13 +  where
    1.14      Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    1.15 -    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    1.16 -    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    1.17 -    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    1.18 +  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    1.19 +  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    1.20 +  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    1.21  
    1.22  
    1.23  (*Monotonicity*)
    1.24 @@ -391,13 +392,14 @@
    1.25      messages, including keys.  A form of downward closure.  Pairs can
    1.26      be taken apart; messages decrypted with known keys.*}
    1.27  
    1.28 -consts  analz   :: "msg set => msg set"
    1.29 -inductive "analz H"
    1.30 -  intros
    1.31 +inductive_set
    1.32 +  analz :: "msg set => msg set"
    1.33 +  for H :: "msg set"
    1.34 +  where
    1.35      Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
    1.36 -    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    1.37 -    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    1.38 -    Decrypt [dest]:
    1.39 +  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    1.40 +  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    1.41 +  | Decrypt [dest]:
    1.42               "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
    1.43  
    1.44  
    1.45 @@ -521,14 +523,14 @@
    1.46                 analz (insert (Crypt K X) H) \<subseteq>
    1.47                 insert (Crypt K X) (analz (insert X H))"
    1.48  apply (rule subsetI)
    1.49 -apply (erule_tac xa = x in analz.induct, auto)
    1.50 +apply (erule_tac x = x in analz.induct, auto)
    1.51  done
    1.52  
    1.53  lemma lemma2: "Key (invKey K) \<in> analz H ==>
    1.54                 insert (Crypt K X) (analz (insert X H)) \<subseteq>
    1.55                 analz (insert (Crypt K X) H)"
    1.56  apply auto
    1.57 -apply (erule_tac xa = x in analz.induct, auto)
    1.58 +apply (erule_tac x = x in analz.induct, auto)
    1.59  apply (blast intro: analz_insertI analz.Decrypt)
    1.60  done
    1.61  
    1.62 @@ -639,15 +641,16 @@
    1.63      encrypted with known keys.  Agent names are public domain.
    1.64      Numbers can be guessed, but Nonces cannot be.*}
    1.65  
    1.66 -consts  synth   :: "msg set => msg set"
    1.67 -inductive "synth H"
    1.68 -  intros
    1.69 +inductive_set
    1.70 +  synth :: "msg set => msg set"
    1.71 +  for H :: "msg set"
    1.72 +  where
    1.73      Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
    1.74 -    Agent  [intro]:   "Agent agt \<in> synth H"
    1.75 -    Number [intro]:   "Number n  \<in> synth H"
    1.76 -    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
    1.77 -    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    1.78 -    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    1.79 +  | Agent  [intro]:   "Agent agt \<in> synth H"
    1.80 +  | Number [intro]:   "Number n  \<in> synth H"
    1.81 +  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
    1.82 +  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    1.83 +  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    1.84  
    1.85  (*Monotonicity*)
    1.86  lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"