# HG changeset patch
# User paulson
# Date 1250180382 -3600
# Node ID a508148f7c254c4c22d2701ded14fd4504a0cc34
# Parent  b269b56b6a145144906ab9c4b19d8a30c610a978
 Removal of redundant settings of unification trace and search bounds.

diff -r b269b56b6a14 -r a508148f7c25 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Thu Aug 13 17:19:10 2009 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Thu Aug 13 17:19:42 2009 +0100
@@ -129,8 +129,7 @@
 lemma YM4_Key_parts_knows_Spy:
      "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
       ==> K \<in> parts (knows Spy evs)"
-by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj])
-
+  by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)
 
 text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
 that NOBODY sends messages containing X! *}
@@ -275,7 +274,7 @@
          Notes Spy {|na, nb, Key K|} \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
+  by (metis A_trusts_YM3 secrecy_lemma)
 
 
 subsubsection{* Security Guarantees for B upon receiving YM4 *}
@@ -409,9 +408,8 @@
 txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
   @{prop "NBa \<noteq> NB"}.  Previous two steps make the next step
   faster.*}
-apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
-         dest: analz.Inj
-           parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
+apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
+      Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
 done
 
 
@@ -514,12 +512,7 @@
   covered by the quantified Oops assumption.*}
 apply (clarify, simp add: all_conj_distrib)
 apply (frule Says_Server_imp_YM2, assumption)
-apply (case_tac "NB = NBa")
-txt{*If NB=NBa then all other components of the Oops message agree*}
-apply (blast dest: Says_unique_NB)
-txt{*case @{prop "NB \<noteq> NBa"}*}
-apply (simp add: single_Nonce_secrecy)
-apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
+apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
 done
 
 
@@ -557,7 +550,7 @@
          \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
+  by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
 
 
 subsection{*Authenticating B to A*}
@@ -594,7 +587,8 @@
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
        \<in> set evs"
-by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
+  by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
+         not_parts_not_analz)
 
 
 subsection{*Authenticating A to B using the certificate 
@@ -639,7 +633,6 @@
          (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
-by (blast intro!: A_Said_YM3_lemma
-          dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
-
+atp_minimize [atp=spass] A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz
+by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
 end
diff -r b269b56b6a14 -r a508148f7c25 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:10 2009 +0100
+++ b/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:42 2009 +0100
@@ -7,8 +7,6 @@
 
 theory Basis imports Main begin
 
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
 
 section "misc"
 
@@ -65,36 +63,36 @@
 by (auto intro: r_into_rtrancl rtrancl_trans)
 
 lemma triangle_lemma:
- "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk> 
- \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
+ "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r*; (a,y)\<in>r*\<rbrakk> 
+ \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
 proof -
   note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
   note converse_rtranclE = converse_rtranclE [consumes 1] 
   assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
-  assume "(a,x)\<in>r\<^sup>*" 
-  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
+  assume "(a,x)\<in>r*" 
+  then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
   proof (induct rule: converse_rtrancl_induct)
-    assume "(x,y)\<in>r\<^sup>*"
+    assume "(x,y)\<in>r*"
     then show ?thesis 
       by blast
   next
     fix a v
     assume a_v_r: "(a, v) \<in> r" and
-          v_x_rt: "(v, x) \<in> r\<^sup>*" and
-          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
-             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
+          v_x_rt: "(v, x) \<in> r*" and
+          a_y_rt: "(a, y) \<in> r*"  and
+             hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
     from a_y_rt 
-    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
+    show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
     proof (cases rule: converse_rtranclE)
       assume "a=y"
-      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
+      with a_v_r v_x_rt have "(y,x) \<in> r*"
 	by (auto intro: r_into_rtrancl rtrancl_trans)
       then show ?thesis 
 	by blast
     next
       fix w 
       assume a_w_r: "(a, w) \<in> r" and
-            w_y_rt: "(w, y) \<in> r\<^sup>*"
+            w_y_rt: "(w, y) \<in> r*"
       from a_v_r a_w_r unique 
       have "v=w" 
 	by auto
@@ -107,7 +105,7 @@
 
 
 lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
- "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ "\<lbrakk>(a,b)\<in>r*;  a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 apply (erule rtranclE)
 apply (auto dest: rtrancl_into_trancl1)
 done
diff -r b269b56b6a14 -r a508148f7c25 src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Thu Aug 13 17:19:10 2009 +0100
+++ b/src/HOL/Induct/Com.thy	Thu Aug 13 17:19:42 2009 +0100
@@ -91,8 +91,6 @@
   "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
   by (auto simp add: le_fun_def le_bool_def mem_def)
 
-declare [[unify_trace_bound = 30, unify_search_bound = 60]]
-
 text{*Command execution is functional (deterministic) provided evaluation is*}
 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
 apply (simp add: single_valued_def)
diff -r b269b56b6a14 -r a508148f7c25 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Aug 13 17:19:10 2009 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Aug 13 17:19:42 2009 +0100
@@ -183,8 +183,6 @@
   (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
 *}
 
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
 
 theorem eval_evals_exec_type_sound: 
 "wf_java_prog G ==>  
@@ -368,8 +366,6 @@
 
 done
 
-declare [[unify_search_bound = 20, unify_trace_bound = 20]]
-
 
 lemma eval_type_sound: "!!E s s'.  
   [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]