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')"
```