src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -72,13 +72,14 @@
 
 subsubsection{*Inductive Definition of All Parts" of a Message*}
 
-consts  parts   :: "msg set => msg set"
-inductive "parts H"
-  intros 
+inductive_set
+  parts :: "msg set => msg set"
+  for H :: "msg set"
+  where
     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
-    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
-    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
-    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
+  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
+  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
+  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
 text{*Monotonicity*}
@@ -335,13 +336,14 @@
     messages, including keys.  A form of downward closure.  Pairs can
     be taken apart; messages decrypted with known keys.  *}
 
-consts  analz   :: "msg set => msg set"
-inductive "analz H"
-  intros 
+inductive_set
+  analz :: "msg set => msg set"
+  for H :: "msg set"
+  where
     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
-    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
-    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
-    Decrypt [dest]: 
+  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+  | Decrypt [dest]: 
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
 
@@ -460,14 +462,14 @@
                analz (insert (Crypt K X) H) \<subseteq>  
                insert (Crypt K X) (analz (insert X H))"
 apply (rule subsetI)
-apply (erule_tac xa = x in analz.induct, auto)
+apply (erule_tac x = x in analz.induct, auto)
 done
 
 lemma lemma2: "Key (invKey K) \<in> analz H ==>   
                insert (Crypt K X) (analz (insert X H)) \<subseteq>  
                analz (insert (Crypt K X) H)"
 apply auto
-apply (erule_tac xa = x in analz.induct, auto)
+apply (erule_tac x = x in analz.induct, auto)
 apply (blast intro: analz_insertI analz.Decrypt)
 done
 
@@ -579,15 +581,16 @@
     encrypted with known keys.  Agent names are public domain.
     Numbers can be guessed, but Nonces cannot be.  *}
 
-consts  synth   :: "msg set => msg set"
-inductive "synth H"
-  intros 
+inductive_set
+  synth :: "msg set => msg set"
+  for H :: "msg set"
+  where
     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
-    Agent  [intro]:   "Agent agt \<in> synth H"
-    Number [intro]:   "Number n  \<in> synth H"
-    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
-    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
-    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+  | Agent  [intro]:   "Agent agt \<in> synth H"
+  | Number [intro]:   "Number n  \<in> synth H"
+  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
+  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 text{*Monotonicity*}
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"