1(* Title: HOL/Wfrec.thy 2 Author: Tobias Nipkow 3 Author: Lawrence C Paulson 4 Author: Konrad Slind 5*) 6 7section \<open>Well-Founded Recursion Combinator\<close> 8 9theory Wfrec 10 imports Wellfounded 11begin 12 13inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F 14 where wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)" 15 16definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" 17 where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)" 18 19definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" 20 where "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)" 21 22definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" 23 where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)" 24 25lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)" 26 by (simp add: fun_eq_iff cut_def) 27 28lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x" 29 by (simp add: cut_def) 30 31text \<open> 32 Inductive characterization of \<open>wfrec\<close> combinator; for details see: 33 John Harrison, "Inductive definitions: automation and application". 34\<close> 35 36lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P" 37 by (auto intro: the_equality[symmetric] theI) 38 39lemma wfrec_unique: 40 assumes "adm_wf R F" "wf R" 41 shows "\<exists>!y. wfrec_rel R F x y" 42 using \<open>wf R\<close> 43proof induct 44 define f where "f y = (THE z. wfrec_rel R F y z)" for y 45 case (less x) 46 then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y" 47 unfolding f_def by (rule theI_unique) 48 with \<open>adm_wf R F\<close> show ?case 49 by (subst wfrec_rel.simps) (auto simp: adm_wf_def) 50qed 51 52lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)" 53 by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2]) 54 55lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a" 56 apply (simp add: wfrec_def) 57 apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality]) 58 apply assumption 59 apply (rule wfrec_rel.wfrecI) 60 apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) 61 done 62 63 64text \<open>This form avoids giant explosions in proofs. NOTE USE OF \<open>\<equiv>\<close>.\<close> 65lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a" 66 by (auto intro: wfrec) 67 68 69subsubsection \<open>Well-founded recursion via genuine fixpoints\<close> 70 71lemma wfrec_fixpoint: 72 assumes wf: "wf R" 73 and adm: "adm_wf R F" 74 shows "wfrec R F = F (wfrec R F)" 75proof (rule ext) 76 fix x 77 have "wfrec R F x = F (cut (wfrec R F) R x) x" 78 using wfrec[of R F] wf by simp 79 also 80 have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y" 81 by (auto simp add: cut_apply) 82 then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x" 83 using adm adm_wf_def[of R F] by auto 84 finally show "wfrec R F x = F (wfrec R F) x" . 85qed 86 87 88subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close> 89 90definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" 91 where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}" 92 \<comment> \<open>For \<^const>\<open>wfrec\<close> declarations where the first n parameters 93 stay unchanged in the recursive call.\<close> 94 95lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R" 96 by (simp add: same_fst_def) 97 98lemma wf_same_fst: 99 assumes "\<And>x. P x \<Longrightarrow> wf (R x)" 100 shows "wf (same_fst P R)" 101proof (clarsimp simp add: wf_def same_fst_def) 102 fix Q a b 103 assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)" 104 show "Q(a,b)" 105 proof (cases "wf (R a)") 106 case True 107 then show ?thesis 108 by (induction b rule: wf_induct_rule) (use * in blast) 109 qed (use * assms in blast) 110qed 111 112end 113