Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Wfrec.thy Sprache: Isabelle

Original von: 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

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 (clarsimp simp add: wf_def same_fst_def)
  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

end

¤ Dauer der Verarbeitung: 0.2 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.