author paulson Thu Mar 04 17:08:41 2010 +0000 (2010-03-04 ago) changeset 35566 3c01f5ad1d34 parent 35565 56b070cd7ab3 child 35567 309e75c58af2
Simplified a couple of proofs and corrected a comment
```     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.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
```