Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Wellfounded_More.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.