src/HOL/Quotient_Examples/Quotient_Message.thy

--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 01:38:29 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 02:18:08 2010 +0100
@@ -32,7 +32,7 @@
 text{*Proving that it is an equivalence relation*}
 
 lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
+by (induct X) (auto intro: msgrel.intros)
 
 theorem equiv_msgrel: "equivp msgrel"
 proof (rule equivpI)
@@ -263,68 +263,47 @@
 
 subsection{*Injectivity Properties of Some Constructors*}
 
-lemma NONCE_imp_eq:
-  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
-  by (drule msgrel_imp_eq_freenonces, simp)
-
 text{*Can also be proved using the function @{term nonces}*}
 lemma Nonce_Nonce_eq [iff]:
   shows "(Nonce m = Nonce n) = (m = n)"
 proof
   assume "Nonce m = Nonce n"
-  then show "m = n" by (lifting NONCE_imp_eq)
+  then show "m = n" 
+    by (descending) (drule msgrel_imp_eq_freenonces, simp)
 next
   assume "m = n"
   then show "Nonce m = Nonce n" by simp
 qed
 
-lemma MPAIR_imp_eqv_left:
-  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
-  by (drule msgrel_imp_eqv_freeleft) (simp)
-
 lemma MPair_imp_eq_left:
   assumes eq: "MPair X Y = MPair X' Y'"
   shows "X = X'"
-  using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
-  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
-  by (drule msgrel_imp_eqv_freeright) (simp)
+  using eq 
+  by (descending) (drule msgrel_imp_eqv_freeleft, simp)
 
 lemma MPair_imp_eq_right:
   shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
-  by (lifting  MPAIR_imp_eqv_right)
+  by (descending) (drule msgrel_imp_eqv_freeright, simp)
 
 theorem MPair_MPair_eq [iff]:
   shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
   by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
 
-lemma NONCE_neqv_MPAIR:
-  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
-  by (auto dest: msgrel_imp_eq_freediscrim)
-
 theorem Nonce_neq_MPair [iff]:
   shows "Nonce N \<noteq> MPair X Y"
-  by (lifting NONCE_neqv_MPAIR)
+  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
 
 text{*Example suggested by a referee*}
 
-lemma CRYPT_NONCE_neq_NONCE:
-  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
-  by (auto dest: msgrel_imp_eq_freediscrim)
-
 theorem Crypt_Nonce_neq_Nonce:
   shows "Crypt K (Nonce M) \<noteq> Nonce N"
-  by (lifting CRYPT_NONCE_neq_NONCE)
+  by (descending) (auto dest: msgrel_imp_eq_freediscrim) 
 
 text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
-  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
-  by (auto dest: msgrel_imp_eq_freediscrim)
 
 theorem Crypt2_Nonce_neq_Nonce:
   shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
-  by (lifting CRYPT2_NONCE_neq_NONCE)
+  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
 
 theorem Crypt_Crypt_eq [iff]:
   shows "(Crypt K X = Crypt K X') = (X=X')"