# HG changeset patch # User haftmann # Date 1291134179 -3600 # Node ID c55ee3793712eb9bd5e82f7b64d1d814f2565a5d # Parent f5a0cb45d2a559959927df7e6003329bd92147b5 adaptions to changes in Equiv_Relation.thy diff -r f5a0cb45d2a5 -r c55ee3793712 src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Tue Nov 30 17:19:11 2010 +0100 +++ b/src/HOL/Induct/QuoDataType.thy Tue Nov 30 17:22:59 2010 +0100 @@ -176,7 +176,7 @@ Abs_Msg (msgrel``{MPAIR U V})" proof - have "(\U V. msgrel `` {MPAIR U V}) respects2 msgrel" - by (simp add: congruent2_def msgrel.MPAIR) + by (auto simp add: congruent2_def msgrel.MPAIR) thus ?thesis by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel]) qed @@ -184,7 +184,7 @@ lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})" proof - have "(\U. msgrel `` {CRYPT K U}) respects msgrel" - by (simp add: congruent_def msgrel.CRYPT) + by (auto simp add: congruent_def msgrel.CRYPT) thus ?thesis by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel]) qed @@ -193,7 +193,7 @@ "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})" proof - have "(\U. msgrel `` {DECRYPT K U}) respects msgrel" - by (simp add: congruent_def msgrel.DECRYPT) + by (auto simp add: congruent_def msgrel.DECRYPT) thus ?thesis by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel]) qed @@ -221,7 +221,7 @@ "nonces X = (\U \ Rep_Msg X. freenonces U)" lemma nonces_congruent: "freenonces respects msgrel" -by (simp add: congruent_def msgrel_imp_eq_freenonces) +by (auto simp add: congruent_def msgrel_imp_eq_freenonces) text{*Now prove the four equations for @{term nonces}*} @@ -256,7 +256,7 @@ "left X = Abs_Msg (\U \ Rep_Msg X. msgrel``{freeleft U})" lemma left_congruent: "(\U. msgrel `` {freeleft U}) respects msgrel" -by (simp add: congruent_def msgrel_imp_eqv_freeleft) +by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) text{*Now prove the four equations for @{term left}*} @@ -290,7 +290,7 @@ "right X = Abs_Msg (\U \ Rep_Msg X. msgrel``{freeright U})" lemma right_congruent: "(\U. msgrel `` {freeright U}) respects msgrel" -by (simp add: congruent_def msgrel_imp_eqv_freeright) +by (auto simp add: congruent_def msgrel_imp_eqv_freeright) text{*Now prove the four equations for @{term right}*} @@ -425,7 +425,7 @@ "discrim X = the_elem (\U \ Rep_Msg X. {freediscrim U})" lemma discrim_congruent: "(\U. {freediscrim U}) respects msgrel" -by (simp add: congruent_def msgrel_imp_eq_freediscrim) +by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) text{*Now prove the four equations for @{term discrim}*}