authentic constants; moved "acyclic" further down
authorkrauss
Mon Oct 26 23:27:16 2009 +0100 (2009-10-26)
changeset 33217ab979f6e99f4
parent 33216 7c61bc5d7310
child 33218 ecb5cd453ef2
authentic constants; moved "acyclic" further down
src/HOL/Wellfounded.thy
     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.23    by (simp add: wfP_def)
    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"
    1.39    by (simp add: acyclic_def)