author krauss Mon Oct 26 23:27:16 2009 +0100 (2009-10-26) changeset 33217 ab979f6e99f4 parent 33216 7c61bc5d7310 child 33218 ecb5cd453ef2
authentic constants; moved "acyclic" further down
 src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:57 2009 +0100
1.2 +++ b/src/HOL/Wellfounded.thy	Mon Oct 26 23:27:16 2009 +0100
1.3 @@ -14,19 +14,12 @@
1.4
1.5  subsection {* Basic Definitions *}
1.6
1.7 -constdefs
1.8 -  wf         :: "('a * 'a)set => bool"
1.9 +definition wf :: "('a * 'a) set => bool" where
1.10    "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
1.11
1.12 -  wfP :: "('a => 'a => bool) => bool"
1.13 +definition wfP :: "('a => 'a => bool) => bool" where
1.14    "wfP r == wf {(x, y). r x y}"
1.15
1.16 -  acyclic :: "('a*'a)set => bool"
1.17 -  "acyclic r == !x. (x,x) ~: r^+"
1.18 -
1.19 -abbreviation acyclicP :: "('a => 'a => bool) => bool" where
1.20 -  "acyclicP r == acyclic {(x, y). r x y}"
1.21 -
1.22  lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
1.24
1.25 @@ -388,7 +381,13 @@
1.26    by (rule wf_union_merge [where S = "{}", simplified])
1.27
1.28
1.29 -subsubsection {* acyclic *}
1.30 +subsection {* Acyclic relations *}
1.31 +
1.32 +definition acyclic :: "('a * 'a) set => bool" where
1.33 +  "acyclic r == !x. (x,x) ~: r^+"
1.34 +
1.35 +abbreviation acyclicP :: "('a => 'a => bool) => bool" where
1.36 +  "acyclicP r == acyclic {(x, y). r x y}"
1.37
1.38  lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"