1.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -605,7 +605,7 @@
     1.4             \<in> set evs;   
     1.5           evs \<in> sr \<rbrakk> \<Longrightarrow> A=A'"
     1.6  apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
     1.7 -apply (fastsimp dest: Outpts_parts_used)
     1.8 +apply (fastforce dest: Outpts_parts_used)
     1.9  apply blast
    1.10  done
    1.11  
    1.12 @@ -615,7 +615,7 @@
    1.13           Outpts (Card B') B' \<lbrace>Nonce Nb, Key SK', Cert1', Cert2'\<rbrace> \<in> set evs;   
    1.14           evs \<in> sr \<rbrakk> \<Longrightarrow> B=B' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
    1.15  apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
    1.16 -apply (fastsimp dest: Outpts_parts_used)
    1.17 +apply (fastforce dest: Outpts_parts_used)
    1.18  apply blast
    1.19  done
    1.20  
    1.21 @@ -626,7 +626,7 @@
    1.22           Outpts (Card B') B' \<lbrace>Nonce Nb', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs;   
    1.23           evs \<in> sr \<rbrakk> \<Longrightarrow> B=B' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
    1.24  apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
    1.25 -apply (fastsimp dest: Outpts_parts_used)
    1.26 +apply (fastforce dest: Outpts_parts_used)
    1.27  apply blast
    1.28  done
    1.29  
    1.30 @@ -644,9 +644,9 @@
    1.31    "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>  
    1.32       \<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs"
    1.33  apply (erule rev_mp, erule sr.induct, simp_all add: Unique_def)
    1.34 -apply (fastsimp dest: Outpts_parts_used)
    1.35 +apply (fastforce dest: Outpts_parts_used)
    1.36  apply blast
    1.37 -apply (fastsimp dest: Outpts_parts_used)
    1.38 +apply (fastforce dest: Outpts_parts_used)
    1.39  apply blast
    1.40  done
    1.41  
    1.42 @@ -699,7 +699,7 @@
    1.43           evs \<in> sr \<rbrakk>     
    1.44       \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
    1.45  apply (case_tac "A = Spy")
    1.46 -apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
    1.47 +apply (fastforce dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
    1.48  apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
    1.49  done
    1.50  
    1.51 @@ -977,7 +977,7 @@
    1.52  (*fake*)
    1.53  apply spy_analz
    1.54  (*forge*)
    1.55 -apply (fastsimp dest: analz.Inj)
    1.56 +apply (fastforce dest: analz.Inj)
    1.57  (*SR7: used B\<noteq>Spy*)
    1.58  (*SR7F*)
    1.59  apply clarify
    1.60 @@ -1028,7 +1028,7 @@
    1.61  (*Forge*)
    1.62  apply (rotate_tac 7)
    1.63  apply (drule parts.Inj)
    1.64 -apply (fastsimp dest: Outpts_B_Card_form_7)
    1.65 +apply (fastforce dest: Outpts_B_Card_form_7)
    1.66  (*SR7*)
    1.67  apply (blast dest!: Outpts_B_Card_form_7)
    1.68  (*SR7F*)
    1.69 @@ -1036,10 +1036,10 @@
    1.70  apply (drule Outpts_parts_used)
    1.71  apply simp
    1.72  (*faster than
    1.73 -  apply (fastsimp dest: Outpts_parts_used)
    1.74 +  apply (fastforce dest: Outpts_parts_used)
    1.75  *)
    1.76  (*SR10*)
    1.77 -apply (fastsimp dest: Outpts_B_Card_form_7)
    1.78 +apply (fastforce dest: Outpts_B_Card_form_7)
    1.79  (*SR10F - uses assumption Card A not cloned*)
    1.80  apply clarify
    1.81  apply (drule Outpts_B_Card_form_7, assumption)
    1.82 @@ -1346,7 +1346,7 @@
    1.83            Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Cert2\<rbrace> \<in> set evs"
    1.84  apply (erule rev_mp)
    1.85  apply (erule sr.induct)
    1.86 -prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10)
    1.87 +prefer 18 apply (fastforce dest: Outpts_A_Card_form_10)
    1.88  apply auto
    1.89  done
    1.90