# HG changeset patch # User krauss # Date 1211555964 -7200 # Node ID cf147f69b3df90de0b9d8ab6d54e91ef8d857b16 # Parent 103dca19ef2ee8aa2fa8106ca0d84c67e06e8efe rearranged subsections diff -r 103dca19ef2e -r cf147f69b3df src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Fri May 23 16:41:39 2008 +0200 +++ b/src/HOL/Wellfounded.thy Fri May 23 17:19:24 2008 +0200 @@ -12,6 +12,8 @@ uses ("Tools/function_package/size.ML") begin +subsection {* Basic Definitions *} + inductive wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" for R :: "('a * 'a) set" @@ -88,6 +90,8 @@ (* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *) lemmas wf_irrefl = wf_not_refl [elim_format] +subsection {* Basic Results *} + text{*transitive closure of a well-founded relation is well-founded! *} lemma wf_trancl: assumes "wf r" @@ -129,8 +133,6 @@ done -subsubsection {* Other simple well-foundedness results *} - text{*Minimal-element characterization of well-foundedness*} lemma wf_eq_minimal: "wf r = (\Q x. x\Q --> (\z\Q. \y. (y,z)\r --> y\Q))" proof (intro iffI strip) @@ -222,7 +224,7 @@ done -subsubsection {* Well-Foundedness Results for Unions *} +subsection {* Well-Foundedness Results for Unions *} lemma wf_union_compatible: assumes "wf R" "wf S"