src/HOL/Relation.thy
changeset 29859 33bff35f1335
parent 29609 a010aab5bed0
child 30198 922f944f03b2
     1.1 --- a/src/HOL/Relation.thy	Tue Feb 10 17:53:51 2009 -0800
     1.2 +++ b/src/HOL/Relation.thy	Wed Feb 11 10:51:07 2009 +0100
     1.3 @@ -70,6 +70,16 @@
     1.4    "trans r == (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
     1.5  
     1.6  definition
     1.7 +irrefl :: "('a * 'a) set => bool" where
     1.8 +"irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
     1.9 +
    1.10 +definition
    1.11 +total_on :: "'a set => ('a * 'a) set => bool" where
    1.12 +"total_on A r \<equiv> \<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
    1.13 +
    1.14 +abbreviation "total \<equiv> total_on UNIV"
    1.15 +
    1.16 +definition
    1.17    single_valued :: "('a * 'b) set => bool" where
    1.18    "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)"
    1.19  
    1.20 @@ -268,6 +278,21 @@
    1.21  lemma trans_diag [simp]: "trans (diag A)"
    1.22  by (fast intro: transI elim: transD)
    1.23  
    1.24 +lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
    1.25 +unfolding antisym_def trans_def by blast
    1.26 +
    1.27 +subsection {* Irreflexivity *}
    1.28 +
    1.29 +lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
    1.30 +by(simp add:irrefl_def)
    1.31 +
    1.32 +subsection {* Totality *}
    1.33 +
    1.34 +lemma total_on_empty[simp]: "total_on {} r"
    1.35 +by(simp add:total_on_def)
    1.36 +
    1.37 +lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
    1.38 +by(simp add: total_on_def)
    1.39  
    1.40  subsection {* Converse *}
    1.41  
    1.42 @@ -330,6 +355,9 @@
    1.43  lemma sym_Int_converse: "sym (r \<inter> r^-1)"
    1.44  by (unfold sym_def) blast
    1.45  
    1.46 +lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
    1.47 +by (auto simp: total_on_def)
    1.48 +
    1.49  
    1.50  subsection {* Domain *}
    1.51