(* Title: HOL/Cardinals/Wellfounded_More.thy Author: Andrei Popescu, TU Muenchen Copyright 2012
More on well-founded relations.
*)
section \<open>More on Well-Founded Relations\<close>
theory Wellfounded_More imports Main Order_Relation_More begin
subsection \<open>Well-founded recursion via genuine fixpoints\<close>
(*2*)lemma adm_wf_unique_fixpoint: fixes r :: "('a * 'a) set"and
H :: "('a \ 'b) \ 'a \ 'b" and
f :: "'a \ 'b" and g :: "'a \ 'b" assumes WF: "wf r"and ADM: "adm_wf r H"and fFP: "f = H f"and gFP: "g = H g" shows"f = g"
proof-
{fix x have"f x = g x" proof(rule wf_induct[of r "(\x. f x = g x)"],
auto simp add: WF) fix x assume"\y. (y, x) \ r \ f y = g y" hence"H f x = H g x"using ADM adm_wf_def[of r H] by auto thus"f x = g x"using fFP and gFP by simp qed
} thus ?thesis by (simp add: ext) qed
(*2*)lemma wfrec_unique_fixpoint: fixes r :: "('a * 'a) set"and
H :: "('a \ 'b) \ 'a \ 'b" and
f :: "'a \ 'b" assumes WF: "wf r"and ADM: "adm_wf r H"and
fp: "f = H f" shows"f = wfrec r H"
proof- have"H (wfrec r H) = wfrec r H" using assms wfrec_fixpoint[of r H] by simp thus ?thesis using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp qed
end
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
