src/HOL/Relation.thy
changeset 24286 7619080e49f0
parent 23709 fd31da8f752a
child 24915 fc90277c0dd7
     1.1 --- a/src/HOL/Relation.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Relation.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
     1.5    by (simp add: diag_def)
     1.6  
     1.7 -lemma diagI [intro!]: "a : A ==> (a, a) : diag A"
     1.8 +lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
     1.9    by (rule diag_eqI) (rule refl)
    1.10  
    1.11  lemma diagE [elim!]:
    1.12 @@ -325,6 +325,8 @@
    1.13  
    1.14  subsection {* Domain *}
    1.15  
    1.16 +declare Domain_def [noatp]
    1.17 +
    1.18  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
    1.19    by (unfold Domain_def) blast
    1.20  
    1.21 @@ -411,6 +413,8 @@
    1.22  
    1.23  subsection {* Image of a set under a relation *}
    1.24  
    1.25 +declare Image_def [noatp]
    1.26 +
    1.27  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
    1.28    by (simp add: Image_def)
    1.29  
    1.30 @@ -420,7 +424,7 @@
    1.31  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
    1.32    by (rule Image_iff [THEN trans]) simp
    1.33  
    1.34 -lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
    1.35 +lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
    1.36    by (unfold Image_def) blast
    1.37  
    1.38  lemma ImageE [elim!]: