# HG changeset patch # User krauss # Date 1256596036 -3600 # Node ID ab979f6e99f42572dbe7fc639e5dca69bb7dcd67 # Parent 7c61bc5d731039b265c6de4b498b23f21330428b authentic constants; moved "acyclic" further down diff -r 7c61bc5d7310 -r ab979f6e99f4 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Mon Oct 26 23:26:57 2009 +0100 +++ b/src/HOL/Wellfounded.thy Mon Oct 26 23:27:16 2009 +0100 @@ -14,19 +14,12 @@ subsection {* Basic Definitions *} -constdefs - wf :: "('a * 'a)set => bool" +definition wf :: "('a * 'a) set => bool" where "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" - wfP :: "('a => 'a => bool) => bool" +definition wfP :: "('a => 'a => bool) => bool" where "wfP r == wf {(x, y). r x y}" - acyclic :: "('a*'a)set => bool" - "acyclic r == !x. (x,x) ~: r^+" - -abbreviation acyclicP :: "('a => 'a => bool) => bool" where - "acyclicP r == acyclic {(x, y). r x y}" - lemma wfP_wf_eq [pred_set_conv]: "wfP (\x y. (x, y) \ r) = wf r" by (simp add: wfP_def) @@ -388,7 +381,13 @@ by (rule wf_union_merge [where S = "{}", simplified]) -subsubsection {* acyclic *} +subsection {* Acyclic relations *} + +definition acyclic :: "('a * 'a) set => bool" where + "acyclic r == !x. (x,x) ~: r^+" + +abbreviation acyclicP :: "('a => 'a => bool) => bool" where + "acyclicP r == acyclic {(x, y). r x y}" lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" by (simp add: acyclic_def)