diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Wfrec.thy --- a/src/HOL/Wfrec.thy Thu Sep 04 11:53:39 2014 +0200 +++ b/src/HOL/Wfrec.thy Thu Sep 04 14:02:37 2014 +0200 @@ -10,86 +10,88 @@ imports Wellfounded begin -inductive - wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" - for R :: "('a * 'a) set" - and F :: "('a => 'b) => 'a => 'b" -where - wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==> - wfrec_rel R F x (F g x)" +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 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 - adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where - "adm_wf R F == ALL f g x. - (ALL 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)" -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 cuts_eq: "(cut f r x = cut g r x) = (ALL 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) +lemma cut_apply: "(x, a) \ R \ cut f R a x = f x" + by (simp add: cut_def) text{*Inductive characterization of wfrec combinator; for details see: John Harrison, "Inductive definitions: automation and application"*} -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y" -apply (simp add: adm_wf_def) -apply (erule_tac a=x in wf_induct) -apply (rule ex1I) -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) -apply (fast dest!: theI') -apply (erule wfrec_rel.cases, simp) -apply (erule allE, erule allE, erule allE, erule mp) -apply (blast intro: the_equality [symmetric]) -done +lemma theI_unique: "\!x. P x \ P x \ x = The P" + by (auto intro: the_equality[symmetric] theI) -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" -apply (simp add: adm_wf_def) -apply (intro strip) -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) -apply (rule refl) -done +lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\!y. wfrec_rel R F x y" + using `wf R` +proof induct + def f \ "\y. THE z. wfrec_rel R F y z" + 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 `adm_wf R F` show ?case + by (subst wfrec_rel.simps) (auto simp: adm_wf_def) +qed -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" +lemma adm_lemma: "adm_wf R (\f x. F (cut f R x) x)" + by (auto simp add: 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], assumption) apply (rule wfrec_rel.wfrecI) -apply (intro strip) apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) done text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} -lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" -apply auto -apply (blast intro: wfrec) -done +lemma def_wfrec: "f \ wfrec R F \ wf R \ f a = F (cut f R a) a" + by (auto intro: wfrec) + + +subsubsection {* Well-founded recursion via genuine fixpoints *} +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) + hence "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 {* Wellfoundedness of @{text same_fst} *} -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}" - --{*For @{text rec_def} declarations where the first n parameters +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}" + --{*For @{const wfrec} declarations where the first n parameters stay unchanged in the recursive call. *} -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 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 prem: "(!!x. P x ==> wf(R x))" - shows "wf(same_fst P R)" + assumes prem: "\x. P x \ wf (R x)" + shows "wf (same_fst P R)" apply (simp cong del: imp_cong add: wf_def same_fst_def) apply (intro strip) apply (rename_tac a b)