Simplified a couple of proofs and corrected a comment
authorpaulson
Thu Mar 04 17:08:41 2010 +0000 (2010-03-04)
changeset 355663c01f5ad1d34
parent 35565 56b070cd7ab3
child 35567 309e75c58af2
Simplified a couple of proofs and corrected a comment
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Mar 04 11:22:06 2010 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Mar 04 17:08:41 2010 +0000
     1.3 @@ -236,7 +236,7 @@
     1.4  by blast
     1.5  
     1.6  lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
     1.7 -by (metis equalityE parts_idem parts_increasing parts_mono subset_trans)
     1.8 +by (metis parts_idem parts_increasing parts_mono subset_trans)
     1.9  
    1.10  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
    1.11  by (drule parts_mono, blast)
    1.12 @@ -611,7 +611,7 @@
    1.13  by blast
    1.14  
    1.15  lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
    1.16 -by (metis equalityE subset_trans synth_idem synth_increasing synth_mono)
    1.17 +by (metis subset_trans synth_idem synth_increasing synth_mono)
    1.18  
    1.19  lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
    1.20  by (drule synth_mono, blast)
    1.21 @@ -674,8 +674,7 @@
    1.22  lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
    1.23  by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)
    1.24  
    1.25 -text{*More specifically for Fake.  Very occasionally we could do with a version
    1.26 -  of the form  @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"} *}
    1.27 +text{*More specifically for Fake. See also @{text Fake_parts_sing} below *}
    1.28  lemma Fake_parts_insert:
    1.29       "X \<in> synth (analz H) ==>  
    1.30        parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
    1.31 @@ -884,17 +883,17 @@
    1.32  
    1.33  lemma Fake_analz_eq [simp]:
    1.34       "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
    1.35 -by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute equalityI
    1.36 +by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute 
    1.37            subset_insertI synth_analz_mono synth_increasing synth_subset_iff)
    1.38  
    1.39  text{*Two generalizations of @{text analz_insert_eq}*}
    1.40  lemma gen_analz_insert_eq [rule_format]:
    1.41 -     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
    1.42 +     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
    1.43  by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
    1.44  
    1.45  lemma synth_analz_insert_eq [rule_format]:
    1.46       "X \<in> synth (analz H) 
    1.47 -      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
    1.48 +      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
    1.49  apply (erule synth.induct) 
    1.50  apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
    1.51  done