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.31 +
1.32 +subsection {* Totality *}
1.33 +
1.34 +lemma total_on_empty[simp]: "total_on {} r"
1.36 +
1.37 +lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
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
```