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,
```