src/HOL/Order_Relation.thy
changeset 58184 db1381d811ab
parent 55173 5556470a02b7
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Order_Relation.thy	Thu Sep 04 11:53:39 2014 +0200
     1.2 +++ b/src/HOL/Order_Relation.thy	Thu Sep 04 14:02:37 2014 +0200
     1.3 @@ -319,27 +319,6 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -subsubsection {* Well-founded recursion via genuine fixpoints *}
     1.8 -
     1.9 -lemma wfrec_fixpoint:
    1.10 -fixes r :: "('a * 'a) set" and
    1.11 -      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12 -assumes WF: "wf r" and ADM: "adm_wf r H"
    1.13 -shows "wfrec r H = H (wfrec r H)"
    1.14 -proof(rule ext)
    1.15 -  fix x
    1.16 -  have "wfrec r H x = H (cut (wfrec r H) r x) x"
    1.17 -  using wfrec[of r H] WF by simp
    1.18 -  also
    1.19 -  {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
    1.20 -   by (auto simp add: cut_apply)
    1.21 -   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
    1.22 -   using ADM adm_wf_def[of r H] by auto
    1.23 -  }
    1.24 -  finally show "wfrec r H x = H (wfrec r H) x" .
    1.25 -qed
    1.26 -
    1.27 -
    1.28  subsubsection {* Characterizations of well-foundedness *}
    1.29  
    1.30  text {* A transitive relation is well-founded iff it is ``locally'' well-founded,