src/HOL/Auth/Message.thy
changeset 17689 a04b5b43625e
parent 16818 2b82259cc7b2
child 17729 d74d0b5052a0
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Sep 28 11:14:26 2005 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Sep 28 11:15:33 2005 +0200
     1.3 @@ -240,6 +240,12 @@
     1.4  lemma parts_idem [simp]: "parts (parts H) = parts H"
     1.5  by blast
     1.6  
     1.7 +lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
     1.8 +apply (rule iffI)
     1.9 +apply (iprover intro: subset_trans parts_increasing)  
    1.10 +apply (frule parts_mono, simp) 
    1.11 +done
    1.12 +
    1.13  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
    1.14  by (drule parts_mono, blast)
    1.15  
    1.16 @@ -288,13 +294,11 @@
    1.17  done
    1.18  
    1.19  lemma parts_insert_Crypt [simp]:
    1.20 -     "parts (insert (Crypt K X) H) =  
    1.21 -          insert (Crypt K X) (parts (insert X H))"
    1.22 +     "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))"
    1.23  apply (rule equalityI)
    1.24  apply (rule subsetI)
    1.25  apply (erule parts.induct, auto)
    1.26 -apply (erule parts.induct)
    1.27 -apply (blast intro: parts.Body)+
    1.28 +apply (blast intro: parts.Body)
    1.29  done
    1.30  
    1.31  lemma parts_insert_MPair [simp]:
    1.32 @@ -303,7 +307,6 @@
    1.33  apply (rule equalityI)
    1.34  apply (rule subsetI)
    1.35  apply (erule parts.induct, auto)
    1.36 -apply (erule parts.induct)
    1.37  apply (blast intro: parts.Fst parts.Snd)+
    1.38  done
    1.39  
    1.40 @@ -507,6 +510,12 @@
    1.41  lemma analz_idem [simp]: "analz (analz H) = analz H"
    1.42  by blast
    1.43  
    1.44 +lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
    1.45 +apply (rule iffI)
    1.46 +apply (iprover intro: subset_trans analz_increasing)  
    1.47 +apply (frule analz_mono, simp) 
    1.48 +done
    1.49 +
    1.50  lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
    1.51  by (drule analz_mono, blast)
    1.52  
    1.53 @@ -528,16 +537,15 @@
    1.54  text{*A congruence rule for "analz" *}
    1.55  
    1.56  lemma analz_subset_cong:
    1.57 -     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
    1.58 -               |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
    1.59 -apply clarify
    1.60 -apply (erule analz.induct)
    1.61 -apply (best intro: analz_mono [THEN subsetD])+
    1.62 +     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
    1.63 +      ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
    1.64 +apply simp
    1.65 +apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) 
    1.66  done
    1.67  
    1.68  lemma analz_cong:
    1.69 -     "[| analz G = analz G'; analz H = analz H'  
    1.70 -               |] ==> analz (G \<union> H) = analz (G' \<union> H')"
    1.71 +     "[| analz G = analz G'; analz H = analz H' |] 
    1.72 +      ==> analz (G \<union> H) = analz (G' \<union> H')"
    1.73  by (intro equalityI analz_subset_cong, simp_all) 
    1.74  
    1.75  lemma analz_insert_cong:
    1.76 @@ -613,6 +621,12 @@
    1.77  lemma synth_idem: "synth (synth H) = synth H"
    1.78  by blast
    1.79  
    1.80 +lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
    1.81 +apply (rule iffI)
    1.82 +apply (iprover intro: subset_trans synth_increasing)  
    1.83 +apply (frule synth_mono, simp add: synth_idem) 
    1.84 +done
    1.85 +
    1.86  lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
    1.87  by (drule synth_mono, blast)
    1.88  
    1.89 @@ -896,7 +910,7 @@
    1.90  by auto
    1.91  
    1.92  lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
    1.93 -by (simp add: synth_mono analz_mono) 
    1.94 +by (iprover intro: synth_mono analz_mono) 
    1.95  
    1.96  lemma Fake_analz_eq [simp]:
    1.97       "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
    1.98 @@ -904,7 +918,9 @@
    1.99  apply (simp add: synth_increasing[THEN Un_absorb2])
   1.100  apply (drule synth_mono)
   1.101  apply (simp add: synth_idem)
   1.102 -apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 
   1.103 +apply (rule equalityI)
   1.104 +apply (simp add: );
   1.105 +apply (rule synth_analz_mono, blast)   
   1.106  done
   1.107  
   1.108  text{*Two generalizations of @{text analz_insert_eq}*}
   1.109 @@ -922,8 +938,9 @@
   1.110  lemma Fake_parts_sing:
   1.111       "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
   1.112  apply (rule subset_trans) 
   1.113 - apply (erule_tac [2] Fake_parts_insert) 
   1.114 -apply (simp add: parts_mono) 
   1.115 + apply (erule_tac [2] Fake_parts_insert)
   1.116 +apply (rule parts_mono)  
   1.117 +apply (blast intro: elim:); 
   1.118  done
   1.119  
   1.120  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]