src/HOL/Wellfounded.thy
changeset 45139 bdcaa3f3a2f4
parent 45137 6e422d180de8
child 45970 b6d0cff57d96
     1.1 --- a/src/HOL/Wellfounded.thy	Thu Oct 13 22:56:19 2011 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu Oct 13 23:02:59 2011 +0200
     1.3 @@ -381,19 +381,6 @@
     1.4  
     1.5  subsection {* Acyclic relations *}
     1.6  
     1.7 -definition acyclic :: "('a * 'a) set => bool" where
     1.8 -  "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
     1.9 -
    1.10 -abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    1.11 -  "acyclicP r \<equiv> acyclic {(x, y). r x y}"
    1.12 -
    1.13 -lemma acyclic_irrefl:
    1.14 -  "acyclic r \<longleftrightarrow> irrefl (r^+)"
    1.15 -  by (simp add: acyclic_def irrefl_def)
    1.16 -
    1.17 -lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
    1.18 -  by (simp add: acyclic_def)
    1.19 -
    1.20  lemma wf_acyclic: "wf r ==> acyclic r"
    1.21  apply (simp add: acyclic_def)
    1.22  apply (blast elim: wf_trancl [THEN wf_irrefl])
    1.23 @@ -401,34 +388,6 @@
    1.24  
    1.25  lemmas wfP_acyclicP = wf_acyclic [to_pred]
    1.26  
    1.27 -lemma acyclic_insert [iff]:
    1.28 -     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
    1.29 -apply (simp add: acyclic_def trancl_insert)
    1.30 -apply (blast intro: rtrancl_trans)
    1.31 -done
    1.32 -
    1.33 -lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
    1.34 -by (simp add: acyclic_def trancl_converse)
    1.35 -
    1.36 -lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
    1.37 -
    1.38 -lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
    1.39 -apply (simp add: acyclic_def antisym_def)
    1.40 -apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
    1.41 -done
    1.42 -
    1.43 -(* Other direction:
    1.44 -acyclic = no loops
    1.45 -antisym = only self loops
    1.46 -Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
    1.47 -==> antisym( r^* ) = acyclic(r - Id)";
    1.48 -*)
    1.49 -
    1.50 -lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
    1.51 -apply (simp add: acyclic_def)
    1.52 -apply (blast intro: trancl_mono)
    1.53 -done
    1.54 -
    1.55  text{* Wellfoundedness of finite acyclic relations*}
    1.56  
    1.57  lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"