src/HOL/Wfrec.thy
 changeset 63572 c0cbfd2b5a45 parent 63040 eb4ddd18d635 child 69593 3dda49e08b9d
```     1.1 --- a/src/HOL/Wfrec.thy	Sun Jul 31 19:09:21 2016 +0200
1.2 +++ b/src/HOL/Wfrec.thy	Sun Jul 31 22:56:18 2016 +0200
1.3 @@ -7,20 +7,20 @@
1.4  section \<open>Well-Founded Recursion Combinator\<close>
1.5
1.6  theory Wfrec
1.7 -imports Wellfounded
1.8 +  imports Wellfounded
1.9  begin
1.10
1.11 -inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F where
1.12 -  wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
1.13 +inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F
1.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)"
1.15
1.16 -definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
1.17 -  "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
1.18 +definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
1.19 +  where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
1.20
1.21 -definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" where
1.22 -  "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)"
1.23 +definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
1.24 +  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)"
1.25
1.26 -definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
1.27 -  "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
1.28 +definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
1.29 +  where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
1.30
1.31  lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
1.32    by (simp add: fun_eq_iff cut_def)
1.33 @@ -28,13 +28,17 @@
1.34  lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
1.36
1.37 -text\<open>Inductive characterization of wfrec combinator; for details see:
1.38 -John Harrison, "Inductive definitions: automation and application"\<close>
1.39 +text \<open>
1.40 +  Inductive characterization of \<open>wfrec\<close> combinator; for details see:
1.41 +  John Harrison, "Inductive definitions: automation and application".
1.42 +\<close>
1.43
1.44  lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
1.45    by (auto intro: the_equality[symmetric] theI)
1.46
1.47 -lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
1.48 +lemma wfrec_unique:
1.49 +  assumes "adm_wf R F" "wf R"
1.50 +  shows "\<exists>!y. wfrec_rel R F x y"
1.51    using \<open>wf R\<close>
1.52  proof induct
1.53    define f where "f y = (THE z. wfrec_rel R F y z)" for y
1.54 @@ -46,44 +50,46 @@
1.55  qed
1.56
1.57  lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
1.59 -           intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
1.60 +  by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
1.61
1.62  lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
1.64 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
1.65 -apply (rule wfrec_rel.wfrecI)
1.66 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
1.67 -done
1.68 +  apply (simp add: wfrec_def)
1.69 +  apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
1.70 +   apply assumption
1.71 +  apply (rule wfrec_rel.wfrecI)
1.72 +  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
1.73 +  done
1.74
1.75
1.76 -text\<open>* This form avoids giant explosions in proofs.  NOTE USE OF ==\<close>
1.77 +text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
1.78  lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
1.79 - by (auto intro: wfrec)
1.80 +  by (auto intro: wfrec)
1.81
1.82
1.83  subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
1.84
1.85  lemma wfrec_fixpoint:
1.87 +  assumes wf: "wf R"
1.89    shows "wfrec R F = F (wfrec R F)"
1.90  proof (rule ext)
1.91    fix x
1.92    have "wfrec R F x = F (cut (wfrec R F) R x) x"
1.93 -    using wfrec[of R F] WF by simp
1.94 +    using wfrec[of R F] wf by simp
1.95    also
1.96 -  { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
1.97 -      by (auto simp add: cut_apply)
1.98 -    hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
1.100 +  have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
1.101 +    by (auto simp add: cut_apply)
1.102 +  then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
1.104    finally show "wfrec R F x = F (wfrec R F) x" .
1.105  qed
1.106
1.107 +
1.108  subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
1.109
1.110 -definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
1.111 -  "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
1.112 -   \<comment>\<open>For @{const wfrec} declarations where the first n parameters
1.113 +definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
1.114 +  where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
1.115 +   \<comment> \<open>For @{const wfrec} declarations where the first n parameters
1.116         stay unchanged in the recursive call.\<close>
1.117
1.118  lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
1.119 @@ -92,12 +98,13 @@
1.120  lemma wf_same_fst:
1.121    assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
1.122    shows "wf (same_fst P R)"
1.123 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
1.124 -apply (intro strip)
1.125 -apply (rename_tac a b)
1.126 -apply (case_tac "wf (R a)")
1.127 - apply (erule_tac a = b in wf_induct, blast)
1.128 -apply (blast intro: prem)
1.129 -done
1.130 +  apply (simp cong del: imp_cong add: wf_def same_fst_def)
1.131 +  apply (intro strip)
1.132 +  apply (rename_tac a b)
1.133 +  apply (case_tac "wf (R a)")
1.134 +   apply (erule_tac a = b in wf_induct)
1.135 +   apply blast
1.136 +  apply (blast intro: prem)
1.137 +  done
1.138
1.139  end
```