author haftmann Tue Nov 30 17:22:59 2010 +0100 (2010-11-30) changeset 40825 c55ee3793712 parent 40824 f5a0cb45d2a5 child 40826 a3af470a55d2
adaptions to changes in Equiv_Relation.thy
```     1.1 --- a/src/HOL/Induct/QuoDataType.thy	Tue Nov 30 17:19:11 2010 +0100
1.2 +++ b/src/HOL/Induct/QuoDataType.thy	Tue Nov 30 17:22:59 2010 +0100
1.3 @@ -176,7 +176,7 @@
1.4                Abs_Msg (msgrel``{MPAIR U V})"
1.5  proof -
1.6    have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
1.7 -    by (simp add: congruent2_def msgrel.MPAIR)
1.8 +    by (auto simp add: congruent2_def msgrel.MPAIR)
1.9    thus ?thesis
1.10      by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
1.11  qed
1.12 @@ -184,7 +184,7 @@
1.13  lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
1.14  proof -
1.15    have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
1.16 -    by (simp add: congruent_def msgrel.CRYPT)
1.17 +    by (auto simp add: congruent_def msgrel.CRYPT)
1.18    thus ?thesis
1.19      by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
1.20  qed
1.21 @@ -193,7 +193,7 @@
1.22       "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
1.23  proof -
1.24    have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
1.25 -    by (simp add: congruent_def msgrel.DECRYPT)
1.26 +    by (auto simp add: congruent_def msgrel.DECRYPT)
1.27    thus ?thesis
1.28      by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
1.29  qed
1.30 @@ -221,7 +221,7 @@
1.31     "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
1.32
1.33  lemma nonces_congruent: "freenonces respects msgrel"
1.34 -by (simp add: congruent_def msgrel_imp_eq_freenonces)
1.35 +by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
1.36
1.37
1.38  text{*Now prove the four equations for @{term nonces}*}
1.39 @@ -256,7 +256,7 @@
1.40     "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
1.41
1.42  lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
1.43 -by (simp add: congruent_def msgrel_imp_eqv_freeleft)
1.44 +by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
1.45
1.46  text{*Now prove the four equations for @{term left}*}
1.47
1.48 @@ -290,7 +290,7 @@
1.49     "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
1.50
1.51  lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
1.52 -by (simp add: congruent_def msgrel_imp_eqv_freeright)
1.53 +by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
1.54
1.55  text{*Now prove the four equations for @{term right}*}
1.56
1.57 @@ -425,7 +425,7 @@
1.58     "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
1.59
1.60  lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
1.61 -by (simp add: congruent_def msgrel_imp_eq_freediscrim)
1.62 +by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
1.63
1.64  text{*Now prove the four equations for @{term discrim}*}
1.65
```