src/HOL/Quotient_Examples/Quotient_Message.thy
changeset 37594 32ad67684ee7
parent 36524 3909002beca5
child 40468 d4aac200199e
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 01:38:29 2010 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 02:18:08 2010 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  text{*Proving that it is an equivalence relation*}
     1.5  
     1.6  lemma msgrel_refl: "X \<sim> X"
     1.7 -by (induct X, (blast intro: msgrel.intros)+)
     1.8 +by (induct X) (auto intro: msgrel.intros)
     1.9  
    1.10  theorem equiv_msgrel: "equivp msgrel"
    1.11  proof (rule equivpI)
    1.12 @@ -263,68 +263,47 @@
    1.13  
    1.14  subsection{*Injectivity Properties of Some Constructors*}
    1.15  
    1.16 -lemma NONCE_imp_eq:
    1.17 -  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
    1.18 -  by (drule msgrel_imp_eq_freenonces, simp)
    1.19 -
    1.20  text{*Can also be proved using the function @{term nonces}*}
    1.21  lemma Nonce_Nonce_eq [iff]:
    1.22    shows "(Nonce m = Nonce n) = (m = n)"
    1.23  proof
    1.24    assume "Nonce m = Nonce n"
    1.25 -  then show "m = n" by (lifting NONCE_imp_eq)
    1.26 +  then show "m = n" 
    1.27 +    by (descending) (drule msgrel_imp_eq_freenonces, simp)
    1.28  next
    1.29    assume "m = n"
    1.30    then show "Nonce m = Nonce n" by simp
    1.31  qed
    1.32  
    1.33 -lemma MPAIR_imp_eqv_left:
    1.34 -  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
    1.35 -  by (drule msgrel_imp_eqv_freeleft) (simp)
    1.36 -
    1.37  lemma MPair_imp_eq_left:
    1.38    assumes eq: "MPair X Y = MPair X' Y'"
    1.39    shows "X = X'"
    1.40 -  using eq by (lifting MPAIR_imp_eqv_left)
    1.41 -
    1.42 -lemma MPAIR_imp_eqv_right:
    1.43 -  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
    1.44 -  by (drule msgrel_imp_eqv_freeright) (simp)
    1.45 +  using eq 
    1.46 +  by (descending) (drule msgrel_imp_eqv_freeleft, simp)
    1.47  
    1.48  lemma MPair_imp_eq_right:
    1.49    shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
    1.50 -  by (lifting  MPAIR_imp_eqv_right)
    1.51 +  by (descending) (drule msgrel_imp_eqv_freeright, simp)
    1.52  
    1.53  theorem MPair_MPair_eq [iff]:
    1.54    shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
    1.55    by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
    1.56  
    1.57 -lemma NONCE_neqv_MPAIR:
    1.58 -  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
    1.59 -  by (auto dest: msgrel_imp_eq_freediscrim)
    1.60 -
    1.61  theorem Nonce_neq_MPair [iff]:
    1.62    shows "Nonce N \<noteq> MPair X Y"
    1.63 -  by (lifting NONCE_neqv_MPAIR)
    1.64 +  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
    1.65  
    1.66  text{*Example suggested by a referee*}
    1.67  
    1.68 -lemma CRYPT_NONCE_neq_NONCE:
    1.69 -  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
    1.70 -  by (auto dest: msgrel_imp_eq_freediscrim)
    1.71 -
    1.72  theorem Crypt_Nonce_neq_Nonce:
    1.73    shows "Crypt K (Nonce M) \<noteq> Nonce N"
    1.74 -  by (lifting CRYPT_NONCE_neq_NONCE)
    1.75 +  by (descending) (auto dest: msgrel_imp_eq_freediscrim) 
    1.76  
    1.77  text{*...and many similar results*}
    1.78 -lemma CRYPT2_NONCE_neq_NONCE:
    1.79 -  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
    1.80 -  by (auto dest: msgrel_imp_eq_freediscrim)
    1.81  
    1.82  theorem Crypt2_Nonce_neq_Nonce:
    1.83    shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
    1.84 -  by (lifting CRYPT2_NONCE_neq_NONCE)
    1.85 +  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
    1.86  
    1.87  theorem Crypt_Crypt_eq [iff]:
    1.88    shows "(Crypt K X = Crypt K X') = (X=X')"