|
(* 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
