src/HOL/Auth/Message.thy
changeset 13922 75ae4244a596
parent 11270 a315a3862bb4
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Apr 23 18:09:48 2003 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Apr 25 11:18:14 2003 +0200
     1.3 @@ -135,6 +135,25 @@
     1.4  
     1.5  use "Message_lemmas.ML"
     1.6  
     1.7 +lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
     1.8 +by auto
     1.9 +
    1.10 +lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
    1.11 +by auto
    1.12 +
    1.13 +lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
    1.14 +by (simp add: synth_mono analz_mono) 
    1.15 +
    1.16 +lemma Fake_analz_eq [simp]:
    1.17 +     "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
    1.18 +apply (drule Fake_analz_insert[of _ _ "H"])
    1.19 +apply (simp add: synth_increasing[THEN Un_absorb2])
    1.20 +apply (drule synth_mono)
    1.21 +apply (simp add: synth_idem)
    1.22 +apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 
    1.23 +done
    1.24 +
    1.25 +
    1.26  lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
    1.27  
    1.28  lemma Fake_parts_insert_in_Un:
    1.29 @@ -142,6 +161,25 @@
    1.30        ==> Z \<in>  synth (analz H) \<union> parts H";
    1.31  by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
    1.32  
    1.33 +text{*Two generalizations of @{text analz_insert_eq}*}
    1.34 +lemma gen_analz_insert_eq [rule_format]:
    1.35 +     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
    1.36 +by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
    1.37 +
    1.38 +lemma synth_analz_insert_eq [rule_format]:
    1.39 +     "X \<in> synth (analz H) 
    1.40 +      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
    1.41 +apply (erule synth.induct) 
    1.42 +apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
    1.43 +done
    1.44 +
    1.45 +lemma Fake_parts_sing:
    1.46 +     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) Un parts H";
    1.47 +apply (rule subset_trans) 
    1.48 + apply (erule_tac [2] Fake_parts_insert) 
    1.49 +apply (simp add: parts_mono) 
    1.50 +done
    1.51 +
    1.52  method_setup spy_analz = {*
    1.53      Method.ctxt_args (fn ctxt =>
    1.54          Method.METHOD (fn facts =>