products/Sources/formale Sprachen/Isabelle/HOL/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: ln.xml   Sprache: Isabelle

Untersuchung 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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff