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