1.1 --- a/src/HOL/Relation.thy	Thu Oct 13 22:56:19 2011 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Oct 13 23:02:59 2011 +0200
     1.3 @@ -307,6 +307,7 @@
     1.4  lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
     1.5  by(simp add:irrefl_def)
     1.6  
     1.7 +
     1.8  subsection {* Totality *}
     1.9  
    1.10  lemma total_on_empty[simp]: "total_on {} r"

     2.1 --- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 22:56:19 2011 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:02:59 2011 +0200
     2.3 @@ -980,6 +980,50 @@
     2.4  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
     2.5  done
     2.6  
     2.7 +subsection {* Acyclic relations *}
     2.8 +
     2.9 +definition acyclic :: "('a * 'a) set => bool" where
    2.10 +  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
    2.11 +
    2.12 +abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    2.13 +  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
    2.14 +
    2.15 +lemma acyclic_irrefl:
    2.16 +  "acyclic r \<longleftrightarrow> irrefl (r^+)"
    2.17 +  by (simp add: acyclic_def irrefl_def)
    2.18 +
    2.19 +lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
    2.20 +  by (simp add: acyclic_def)
    2.21 +
    2.22 +lemma acyclic_insert [iff]:
    2.23 +     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
    2.24 +apply (simp add: acyclic_def trancl_insert)
    2.25 +apply (blast intro: rtrancl_trans)
    2.26 +done
    2.27 +
    2.28 +lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
    2.29 +by (simp add: acyclic_def trancl_converse)
    2.30 +
    2.31 +lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
    2.32 +
    2.33 +lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
    2.34 +apply (simp add: acyclic_def antisym_def)
    2.35 +apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
    2.36 +done
    2.37 +
    2.38 +(* Other direction:
    2.39 +acyclic = no loops
    2.40 +antisym = only self loops
    2.41 +Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
    2.42 +==> antisym( r^* ) = acyclic(r - Id)";
    2.43 +*)
    2.44 +
    2.45 +lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
    2.46 +apply (simp add: acyclic_def)
    2.47 +apply (blast intro: trancl_mono)
    2.48 +done
    2.49 +
    2.50 +
    2.51  subsection {* Setup of transitivity reasoner *}
    2.52  
    2.53  ML {*

     3.1 --- a/src/HOL/Wellfounded.thy	Thu Oct 13 22:56:19 2011 +0200
     3.2 +++ b/src/HOL/Wellfounded.thy	Thu Oct 13 23:02:59 2011 +0200
     3.3 @@ -381,19 +381,6 @@
     3.4  
     3.5  subsection {* Acyclic relations *}
     3.6  
     3.7 -definition acyclic :: "('a * 'a) set => bool" where
     3.8 -  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
     3.9 -
    3.10 -abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    3.11 -  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
    3.12 -
    3.13 -lemma acyclic_irrefl:
    3.14 -  "acyclic r \<longleftrightarrow> irrefl (r^+)"
    3.15 -  by (simp add: acyclic_def irrefl_def)
    3.16 -
    3.17 -lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
    3.18 -  by (simp add: acyclic_def)
    3.19 -
    3.20  lemma wf_acyclic: "wf r ==> acyclic r"
    3.21  apply (simp add: acyclic_def)
    3.22  apply (blast elim: wf_trancl [THEN wf_irrefl])
    3.23 @@ -401,34 +388,6 @@
    3.24  
    3.25  lemmas wfP_acyclicP = wf_acyclic [to_pred]
    3.26  
    3.27 -lemma acyclic_insert [iff]:
    3.28 -     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
    3.29 -apply (simp add: acyclic_def trancl_insert)
    3.30 -apply (blast intro: rtrancl_trans)
    3.31 -done
    3.32 -
    3.33 -lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
    3.34 -by (simp add: acyclic_def trancl_converse)
    3.35 -
    3.36 -lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
    3.37 -
    3.38 -lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
    3.39 -apply (simp add: acyclic_def antisym_def)
    3.40 -apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
    3.41 -done
    3.42 -
    3.43 -(* Other direction:
    3.44 -acyclic = no loops
    3.45 -antisym = only self loops
    3.46 -Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
    3.47 -==> antisym( r^* ) = acyclic(r - Id)";
    3.48 -*)
    3.49 -
    3.50 -lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
    3.51 -apply (simp add: acyclic_def)
    3.52 -apply (blast intro: trancl_mono)
    3.53 -done
    3.54 -
    3.55  text{* Wellfoundedness of finite acyclic relations*}
    3.56  
    3.57  lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"