Quellcode-Bibliothek Wfrec.thy Sprache: Isabelle

(*  Title:      HOL/Wfrec.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Konrad Slind
*)

section \<open>Well-Founded Recursion Combinator\<close>

theory Wfrec
  imports Wellfounded
begin

inductive wfrec_rel :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ 'a \ 'b \ bool" for R F
  where wfrecI: "(\z. (z, x) \ R \ wfrec_rel R F z (g z)) \ wfrec_rel R F x (F g x)"

definition cut :: "('a \ 'b) \ ('a \ 'a) set \ 'a \ 'a \ 'b"
  where "cut f R x = (\y. if (y, x) \ R then f y else undefined)"

definition adm_wf :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ bool"
  where "adm_wf R F \ (\f g x. (\z. (z, x) \ R \ f z = g z) \ F f x = F g x)"

definition wfrec :: "('a \ 'a) set \ (('a \ 'b) \ ('a \ 'b)) \ ('a \ 'b)"
  where "wfrec R F = (\x. THE y. wfrec_rel R (\f x. F (cut f R x) x) x y)"

lemma cuts_eq: "(cut f R x = cut g R x) \ (\y. (y, x) \ R \ f y = g y)"
  by (simp add: fun_eq_iff cut_def)

lemma cut_apply: "(x, a) \ R \ cut f R a x = f x"
  by (simp add: cut_def)

text \<open>
  Inductive characterization of \<open>wfrec\<close> combinator; for details see:
  John Harrison, "Inductive definitions: automation and application".
\<close>

lemma theI_unique: "\!x. P x \ P x \ x = The P"
  by (auto intro: the_equality[symmetric] theI)

lemma wfrec_unique:
  assumes "adm_wf R F" "wf R"
  shows "\!y. wfrec_rel R F x y"
  using \<open>wf R\<close>
proof induct
  define f where "f y = (THE z. wfrec_rel R F y z)" for y
  case (less x)
  then have "\y z. (y, x) \ R \ wfrec_rel R F y z \ z = f y"
    unfolding f_def by (rule theI_unique)
  with \<open>adm_wf R F\<close> show ?case
    by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
qed

lemma adm_lemma: "adm_wf R (\f x. F (cut f R x) x)"
  by (auto simp: adm_wf_def intro!: arg_cong[where f="\x. F x y" for y] cuts_eq[THEN iffD2])

lemma wfrec: "wf R \ wfrec R F a = F (cut (wfrec R F) R a) a"
  apply (simp add: wfrec_def)
  apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
   apply assumption
  apply (rule wfrec_rel.wfrecI)
  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
  done

text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
lemma def_wfrec: "f \ wfrec R F \ wf R \ f a = F (cut f R a) a"
  by (auto intro: wfrec)

subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>

lemma wfrec_fixpoint:
  assumes wf: "wf R"
    and adm: "adm_wf R F"
  shows "wfrec R F = F (wfrec R F)"
proof (rule ext)
  fix x
  have "wfrec R F x = F (cut (wfrec R F) R x) x"
    using wfrec[of R F] wf by simp
  also
  have "\y. (y, x) \ R \ cut (wfrec R F) R x y = wfrec R F y"
    by (auto simp add: cut_apply)
  then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
    using adm adm_wf_def[of R F] by auto
  finally show "wfrec R F x = F (wfrec R F) x" .
qed

lemma wfrec_def_adm: "f \ wfrec R F \ wf R \ adm_wf R F \ f = F f"
  using wfrec_fixpoint by simp

subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>

definition same_fst :: "('a \ bool) \ ('a \ ('b \ 'b) set) \ (('a \ 'b) \ ('a \ 'b)) set"
  where "same_fst P R = {((x', y'), (x, y)) . x' = x \ P x \ (y',y) \ R x}"
   \<comment> \<open>For \<^const>\<open>wfrec\<close> declarations where the first n parameters
       stay unchanged in the recursive call.\<close>

lemma same_fstI [intro!]: "P x \ (y', y) \ R x \ ((x, y'), (x, y)) \ same_fst P R"
  by (simp add: same_fst_def)

lemma wf_same_fst:
  assumes "\x. P x \ wf (R x)"
  shows "wf (same_fst P R)"
proof -
  have "\a b Q. \a b. (\x. P a \ (x, b) \ R a \ Q (a, x)) \ Q (a, b) \ Q (a, b)"
  proof -
    fix Q a b
    assume *: "\a b. (\x. P a \ (x,b) \ R a \ Q (a,x)) \ Q (a,b)"
    show "Q(a,b)"
    proof (cases "wf (R a)")
      case True
      then show ?thesis
        by (induction b rule: wf_induct_rule) (use * in blast)
    qed (use * assms in blast)
  qed
  then show ?thesis
    by (clarsimp simp add: wf_def same_fst_def)
qed

end

quality98%

¤ 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.15Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.