src/HOL/Auth/Kerberos_BAN_Gets.thy

--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -63,24 +63,23 @@
       ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
 
 
-consts  bankerb_gets   :: "event list set"
-inductive "bankerb_gets"
- intros
+inductive_set bankerb_gets :: "event list set"
+ where
 
    Nil:  "[] \<in> bankerb_gets"
 
-   Fake: "\<lbrakk> evsf \<in> bankerb_gets;  X \<in> synth (analz (knows Spy evsf)) \<rbrakk>
+ | Fake: "\<lbrakk> evsf \<in> bankerb_gets;  X \<in> synth (analz (knows Spy evsf)) \<rbrakk>
 	  \<Longrightarrow> Says Spy B X # evsf \<in> bankerb_gets"
 
-   Reception: "\<lbrakk> evsr\<in> bankerb_gets; Says A B X \<in> set evsr \<rbrakk>
+ | Reception: "\<lbrakk> evsr\<in> bankerb_gets; Says A B X \<in> set evsr \<rbrakk>
                 \<Longrightarrow> Gets B X # evsr \<in> bankerb_gets"
 
-   BK1:  "\<lbrakk> evs1 \<in> bankerb_gets \<rbrakk>
+ | BK1:  "\<lbrakk> evs1 \<in> bankerb_gets \<rbrakk>
 	  \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1
 		\<in>  bankerb_gets"
 
 
-   BK2:  "\<lbrakk> evs2 \<in> bankerb_gets;  Key K \<notin> used evs2; K \<in> symKeys;
+ | BK2:  "\<lbrakk> evs2 \<in> bankerb_gets;  Key K \<notin> used evs2; K \<in> symKeys;
 	     Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk>
 	  \<Longrightarrow> Says Server A
 		(Crypt (shrK A)
@@ -89,7 +88,7 @@
 		# evs2 \<in> bankerb_gets"
 
 
-   BK3:  "\<lbrakk> evs3 \<in> bankerb_gets;
+ | BK3:  "\<lbrakk> evs3 \<in> bankerb_gets;
 	     Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
 	       \<in> set evs3;
 	     Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3;
@@ -98,7 +97,7 @@
 	       # evs3 \<in> bankerb_gets"
 
 
-   BK4:  "\<lbrakk> evs4 \<in> bankerb_gets;
+ | BK4:  "\<lbrakk> evs4 \<in> bankerb_gets;
 	     Gets B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>),
 			 (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4;
 	     \<not> expiredK Tk evs4;  \<not> expiredA Ta evs4 \<rbrakk>
@@ -106,7 +105,7 @@
 		\<in> bankerb_gets"
 
 	(*Old session keys may become compromised*)
-   Oops: "\<lbrakk> evso \<in> bankerb_gets;
+ | Oops: "\<lbrakk> evso \<in> bankerb_gets;
          Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
 	       \<in> set evso;
 	     expiredK Tk evso \<rbrakk>