author haftmann Thu Oct 13 23:02:59 2011 +0200 (2011-10-13) changeset 45139 bdcaa3f3a2f4 parent 45138 ba618e9288b8 child 45140 339a8b3c4791
moved acyclic predicate up in hierarchy
 src/HOL/Relation.thy file | annotate | diff | revisions src/HOL/Transitive_Closure.thy file | annotate | diff | revisions src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     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.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.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.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"