added lemmas
authornipkow
Mon Mar 17 16:47:24 2008 +0100 (2008-03-17)
changeset 2629774012d599204
parent 26296 988a103afbab
child 26298 53e382ccf71f
added lemmas
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Mon Mar 17 16:13:05 2008 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Mar 17 16:47:24 2008 +0100
     1.3 @@ -54,6 +54,10 @@
     1.4    refl :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
     1.5    "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
     1.6  
     1.7 +abbreviation
     1.8 +  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
     1.9 +  "reflexive == refl UNIV"
    1.10 +
    1.11  definition
    1.12    sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
    1.13    "sym r == ALL x y. (x,y): r --> (y,x): r"
    1.14 @@ -74,10 +78,6 @@
    1.15    inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
    1.16    "inv_image r f == {(x, y). (f x, f y) : r}"
    1.17  
    1.18 -abbreviation
    1.19 -  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
    1.20 -  "reflexive == refl UNIV"
    1.21 -
    1.22  
    1.23  subsection {* The identity relation *}
    1.24  
    1.25 @@ -195,6 +195,9 @@
    1.26    "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
    1.27  by (unfold refl_def) blast
    1.28  
    1.29 +lemma refl_empty[simp]: "refl {} {}"
    1.30 +by(simp add:refl_def)
    1.31 +
    1.32  lemma refl_diag: "refl A (diag A)"
    1.33  by (rule reflI [OF diag_subset_Times diagI])
    1.34