Removal of redundant settings of unification trace and search bounds.
authorpaulson
Thu Aug 13 17:19:42 2009 +0100 (2009-08-13)
changeset 32367a508148f7c25
parent 32366 b269b56b6a14
child 32368 37d87022cad3
Removal of redundant settings of unification trace and search bounds.
src/HOL/Auth/Yahalom.thy
src/HOL/Bali/Basis.thy
src/HOL/Induct/Com.thy
src/HOL/MicroJava/J/JTypeSafe.thy
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Aug 13 17:19:10 2009 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Aug 13 17:19:42 2009 +0100
     1.3 @@ -129,8 +129,7 @@
     1.4  lemma YM4_Key_parts_knows_Spy:
     1.5       "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
     1.6        ==> K \<in> parts (knows Spy evs)"
     1.7 -by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj])
     1.8 -
     1.9 +  by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)
    1.10  
    1.11  text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
    1.12  that NOBODY sends messages containing X! *}
    1.13 @@ -275,7 +274,7 @@
    1.14           Notes Spy {|na, nb, Key K|} \<notin> set evs;
    1.15           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
    1.16        ==> Key K \<notin> analz (knows Spy evs)"
    1.17 -by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
    1.18 +  by (metis A_trusts_YM3 secrecy_lemma)
    1.19  
    1.20  
    1.21  subsubsection{* Security Guarantees for B upon receiving YM4 *}
    1.22 @@ -409,9 +408,8 @@
    1.23  txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
    1.24    @{prop "NBa \<noteq> NB"}.  Previous two steps make the next step
    1.25    faster.*}
    1.26 -apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
    1.27 -         dest: analz.Inj
    1.28 -           parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
    1.29 +apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
    1.30 +      Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
    1.31  done
    1.32  
    1.33  
    1.34 @@ -514,12 +512,7 @@
    1.35    covered by the quantified Oops assumption.*}
    1.36  apply (clarify, simp add: all_conj_distrib)
    1.37  apply (frule Says_Server_imp_YM2, assumption)
    1.38 -apply (case_tac "NB = NBa")
    1.39 -txt{*If NB=NBa then all other components of the Oops message agree*}
    1.40 -apply (blast dest: Says_unique_NB)
    1.41 -txt{*case @{prop "NB \<noteq> NBa"}*}
    1.42 -apply (simp add: single_Nonce_secrecy)
    1.43 -apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
    1.44 +apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
    1.45  done
    1.46  
    1.47  
    1.48 @@ -557,7 +550,7 @@
    1.49           \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
    1.50           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
    1.51        ==> Key K \<notin> analz (knows Spy evs)"
    1.52 -by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
    1.53 +  by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
    1.54  
    1.55  
    1.56  subsection{*Authenticating B to A*}
    1.57 @@ -594,7 +587,8 @@
    1.58           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
    1.59        ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
    1.60         \<in> set evs"
    1.61 -by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
    1.62 +  by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
    1.63 +         not_parts_not_analz)
    1.64  
    1.65  
    1.66  subsection{*Authenticating A to B using the certificate 
    1.67 @@ -639,7 +633,6 @@
    1.68           (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
    1.69           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
    1.70        ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    1.71 -by (blast intro!: A_Said_YM3_lemma
    1.72 -          dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
    1.73 -
    1.74 +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
    1.75 +by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
    1.76  end
     2.1 --- a/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:10 2009 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:42 2009 +0100
     2.3 @@ -7,8 +7,6 @@
     2.4  
     2.5  theory Basis imports Main begin
     2.6  
     2.7 -declare [[unify_search_bound = 40, unify_trace_bound = 40]]
     2.8 -
     2.9  
    2.10  section "misc"
    2.11  
    2.12 @@ -65,36 +63,36 @@
    2.13  by (auto intro: r_into_rtrancl rtrancl_trans)
    2.14  
    2.15  lemma triangle_lemma:
    2.16 - "\<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> 
    2.17 - \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    2.18 + "\<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> 
    2.19 + \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
    2.20  proof -
    2.21    note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
    2.22    note converse_rtranclE = converse_rtranclE [consumes 1] 
    2.23    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
    2.24 -  assume "(a,x)\<in>r\<^sup>*" 
    2.25 -  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    2.26 +  assume "(a,x)\<in>r*" 
    2.27 +  then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
    2.28    proof (induct rule: converse_rtrancl_induct)
    2.29 -    assume "(x,y)\<in>r\<^sup>*"
    2.30 +    assume "(x,y)\<in>r*"
    2.31      then show ?thesis 
    2.32        by blast
    2.33    next
    2.34      fix a v
    2.35      assume a_v_r: "(a, v) \<in> r" and
    2.36 -          v_x_rt: "(v, x) \<in> r\<^sup>*" and
    2.37 -          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
    2.38 -             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
    2.39 +          v_x_rt: "(v, x) \<in> r*" and
    2.40 +          a_y_rt: "(a, y) \<in> r*"  and
    2.41 +             hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
    2.42      from a_y_rt 
    2.43 -    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
    2.44 +    show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
    2.45      proof (cases rule: converse_rtranclE)
    2.46        assume "a=y"
    2.47 -      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
    2.48 +      with a_v_r v_x_rt have "(y,x) \<in> r*"
    2.49  	by (auto intro: r_into_rtrancl rtrancl_trans)
    2.50        then show ?thesis 
    2.51  	by blast
    2.52      next
    2.53        fix w 
    2.54        assume a_w_r: "(a, w) \<in> r" and
    2.55 -            w_y_rt: "(w, y) \<in> r\<^sup>*"
    2.56 +            w_y_rt: "(w, y) \<in> r*"
    2.57        from a_v_r a_w_r unique 
    2.58        have "v=w" 
    2.59  	by auto
    2.60 @@ -107,7 +105,7 @@
    2.61  
    2.62  
    2.63  lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
    2.64 - "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    2.65 + "\<lbrakk>(a,b)\<in>r*;  a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    2.66  apply (erule rtranclE)
    2.67  apply (auto dest: rtrancl_into_trancl1)
    2.68  done
     3.1 --- a/src/HOL/Induct/Com.thy	Thu Aug 13 17:19:10 2009 +0100
     3.2 +++ b/src/HOL/Induct/Com.thy	Thu Aug 13 17:19:42 2009 +0100
     3.3 @@ -91,8 +91,6 @@
     3.4    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
     3.5    by (auto simp add: le_fun_def le_bool_def mem_def)
     3.6  
     3.7 -declare [[unify_trace_bound = 30, unify_search_bound = 60]]
     3.8 -
     3.9  text{*Command execution is functional (deterministic) provided evaluation is*}
    3.10  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
    3.11  apply (simp add: single_valued_def)
     4.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Aug 13 17:19:10 2009 +0100
     4.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Aug 13 17:19:42 2009 +0100
     4.3 @@ -183,8 +183,6 @@
     4.4    (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
     4.5  *}
     4.6  
     4.7 -declare [[unify_search_bound = 40, unify_trace_bound = 40]]
     4.8 -
     4.9  
    4.10  theorem eval_evals_exec_type_sound: 
    4.11  "wf_java_prog G ==>  
    4.12 @@ -368,8 +366,6 @@
    4.13  
    4.14  done
    4.15  
    4.16 -declare [[unify_search_bound = 20, unify_trace_bound = 20]]
    4.17 -
    4.18  
    4.19  lemma eval_type_sound: "!!E s s'.  
    4.20    [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]