src/HOL/Induct/QuoDataType.thy
changeset 40825 c55ee3793712
parent 39910 10097e0a9dbd
child 41959 b460124855b8
     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