(* 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.12 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.
|
