fun_rel_def is no simp rule by default
authorhaftmann
Tue Nov 09 14:02:14 2010 +0100 (2010-11-09)
changeset 40468d4aac200199e
parent 40467 dc0439fdd7c5
child 40469 f208cb239da1
fun_rel_def is no simp rule by default
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Nov 09 14:02:13 2010 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Nov 09 14:02:14 2010 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4    shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
     1.5    and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
     1.6    and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
     1.7 -  by auto
     1.8 +  by (auto intro!: fun_relI)
     1.9  
    1.10  lemma times_int_raw_fst:
    1.11    assumes a: "x \<approx> z"
    1.12 @@ -167,7 +167,7 @@
    1.13  
    1.14  lemma[quot_respect]:
    1.15    shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
    1.16 -  by (simp add: equivp_reflp[OF int_equivp])
    1.17 +  by (auto simp add: equivp_reflp [OF int_equivp])
    1.18  
    1.19  lemma int_of_nat:
    1.20    shows "of_nat m = int_of_nat m"
     2.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 09 14:02:13 2010 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 09 14:02:14 2010 +0100
     2.3 @@ -179,11 +179,11 @@
     2.4  
     2.5  lemma [quot_respect]:
     2.6    shows "(op \<sim> ===> op =) freenonces freenonces"
     2.7 -  by (simp add: msgrel_imp_eq_freenonces)
     2.8 +  by (auto simp add: msgrel_imp_eq_freenonces)
     2.9  
    2.10  lemma [quot_respect]:
    2.11    shows "(op = ===> op \<sim>) NONCE NONCE"
    2.12 -  by (simp add: NONCE)
    2.13 +  by (auto simp add: NONCE)
    2.14  
    2.15  lemma nonces_Nonce [simp]:
    2.16    shows "nonces (Nonce N) = {N}"
    2.17 @@ -191,7 +191,7 @@
    2.18  
    2.19  lemma [quot_respect]:
    2.20    shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
    2.21 -  by (simp add: MPAIR)
    2.22 +  by (auto simp add: MPAIR)
    2.23  
    2.24  lemma nonces_MPair [simp]:
    2.25    shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
    2.26 @@ -214,7 +214,7 @@
    2.27  
    2.28  lemma [quot_respect]:
    2.29    shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
    2.30 -  by (simp add: msgrel_imp_eqv_freeleft)
    2.31 +  by (auto simp add: msgrel_imp_eqv_freeleft)
    2.32  
    2.33  lemma left_Nonce [simp]:
    2.34    shows "left (Nonce N) = Nonce N"
    2.35 @@ -243,7 +243,7 @@
    2.36  
    2.37  lemma [quot_respect]:
    2.38    shows "(op \<sim> ===> op \<sim>) freeright freeright"
    2.39 -  by (simp add: msgrel_imp_eqv_freeright)
    2.40 +  by (auto simp add: msgrel_imp_eqv_freeright)
    2.41  
    2.42  lemma right_Nonce [simp]:
    2.43    shows "right (Nonce N) = Nonce N"