# HG changeset patch
# User bulwahn
# Date 1284047891 -7200
# Node ID 1ff57c8ea8f90d8c932346ee9f334f4ecee0ef80
# Parent  432ed333294c8603bd7f24ebeafb08ba8a93f173# Parent  8756b44582e2d95f6f62a320fa3ebf69e58fb475
merged

diff -r 432ed333294c -r 1ff57c8ea8f9 src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu Sep 09 17:58:11 2010 +0200
@@ -171,21 +171,21 @@
 
 
 text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
 apply auto
 done
 
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
 apply auto
 done
 
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
diff -r 432ed333294c -r 1ff57c8ea8f9 src/HOL/Auth/Kerberos_BAN_Gets.thy
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Sep 09 17:58:11 2010 +0200
@@ -157,10 +157,7 @@
 
 lemma Gets_imp_knows:
      "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
-apply (case_tac "B = Spy")
-apply (blast dest!: Gets_imp_knows_Spy)
-apply (blast dest!: Gets_imp_knows_agents)
-done
+by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
 
 lemma Gets_imp_knows_analz:
     "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk>  \<Longrightarrow> X \<in> analz (knows B evs)"
@@ -168,21 +165,21 @@
 done
 
 text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
 apply auto
 done
 
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
 apply auto
 done
 
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
diff -r 432ed333294c -r 1ff57c8ea8f9 src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Thu Sep 09 17:58:11 2010 +0200
@@ -104,11 +104,7 @@
 
 lemma Gets_imp_knows:
      "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
-apply (case_tac "B = Spy")
-apply (blast dest!: Gets_imp_knows_Spy)
-apply (blast dest!: Gets_imp_knows_agents)
-done
-
+by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
 
 lemma OR2_analz_knows_Spy: 
    "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>   
@@ -218,15 +214,8 @@
     evs \<in> orb\<rbrakk>                                              
  \<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))    
              | X \<in> analz (knows Spy evs)"
-apply (case_tac "B \<in> bad")
-apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, 
-                                 THEN analz.Decrypt, THEN analz.Fst])
-prefer 3 apply blast
-prefer 3 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN 
-                                                 parts.Snd, THEN B_trusts_OR3]
-                             Says_Server_message_form)
-apply simp_all                                    
-done
+by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
+          Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)
 
 lemma unique_Na: "\<lbrakk>Says A B  \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
          Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs;  
@@ -240,7 +229,7 @@
 
 lemma analz_image_freshCryptK_lemma:
 "(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>  
-        (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)";
+        (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 ML
@@ -376,8 +365,6 @@
 apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
 apply (drule analz_hard, assumption, assumption, assumption, assumption)
 apply (drule OR4_imp_Gets, assumption, assumption)
-apply (erule exE)
-(*blast doesn't do because it can't infer that Key (shrK P) \<in> (knows P evs)*)
 apply (fastsimp dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
 done
 
diff -r 432ed333294c -r 1ff57c8ea8f9 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/Public.thy	Thu Sep 09 17:58:11 2010 +0200
@@ -235,12 +235,10 @@
      "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
 apply (induct evs) 
  prefer 2
- apply (simp add: used_Cons)
- apply (rule ballI)  
- apply (case_tac a, auto)  
-apply (auto dest!: parts_cut) 
+ apply (simp add: used_Cons split: event.split)
+ apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
 txt{*Base case*}
-apply (simp add: used_Nil) 
+apply (auto dest!: parts_cut simp add: used_Nil) 
 done
 
 lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"