src/HOL/Wellfounded.thy
changeset 26976 cf147f69b3df
parent 26803 0af0f674845d
child 27823 52971512d1a2
     1.1 --- a/src/HOL/Wellfounded.thy	Fri May 23 16:41:39 2008 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Fri May 23 17:19:24 2008 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4  uses ("Tools/function_package/size.ML")
     1.5  begin
     1.6  
     1.7 +subsection {* Basic Definitions *}
     1.8 +
     1.9  inductive
    1.10    wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
    1.11    for R :: "('a * 'a) set"
    1.12 @@ -88,6 +90,8 @@
    1.13  (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    1.14  lemmas wf_irrefl = wf_not_refl [elim_format]
    1.15  
    1.16 +subsection {* Basic Results *}
    1.17 +
    1.18  text{*transitive closure of a well-founded relation is well-founded! *}
    1.19  lemma wf_trancl:
    1.20    assumes "wf r"
    1.21 @@ -129,8 +133,6 @@
    1.22    done
    1.23  
    1.24  
    1.25 -subsubsection {* Other simple well-foundedness results *}
    1.26 -
    1.27  text{*Minimal-element characterization of well-foundedness*}
    1.28  lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
    1.29  proof (intro iffI strip)
    1.30 @@ -222,7 +224,7 @@
    1.31  done
    1.32  
    1.33  
    1.34 -subsubsection {* Well-Foundedness Results for Unions *}
    1.35 +subsection {* Well-Foundedness Results for Unions *}
    1.36  
    1.37  lemma wf_union_compatible:
    1.38    assumes "wf R" "wf S"