# HG changeset patch
# User haftmann
# Date 1318539779 -7200
# Node ID bdcaa3f3a2f418a389d7cee78bf7f9f02309cbe8
# Parent  ba618e9288b859f2d6c9e1b0c7468fb05d04aa50
moved acyclic predicate up in hierarchy

diff -r ba618e9288b8 -r bdcaa3f3a2f4 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Oct 13 22:56:19 2011 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 13 23:02:59 2011 +0200
@@ -307,6 +307,7 @@
 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
 by(simp add:irrefl_def)
 
+
 subsection {* Totality *}
 
 lemma total_on_empty[simp]: "total_on {} r"
diff -r ba618e9288b8 -r bdcaa3f3a2f4 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 22:56:19 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:02:59 2011 +0200
@@ -980,6 +980,50 @@
 apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
 done
 
+subsection {* Acyclic relations *}
+
+definition acyclic :: "('a * 'a) set => bool" where
+  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
+
+abbreviation acyclicP :: "('a => 'a => bool) => bool" where
+  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
+
+lemma acyclic_irrefl:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (simp add: acyclic_def irrefl_def)
+
+lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
+  by (simp add: acyclic_def)
+
+lemma acyclic_insert [iff]:
+     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
+apply (simp add: acyclic_def trancl_insert)
+apply (blast intro: rtrancl_trans)
+done
+
+lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
+by (simp add: acyclic_def trancl_converse)
+
+lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
+
+lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
+apply (simp add: acyclic_def antisym_def)
+apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
+done
+
+(* Other direction:
+acyclic = no loops
+antisym = only self loops
+Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
+==> antisym( r^* ) = acyclic(r - Id)";
+*)
+
+lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
+apply (simp add: acyclic_def)
+apply (blast intro: trancl_mono)
+done
+
+
 subsection {* Setup of transitivity reasoner *}
 
 ML {*
diff -r ba618e9288b8 -r bdcaa3f3a2f4 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Oct 13 22:56:19 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Oct 13 23:02:59 2011 +0200
@@ -381,19 +381,6 @@
 
 subsection {* Acyclic relations *}
 
-definition acyclic :: "('a * 'a) set => bool" where
-  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
-
-abbreviation acyclicP :: "('a => 'a => bool) => bool" where
-  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
-
-lemma acyclic_irrefl:
-  "acyclic r \<longleftrightarrow> irrefl (r^+)"
-  by (simp add: acyclic_def irrefl_def)
-
-lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
-  by (simp add: acyclic_def)
-
 lemma wf_acyclic: "wf r ==> acyclic r"
 apply (simp add: acyclic_def)
 apply (blast elim: wf_trancl [THEN wf_irrefl])
@@ -401,34 +388,6 @@
 
 lemmas wfP_acyclicP = wf_acyclic [to_pred]
 
-lemma acyclic_insert [iff]:
-     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
-apply (simp add: acyclic_def trancl_insert)
-apply (blast intro: rtrancl_trans)
-done
-
-lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
-by (simp add: acyclic_def trancl_converse)
-
-lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
-
-lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
-apply (simp add: acyclic_def antisym_def)
-apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
-done
-
-(* Other direction:
-acyclic = no loops
-antisym = only self loops
-Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
-==> antisym( r^* ) = acyclic(r - Id)";
-*)
-
-lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
-apply (simp add: acyclic_def)
-apply (blast intro: trancl_mono)
-done
-
 text{* Wellfoundedness of finite acyclic relations*}
 
 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"