minor metis proof tuning
authorhaftmann
Wed Feb 10 15:14:01 2010 +0100 (2010-02-10)
changeset 350956cdf9bbd0342
parent 35094 a0e89e47b083
child 35096 f36965a1fd42
minor metis proof tuning
src/HOL/Metis_Examples/Message.thy
     1.1 --- a/src/HOL/Metis_Examples/Message.thy	Wed Feb 10 14:12:40 2010 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Message.thy	Wed Feb 10 15:14:01 2010 +0100
     1.3 @@ -252,7 +252,7 @@
     1.4  
     1.5  declare [[ atp_problem_prefix = "Message__parts_cut" ]]
     1.6  lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
     1.7 -by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
     1.8 +by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
     1.9  
    1.10  
    1.11  
    1.12 @@ -698,13 +698,12 @@
    1.13  apply (rule subsetI)
    1.14  apply (erule analz.induct)
    1.15  apply (metis UnCI UnE Un_commute analz.Inj)
    1.16 -apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
    1.17 -apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
    1.18 +apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
    1.19 +apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
    1.20  apply (blast intro: analz.Decrypt)
    1.21  apply blast
    1.22  done
    1.23  
    1.24 -
    1.25  declare [[ atp_problem_prefix = "Message__analz_synth" ]]
    1.26  lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
    1.27  proof (neg_clausify)